Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem with terms differing in their obligations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with terms differing in their obligations


chronological Thread 
  • From: Adam Koprowski <adam.koprowski AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Problem with terms differing in their obligations
  • Date: Mon, 1 Mar 2010 21:47:31 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :content-type; b=Eg0qfvmJmLCRDd6rM4PFHQfR+50ornav9PLRvEAhZ1uMV8ss39ESzCLqGOSalgmxAs XahnBE44hdreZ0oOMweTuKjTmFIYlDM/VTdT2Vpv3NStz+DmQu1BTc8eQWcsDoyyJQ31 0cTsGIa3pdg/e20hCvrmYHI0b1D4k3/z+JF14=

  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]



Archive powered by MhonArc 2.6.16.

Top of Page