Unifying dependent types

Stream: lean4

[verified_whale]

Hi, I'm someone who's mainly been working with Coq and started dabbling in Lean recently. Currently I am facing the problem of wanting to unify dependent type arguments. Specifically assume I have the constructor T (n : nat) and want to show the equality of T (a + (b + c)) and T ((a + b) + c) (see this playground). In the Coq world I could define a program lemma, where I could prove the equivalence of the dependent arguments for the types. How would I go about handling this in Lean 4?

[Kevin Buzzard]

You can prove it via a rewrite but then the proof involves an axiom so is difficult to use. This is a real Achilles heel in lean and I had expected things to be the same in Coq. I have no idea what "define a program lemma" means and would be happy to hear more. In the liquid tensor experiment we usually don't attempt to use the resulting equalities, we define isomorphisms from T(x) to T(x') if x=x' and train the simplifier to cancel these isomorphisms when it can. Why do you need the equalities?

[František Silváši 🦉]

The way you state test surely cannot work in Coq either, with the exact kind of error you're getting in Lean. I don't know what a program lemma in Coq is, but an approach I have seen Coq people take quite a bit also translates to Lean just fine - e.g. Coq's Vector library defines a cast function and then states 'these kinds of theorems' in terms of it.

inductive Test (n : nat)
| T : Test

def eqT {n : nat} (t1 : Test n) (t2 : Test n) := true.

-- Here we can use h to give proofs of equality for indices.
def Test.cast (m : ℕ) (x : Test m) (n : ℕ) (h : m = n) : Test n := eq.mpr (congr_arg _ h.symm) x

--  add_assoc _ _ _ relates these specific indices.
theorem test (a b c : nat) : eqT (Test.T (a + (b + c))) (Test.cast _ (Test.T (a + b + c)) _ (add_assoc _ _ _)) := sorry

[Eric Wieser]

Note that that playground link points to a very old version of Lean 3, not Lean 4!

[Kyle Miller]

Ah, @František Silváši 🦉 beat me to it. This is a pattern I've been using when you need to deal with equality on indices:

inductive Test : Nat → Type
| T (n : Nat) : Test n

def Test.cast (x : Test n) (h : n = m) : Test m :=
  Eq.rec x h

@[simp] theorem Test.cast_rfl (x : Test n) : x.cast rfl = x := rfl

@[simp] theorem Test.cast_cast (x : Test a) (h : a = b) (h' : b = c) :
  (x.cast h).cast h' = x.cast (h.trans h') := rfl

def eqT {n : Nat} (t1 : Test n) (t2 : Test n) := True

theorem test (a b c : Nat) :
  eqT ((Test.T (a + (b + c))).cast (by rw [Nat.add_assoc])) (Test.T ((a + b) + c)) :=
True.intro

[Kyle Miller]

(The differences here are just that it's in Lean 4 and it has a couple useful boilerplate simp lemmas.)

[verified_whale]

Re: How this would work in Coq: When you define such a lemma in Coq you'd define it as a program lemma, which would let you use a tactic to unify the types. In effect a program lemma generates a lemma that makes use of eq_rect and carries a proof term of the equalities, similar to what was suggested in this thread. Here's the (admittedly, sparse) documentation https://coq.inria.fr/refman/addendum/program.html. And it's a bummer that Lean doesn't support this. In an ideal world it would be great, if one could first prove the dependent types equal and if that's the case proceed to prove the two statements in equal. Would such a feature cause any undesirable side effects?

[Kyle Miller]

I've seen that documentation before, but I've never really understood what the feature is about... Is it that a "program lemma" is a program that can generate lemmas for you, depending on the context? If so, a relevant Lean feature is its system for generating congruence lemmas.

Here's a Lean 3 example, using the convert tactic which makes use of this system:

inductive Test : nat → Type
| T (n : nat) : Test n

def eqT {n : nat} (t1 : Test n) (t2 : Test n) := true.

theorem test (a b c : nat) :
  eqT (Test.T (a + (b + c))) (by { convert Test.T (a + b + c) using 1, rw add_assoc }) := sorry

(The using 1 is to tell it to only try unifying the types using only a single step.)

[Kyle Miller]

convert creates proof obligations for each so-far-not-unified pair of terms.

[Mario Carneiro]

From what I can recall, the major advantage of Program Fixpoint is that you get proofs in the match that you are not in previous cases, but this is supported in lean 4 with the split tactic

[verified_whale]

@Kyle Miller Thanks for the pointer to convert. This looks like what I am looking for. With theses conversions, are you still able to rewrite with the resulting theorems easily or will there be extraneous equality proof terms to take care of?