Ssreflect Users Discussion List

[Ralf Jung <>]

Hi all,

when I use rewrite to instantiate an existential, I often see failures
of the proof after completing all subgoals, when running "Qed.".

For example, when I have a situation like this

  a: nat
  H: S a = 42
  ============
  S ?56 = 42

I use "rewrite H" to then solve the goal with reflexivity (or "by
rewrite H"). This seems to instantiate the existential, but something
goes wrong:

In SSReflect 1.4, after completing all subgoals, Coq informs me that I
have uninstantiated existentials left. I then instantiate them using
"Grab Existential Variables", but if I do not use the same instance that
was used when the rewrite tactic instantiated the existential, "Qed." fails.

In SSReflect 1.5, "apply" always introduces extra goals for the
existentials on my system (see the other mail I sent earlier). However,
I can still use rewrite to instantiate the existential with "last
first". Then later I solve the extra "existential" goal "apply" added,
but like for ssreflect 1.4, if I do not choose the same instance as
rewrite, I get a type checking failure on "Qed." - so the proof term
that got created is invalid.

It seems to me that this is a bug as Qed should never fail if all goals
were closed (well, tactics like fix validate this, but that's a
different matter IMHO). In any case I would appreciate guidance on
whether I should fix this on my side (by simply not ever instantiating
existentials with rewrite, but passing them as arguments explicitly), or
if this needs fixing in ssreflect.
I certainly liked this auto-instantiation a lot when I first noticed it,
as it lets me write down even less fragments of the proof term
explicitly, which IMHO is always an improvement.

Sample files to reproduce the problem are attached.

Kind regards
Ralf

Require Import ssreflect. 

Section TEST.

Definition test (a:nat):Prop := True.

Lemma L1: forall a b, S a = 42 -> test b.
Proof.
move=> ? ?. done.
Qed.

Lemma L2: forall a, S a = 42 -> test a.
Proof.
move=>a EQ.
apply: L1.
by rewrite EQ.
Grab Existential Variables.
exact 42.
Qed.

End TEST.

Require Import ssreflect. 

Section TEST.

Definition test (a:nat):Prop := True.

Lemma L1: forall a b, S a = 42 -> test b.
Proof.
move=> ? ?. done.
Qed.

Lemma L2: forall a, S a = 42 -> test a.
Proof.
move=>a EQ.
apply: L1; last first.
by rewrite EQ.
exact 0.
Qed.

End TEST.