Zulip Chat Archive
Stream: lean4
Topic: Implicit arguments
Dan Velleman (Nov 26 2022 at 14:43):
This example works:
example (P : Nat → Prop) : (∀ {x : Nat}, P x) → ∀ {x : Nat}, P x := by
intro h
exact h
But this one doesn't:
example (P : Nat → Prop) : (∀ {x : Nat}, P x) → ∀ {x : Nat}, P x := by
intro h
have h2 : 0 = 0 := Eq.refl 0
exact h
The exact h
in the second example generates the error:
type mismatch
h
has type
P ?m.190 : Prop
but is expected to have type
∀ {x : Nat}, P x : Prop
In both examples, in the tactic state, both h
and the goal are listed as ∀ {x : Nat}, P x
, so it looks to a user like exact h
should work. Examining the expressions for h
and the goal, they are identical except that in the second example, the goal has mdata
associated with it that says "noImplicitLambda". It is the introduction of h2
that causes that mdata
to be attached to the goal, which explains why the first example works but the second doesn't.
Is this how it's supposed to work?
Yury G. Kudryashov (Jan 11 2024 at 23:00):
Here is an #mwe
structure TestProp (p : Nat → Prop) : Prop where
add : ∀ ⦃m n⦄, p m → p n → p (m + n)
structure TestProp' (p : Nat → Prop) : Prop where
add : ∀ {m} ⦃n⦄, p m → p n → p (m + n)
example : TestProp fun _ ↦ True where
add := fun _ _ _ _ ↦ trivial
example : TestProp' fun _ ↦ True where
add := fun _ _ ↦ trivial
Note that in the second example, I need two underscores, not three. IMHO, this is a bug. Occurred to me on Mathlib with the actual predicate implying s ⊆ t
for some sets: ∀ {{x}}
from the definition of ⊆
got autointroduced.
Last updated: May 02 2025 at 03:31 UTC