Zulip Chat Archive

Stream: lean4

Topic: Type equality issue


Frederic Peschanski (Sep 01 2022 at 22:17):

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 (Sep 01 2022 at 22:20):

Does cases H2 help? Or subst H2?

Kevin Buzzard (Sep 01 2022 at 22:22):

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 (Sep 02 2022 at 04:58):

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 (Sep 02 2022 at 09:51):

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 (Sep 02 2022 at 10:03):

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 (Sep 02 2022 at 10:05):

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

Frederic Peschanski (Sep 02 2022 at 11:22):

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 (Sep 02 2022 at 11:36):

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 (Sep 02 2022 at 21:01):

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 (Sep 02 2022 at 22:14):

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 (Sep 04 2022 at 13:34):

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 (Sep 04 2022 at 13:38):

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 (Sep 28 2022 at 15:57):

Problem solved with cast_eq ...


Last updated: Dec 20 2023 at 11:08 UTC