Proving theorems about functions involving equality rewrites

Stream: lean4

[Anand Rao]

I am facing some trouble proving theorems about a function that makes use of an equality rewrite (in my case, this was done to ensure consistency with the declared output type). I have replicated the essence of the issue in the following code snippet:

structure Foo (n : Nat) where
  foo : Nat

def Foo.bar₁ {m n : Nat} : Foo m → Foo n → Foo (n + m)
  | ⟨f₁⟩, ⟨f₂⟩ => ⟨f₁ + f₂⟩

def Foo.bar₂ {m n : Nat} : Foo m → Foo n → Foo (m + n) :=
    Nat.add_comm n m ▸ Foo.bar₁

theorem barEquiv {m n : Nat} : ∀ fm : Foo m, ∀ fn : Foo n, (Foo.bar₁ fm fn).foo = (Foo.bar₂ fm fn).foo := by
  intro fm fn
  simp [Foo.bar₁, Foo.bar₂]
  -- Goal : fm.1 + fn.1 =
  -- (Eq.rec (motive := fun α x => Foo m → Foo n → Foo α) (fun x x_1 => { foo := x.1 + x_1.1 }) (_ : n + m = m + n) fm fn).foo
  sorry

I am unable to proceed here because the portion involving the equality rewrite is blocking the simplification. Does anyone know of a way around this? Thanks in advance.

[Leonardo de Moura]

You can use the following

theorem barEquiv {m n : Nat} : ∀ fm : Foo m, ∀ fn : Foo n, (Foo.bar₁ fm fn).foo = (Foo.bar₂ fm fn).foo := by
  intro fm fn
  simp [Foo.bar₁, Foo.bar₂]
  generalize n+m=i, Nat.add_comm n m=h
  -- We applied the `generalize` tactic to make sure we can use the `subst` tactic
  subst h
  -- After this `subst`, the `Eq.rec` application will reduce since its major premise is now an `Eq.refl`
  rfl

In the future, we will add better support for Eq.rec to the simp tactic.

[Gabriel Ebner]

Another (also more generally applicable) trick is to push casts into structures as far as possible:

def Foo.bar₂ {m n : Nat} (f₁ : Foo m) (f₂ : Foo n) : Foo (m + n) where
  foo := (Foo.bar₁ f₁ f₂).foo
  -- bar := Nat.add_comm n m ▸ (Foo.bar₁ f₁ f₂).bar

This has the additional advantage that (Foo.bar₁ f₁ f₂).foo will reduce definitionally. We do this extensively in mathlib for various structures, see e.g. docs#decidable_of_iff

[Anand Rao]

Thank you very much for the suggestions. I have a related question about simplifying functions with termination proofs, which I will ask on a separate thread.