Ssreflect Users Discussion List

[Beta Ziliani <>]

The reason why I'm asking is because this is one of the few places where our algorithm breaks Mathcomp compilation. In a few places of the library all_and2 is used as a view, and since our algorithm solves the equation above, then those lines break. From your description I gather that our algorithm is right, and those lines in MathComp should be changed.

Cheers,
Beta

Written from mobile. Excuse my limited communication.

On May 1, 2015 6:51 AM, "Georges Gonthier" <> wrote:

  Hi Beta,

this is a known issue, whose root cause is the historical error of encoding A <-> B as (A -> B) /\ (B -> A) in the Coq prelude.

  The “view” operation move/v: H, as its name suggests, does do more than application: it looks at v as some form of equivalence under which H is to be “interpreted”. It has a catalogue of such interpretations, declared using Hint View, and it tries to use these before resorting to guessing the number of implicit arguments required for direct application, when the type of v is a quantified inductive – for instance the reflect predicate.

  This is more general than coercion to Funclass (when andP AandB is interpreted as elimT andP AandB) because more than one interpretation can be tried – using an equivalence right-to-left, or on contrapositives, for instance.

  In addition to the views for reflect declared in ssrbool.v, ssreflect.v declares views for the iff predicate, but, due to the ill-advised encoding of iff, these will interpret all_and2 as an “equivalence” – specifically move/all_and2: H  gets interpreted as move: {H}(iffLR (@all_and2 _ _ _ _) H), hence the weird result: if you do solve the equation the predicate applied to H has type ?P -> ?P.

  I’m not sure why Coq fails to do so (failing to recognize Miller patterns – I suspect the flex-flex heuristics) , though the fact it does gets us off the hook here. A possible workaround would be to have a view form of all_and2 tha is stated as an equivalence, so the iffLR view would actually always be used – however, since it is not a coercion, we’d still need the current version for direct application.

   Cheers,

Georges

 

From: [mailto:] On Behalf Of Beta Ziliani
Sent: 30 April 2015 22:17
To:
Subject: [ssreflect] Difference between move/L and move=>H; move: {H}(L H)

 

Dear ssr devs:

I know [move/L] do some more stuff than [move=>H; move: {H}(L H)], but what is it exactly? I'm having a weird behavior testing it with our unification algorithm[1].

An example is the following:

Goal (forall x, x > 0 /\ x < 1) -> False.

When doing
move=>H; move: {H}(all_and2 H).

I get the expected result:
(forall x : nat, x > 0) /\ (forall x : nat, x < 1) -> False

However with
move/all_and2.

I get (with our algorithm) a weird expansion:
  (((forall x : nat, x > 0 /\ x < 1) ->
     (forall x0 : nat, x0 > 0 /\ x0 < 1) /\
     (forall x0 : nat, x0 > 0 /\ x0 < 1)) -> forall x : nat, x > 0 /\ x < 1) ->
   False

The trace of the algorithm shows that there is unification step that is present in [move/all_and2], and not present in [move: (all_and2 H)]:
(forall x : ?X61, ?X62 x) /\ (forall x : ?X61, ?X63 x) =?= ?X59 <-> ?X60

which our algorithm expands to
(forall x : ?X61, ?X62 x) /\ (forall x : ?X61, ?X63 x)
=?= (?X59 -> ?X60) /\ (?X60 -> ?X59)

And solves. I don't quite understand why Coq's algorithm fails to solve this equation (according to my understanding of the code it should), and why that seems to be the expected behavior in this case.

 

Any help is appreciated.

Beta

[1] https://github.com/unicoq/unicoq