Search code examples
coq

Why we can't use "simpl" on `j = j -> x = y`?

I am trying to solve the injection_ex3 exercise in Software Foundation Volume 1.

I have the following prove

Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  j = z :: l ->
  x = y.
Proof.
  intros t x y z l j.
  intros H1 H2.
  injection H1 as Hnm1.
  assert (H3: z :: j = z :: z :: l).
  replace j with (z :: l).
  reflexivity.
  injection H3.
  rewrite <- H2.

and it gives me like

1 goal
t : Type
x, y, z : t
l, j : list t
Hnm1 : x = z
H : y :: l = j
H2 : j = z :: l
H3 : z :: j = z :: z :: l
______________________________________(1/1)
j = j -> x = y

I think since j = j is always true, so I can always have x = y. However, when I use simpl, I can no further simplify the goal.

So, is there any solution to make coq accept that j = j -> x = y?

Solution

  • The simple answer is that simpl doesnt do that kind of "simplification" of the proof. simpl does things like replacing variables with their definitions (unfolding/folding), beta reduction, etc. but it does not remove hypotheses from the environment.

    In this particular case, to "simplify" the goal from j=j -> x=y to the new "simpler" goal x=y, you can move the antecedent into the context with the tactict intros.