coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
--
Adam Koprowski [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]
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]
- [Coq-Club] Problem with terms differing in their obligations, Ian Lynagh
- Re: [Coq-Club] Problem with terms differing in their obligations, Adam Koprowski
Archive powered by MhonArc 2.6.16.