Search code examples
dependent-typelean

Composing dependent functions in Lean

In Lean 4, this code compiles:

variable (α : Type)
variable (f : {p : α → Prop} → (x : α) → p x)
variable (g : {a b : Prop} → a → a ∨ b)
#check g ∘ f

But this code does not:

variable (α : Type) (p : α → Prop)
variable (f : (x : α) → p x)
variable (g : {a b : Prop} → a → a ∨ b)
#check g ∘ f

The error I get is:

application type mismatch
  g ∘ f
argument
  f
has type
  ∀ (x : α), p x : Prop
but is expected to have type
  ?m.224 → ?m.227 : Prop

Can someone explain why the second piece of code fails?

Solution

  • ∘ can't compose dependent functions.

    In first example, the argument p in f is infered as fun _ => a, so f become independent function so ∘ works coincidentally.

    If you want to compose dependent functions, write fun a => g (f a), or use g ∘' f in Mathlib.