1
$\begingroup$

In Lean, given an equality eq: e0 = e1, one may rewrite either e0 or e1 with the other one in a proposition P using eq ▸ P.

def f: Nat → Nat := sorry

def exampleA
  (eq: x = f c)
  (ex: ∃ a, a = f c)
:
  ∃ a, a = x
:=
  eq ▸ ex

def exampleB
  (eq: x = f c)
:
  (∃ a, a = f c) = (∃ a, a = x)
:=
  eq ▸ rfl

However, the same does not work with universally quantified equalities.

def quantifiedExampleA
  (eqQuantified: ∀ c, x = f c)
  (ex: ∃ c, a = f c)
:
  ∃ (_c: Nat), a = x
:=
  -- Obviously does not work:
  -- eqQuantified ▸ ex
  
  let ⟨c, afc⟩ := ex
  ⟨c, eqQuantified c ▸ afc⟩

def quantifiedExampleB
  (eqQuantified: ∀ c, x = f c)
:
  (∃ c, a = f c) = ∃ (_c: Nat), a = x
:=
  -- Again, not working :(
  -- eqQuantified ▸ rfl
  
  propext
    (Iff.intro
      (quantifiedExampleA eqQuantified)
      (fun ex =>
        let ⟨c, ax⟩ := ex
        ⟨c, eqQuantified c ▸ ax⟩))

As the example B shows, doing these proofs manually can get cumbersome really quickly if the existentials aren't top-level. ▸ is able to do the replacement anywhere in a proposition. Is it possible to achieve the same level of "comfort" or simplicity with universally quantified equalities as we have with ordinary equalities?

Additionally: would it be possible to support multiple quantified variables, not just one?

$\endgroup$

1 Answer 1

1
$\begingroup$

There are some lemmas that help dealing with these situations. For quantifiedExampleA, you can use Exists.imp, which shortens the proof to

theorem quantifiedExampleA
    (eqQuantified : ∀ c, x = f c)
    (ex : ∃ c, a = f c) : ∃ (_c : Nat), a = x :=
  ex.imp (fun b => eqQuantified b ▸ id)

For quantifiedExampleB, there is exists_congr, which shortens the proof to

theorem quantifiedExampleB (eqQuantified : ∀ c, x = f c) :
    (∃ c, a = f c) = ∃ (_c : Nat), a = x :=
  propext (exists_congr (fun b => eqQuantified b ▸ Iff.rfl))

In fact, the simplifier is able to apply these lemmas for you, so you can just use simp/simpa:

theorem quantifiedExampleA
    (eqQuantified : ∀ c, x = f c)
    (ex : ∃ c, a = f c) : ∃ (_c : Nat), a = x := by
  simpa [← eqQuantified] using ex

theorem quantifiedExampleB (eqQuantified : ∀ c, x = f c) :
    (∃ c, a = f c) = ∃ (_c : Nat), a = x := by
  simp [← eqQuantified]
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.