Ssreflect Users Discussion List

[Ralf Jung <>]

Hi all,

I am having trouble with proof scripts working fine with ssreflect 1.4,
but failing with ssreflect 1.5. I am very new to ssreflect, so the issue
may just as well be on my side, but still the behaviour looks strange to me.

The attached "minimal example" proof script works fine for me with Coq
8.4pl3 and SSReflect 1.4, but fails when I used SSRfelect 1.5 instead.
For some reason, when apply adds an existential variable, it now also
adds a new goal for that variable. Is that the expected behaviour?

In the first proof, this results in three goals being opened instead of
two, so the "first" tactical selects a different goal in the newer
version, which breaks the script.

In the second proof, it gets even better: I get the following error message
  Anomaly: Evd.define: cannot define an evar twice. Please report.

I would appreciate if you could clarify whether there's a problem with
my script, or whether this is a bug in the library.

Kind regards
Ralf



Require Import ssreflect.

Section TEST.

Parameter A: Type.
Parameter world: Type.
Definition prop := world -> Prop.
Parameter wle: world-> world -> Prop.

Goal forall (P:prop) (w w':world), wle w w' -> P w ->
   (forall (w : world), P w -> forall (w' : world), wle w w' -> P w') -> 
    P w'.
Proof.
move => P w w' H_wle HP.
by apply; first by apply HP.
Qed.

Goal forall (P:prop) (w w':world), wle w w' -> P w ->
   (forall (w : world), P w -> forall (w' : world), wle w w' -> P w') -> 
    P w'.
Proof.
move => P w w' H_wle HP.
by apply; last by apply H_wle.
Qed.

End TEST.