The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Hi Ian,

  A quick answer would be: take a look at the proof-irrelevance axiom (Coq.Logic.ProofIrrelevance), which will allow you to equate such obligations. 

  Adam

On Mon, Mar 1, 2010 at 21:37, Ian Lynagh <igloo AT earth.li> wrote:

Hi all,

I am stuck, with a goal:
   << p :> s >> <~~>* << p :> s >>
which I want to prove with
   apply Same.
where Same is defined as:
   := Same : forall (s : Sequence patchUniverse from to contains),
             (<<s>> <~~>* <<s>>)

Unfortunately, this fails with
   Error: Impossible to unify "p :> s" with "p :> s".
as the two (p :> s) terms are not as identical as they appear. With
notations off, they differ in the obligation functions that they
contain:
   Error: Impossible to unify
 "Cons p s
   (EnlargeTransitiveCommuteRelation2_obligation_4 patchUniverse from mid to
      contains contains' p s s pNotInTail containsOK)
   (EnlargeTransitiveCommuteRelation2_obligation_5 patchUniverse from mid to
      contains contains' p s s pNotInTail containsOK)
   (EnlargeTransitiveCommuteRelation2_obligation_6 patchUniverse from mid to
      contains contains' p s s pNotInTail containsOK)" with
 "Cons p s
   (EnlargeTransitiveCommuteRelation2_obligation_1 patchUniverse from mid to
      contains contains' p s s pNotInTail containsOK)
   (EnlargeTransitiveCommuteRelation2_obligation_2 patchUniverse from mid to
      contains contains' p s s pNotInTail containsOK)
   (EnlargeTransitiveCommuteRelation2_obligation_3 patchUniverse from mid to
      contains contains' p s s pNotInTail containsOK)".

I can see why it doesn't work, but I can't see how I can reasonably
solve it. Has anyone got any suggestions please? I've attached the
cut-down example.


Thanks
Ian

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]