Type equality issue

Stream: lean4

[Frederic Peschanski]

I don't know if my question will have enough context but I'm blocking with a context of the form:

H1 : f x y = z
H2: T1 = T2
|-  f x (Eq.mpr (_ : T1 = T2) y) = z

I do not see how to discharge hypothesis H2 to resolve the Eq.mpr constraint and conclude.
(sorry if this does not make sense, I have a concrete example but it's kind of ugly)

[Kevin Buzzard]

Does cases H2 help? Or subst H2?

[Kevin Buzzard]

Oh sorry this is lean 4, I don't know if these tactics exist. A perhaps more helpful comment might be that you might have gone wrong at the point where the eq.mpr appeared.

[Jan-Mirko Otter]

Could you give at least the types of f, x and y? On the first sight, I have trouble understanding how your goal even typechecks.

If I try to reconstruct the type of y I find that y should have type T2 and the Eq.mpr ... has T1, so how can you put both of them into the second argument of f?

Are there any coercions between T1 and T2? As far as I know, the type checker does not care about equality, only about definitional equality. So there should be a type mismatch in the goal, shouldn't it?

If T1 and T2 are in fact definitionally equal, you can just use exact H1 because the goal would be defeq to the assumption

[Frederic Peschanski]

Thanks for the suggestions. I should have added that the equation T1 = T2 is more of the form T u1 = T u2 with u1 = u2provable, but not by definitional equality. It is not exactly the same situation but what follows maybe gives some hint.

inductive T : Nat → Prop where
  | mk (n : Nat): T n

def f: {n : Nat} → (x : T n) → (y : Nat) → Nat
  | n, _, y => n + y

#eval f (T.mk 3) 4

def same: Nat → Nat
  | n => 1 + n - 1

theorem sameEq (n : Nat): same n = n :=
by simp[same, Nat.add_comm] ; rfl

theorem dummy {n : Nat} (x : T n) (y : Nat) (z : Nat) (u : T (same n) = T n):
  f x y = z → f (Eq.mpr (u : T (same n) = T n) x) y = z :=
by
  intro H1
  ???

at the point ???, the context is :

n: Nat
x: T n
yz: Nat
u: T (same n) = T n
H1: f x y = z
⊢ f (_ : T (same n)) y = z

The difference here is that I have not an explicit Eq.mpr but still exact H1 will fail (and so is e.g. rw[u])

Maybe the general question is how to manage non-definitional Type-level equality (substitutions, etc.) ?
(sorry if all this does not make much sense, I'm rather new to lean4 ...)

[František Silváši]

I would prove it as follows:

theorem dummy {n : Nat} (x : T n) (y : Nat) (z : Nat) (u : T (same n) = T n):
  f x y = z → f (Eq.mpr (u : T (same n) = T n) x) y = z :=
by
  intro H1
  unfold f
  split
  simp only [same]
  rw [add_comm 1, Nat.add_sub_cancel, ←H1]
  rfl

[František Silváši]

I.e. unfold f and use split to generate 'per partes' equalites for the match.

[Frederic Peschanski]

Thx @František Silváši it's a good hint for me! I'm able to progress. One problem is that the split use to destruct the match introduces many fresh variables (e.g. _fun_discr✝³..., which seems to loose some information wrt. the context although not in this particular case). This reminds me of case_eq vs. case/destruct in Coq...

[František Silváši]

I am not sure exactly what your goal looks like, you can try to generalize the terms before you destruct them, which should preserve the equalities you care about. By the way, I've just realized that the split is unnecessary.
You can do:

by
  intro H1
  simp only [f, same]
  rw [add_comm 1, Nat.add_sub_cancel, ←H1]
  rfl

Unfolding f gives you the match, which you can now reduce with simp to get rid of the dependency on u (i.e. you can clear u there, as in:

  intro H1
  unfold f
  simp
  clear u

).
The rest is independent of u so simp only [same]; rw [add_comm 1, Nat.add_sub_cancel, ←H1]; rfl closes the goal. (Worth noting you need u thereuntil for your conclusion depends thereon.)

[Jan-Mirko Otter]

How about the following solution?

theorem dummy {n : Nat} (x : T n) (y : Nat) (z : Nat) (u : T (same n) = T n):
  f x y = z → f (Eq.mpr (u : T (same n) = T n) x) y = z :=
by
  intro H1
  show @f (same n) (_ : T (same n)) y = z
  exact Eq.subst
    (motive :=λ n => (h : T n) -> @f n h y = z)
    (sameEq _).symm
    (λ _ => H1)
    (Eq.mpr u x)

It's longer, but I think it explains more what is going on, and maybe helps you to adapt it to your problem.

If I understand you correctly, you want to substitue n with same n in the proposition @f n _ y = z. You can use Eq.subst for that.

The main problem is the proof term. That's why I substitute in the expression (h : T n) → @f n h y instead. Doing the substitution, you get (h : T (same n)) → @f (same n) h y = z. Then you just need to apply a simple proof of T (same n), which is given by Eq.mpr u x

[Kevin Buzzard]

Just to say again: in Lean 3 if I was faced with a goal which has an Eq.rec or one of its derivatives in it then I'd backtrack and find out how it appeared. This comes up when doing category theory in Lean 3 and there the standard fix is that if X = Y but the proof isn't rfl then we might use eq_to_hom to get a morphism X \hom Y and apply that morphism instead. The simplifier has been trained to know what to do with eq_to_hom and things tend to work out smoothly. I think that blindly soldiering on with an Eq.rec can be quite unpleasant.

[Frederic Peschanski]

Jan-Mirko Otter said:

How about the following solution?
...

Great ! I did not have the idea to use Eq.subst this way
... This might adapt to my problem, I'll tell you soon thank you !

[Frederic Peschanski]

Kevin Buzzard said:

(...) if X = Y but the proof isn't rfl then we might use eq_to_hom to get a morphism X \hom Y and apply that morphism instead. (...)

I guess Lean4 is not yet ready for let's say a higher-level approach (hopefully mathlib4 will catch up at some point). I should add that I get such relatively strange proof contexts through very lean4-ish type-level computations (in fact, playing with sized-types like vectors).

[Frederic Peschanski]

Problem solved with cast_eq ...