coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Beta Ziliani <beta AT mpi-sws.org>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Using Canonical Structures for proof automation
- Date: Wed, 13 Mar 2013 10:43:51 -0400
That works, thanks so much!
-Jason
On Wed, Mar 13, 2013 at 7:14 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:
> Thanks so much! I've been able to mostly fix my problem with your help,I think "apply" is the culprit. Try replacing the line 336
> though I'm still having trouble getting tagging to work correctly; Coq
> doesn't complain about overlapping instances or anything, but it chooses to
> apply the generic version of the tag/canonical structure in preference to
> the other ones, unless I comment out the generic version. I don't have a
> minimal example, though the file I'm having trouble with is at
> https://bitbucket.org/JasonGross/catdb/src/4d72bb8c222f11ff622b472a0e3564f3cb950f19/CanonicalStructureSimplification.v?at=default
> (around line 336), if you feel like taking a look at it. I'll probably try
> to come up with a smaller example to express my problem over the next few
> days.
>
apply rsimplify_morphisms.
with
refine (rsimplify_morphisms _).
(or perhaps without the _, I'm not sure).
> -Jason
>
> P.S. What's the difference between how ssreflect tactics use canonical
> structures, and how standard tactics use canonical structures?
>
>
> On Mon, Mar 11, 2013 at 3:39 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:
>>
>> Hi Jason,
>>
>> Indeed, Coq is creating an existential there because there is no way
>> of figuring out which instance to use (even when there's only one). I
>> will explain why it is failing, and then I will propose a fix, which
>> basically follows ideas drawn in Section 4 in our paper. But let me
>> start by saying that you should seriously consider using the ssreflect
>> plugin, since ssreflect's tactics use canonical structures in a more
>> systematic way than Coq's.
>>
>> As for your problem:
>>
>> I will denote ?X as an unification variable (meta-variable)
>>
>> You have the proposition [True /\ True] and you are rewriting it the lemma
>>
>> P <-> PropDenote (PropSimplify (reified_prop S))
>>
>> so Coq changes the goal into
>>
>> PropDenote (PropSimplify (reified_prop ?S))
>>
>> where [?S : SimplifiedProp (True /\ True)]
>>
>> Now, canonical structures (CS) are triggered with an equation of the form
>>
>> proj ?S = c args
>>
>> where proj is a projector of the structure ?S, c is a constant, and
>> args are (optional) arguments of the constant. In this case, there is
>> no such an equation, so CS are not triggered.
>>
>> What you should do, instead, is to use the proposition (that is, the
>> input to your algorithm) as one of the projectors of the structure:
>>
>>
>> Structure SimplifiedProp :=
>> SimplifyProp { prop :> TaggedProp;
>> reified_prop : ReifiedProp;
>> reified_prop_ok : prop <-> PropDenote reified_prop }.
>>
>>
>> The lemma that you need goes only in one direction, there's no reason
>> to make it iif:
>>
>> Lemma SimplifyReifiyPropOk `(S : SimplifiedProp)
>> : PropDenote (PropSimplify (reified_prop S)) -> S.
>> rewrite <-PropSimplifyOk.
>> rewrite <-reified_prop_ok.
>> auto.
>> Qed.
>>
>> Now, since you have a case for any proposition, you're going to have
>> overlapping instances. Therefore, you need to differentiate them using
>> the "tagging pattern" (Section 2.3 in the paper).
>>
>> Structure TaggedProp := Tag { untag :> Prop }.
>>
>> Definition unchanged_prop_tag := Tag.
>> Definition and_tag := unchanged_prop_tag.
>> Definition false_tag := and_tag.
>> Canonical Structure true_tag P := false_tag P.
>>
>> Now, the instances:
>>
>> Canonical Structure true_inst :=
>> SimplifyProp (true_tag True) Tr (RelationClasses.reflexivity _).
>>
>> Canonical Structure false_inst :=
>> SimplifyProp (false_tag False) Fa (RelationClasses.reflexivity _).
>>
>> Program
>> Canonical Structure and_inst (S1 S2 : SimplifiedProp) :=
>> SimplifyProp (and_tag (S1 /\ S2)) (RAnd (reified_prop S1) (reified_prop
>> S2))
>> _.
>> Next Obligation. t. Qed.
>>
>> Canonical Structure unchanged_prop P : SimplifiedProp :=
>> SimplifyProp (unchanged_prop_tag P) (RProp P)
>> (RelationClasses.reflexivity _).
>>
>>
>> And you're ready to go! (note that I'm using ssreflect's apply:)
>>
>> Goal True /\ True <-> True.
>> split.
>> Focus 2.
>> intro.
>> apply: SimplifyReifiyPropOk.
>>
>>
>> If you need me to clarify something, let me know.
>>
>> Best regards,
>> Beta
>>
>>
>> On Sat, Mar 9, 2013 at 11:46 PM, Jason Gross <jasongross9 AT gmail.com>
>> wrote:
>> > Hi,
>> > I am attempting to figure out how to use canonical structures for proof
>> > automation, a la
>> > http://www.mpi-sws.org/~beta/lessadhoc/lessadhoc-extended.pdf, in
>> > particular
>> > for partial simplification of formulae. I wrote some code that resulted
>> > in
>> > Coq not being able to infer the canonical structure, and to try to
>> > figure
>> > out what I did wrong, I attempted to create a smaller example. Coq
>> > seems to
>> > replace the canonical structure with an existential in my smaller
>> > example
>> > (included below), which does not seem to be the desired behavior. Can
>> > someone give me tips, or point me to a more in depth tutorial, or
>> > examples,
>> > on using canonical structures for proof automation? Thanks.
>> >
>> > -Jason
>> >
>> > Set Implicit Arguments.
>> >
>> > Generalizable All Variables.
>> >
>> > Inductive ReifiedProp :=
>> > | Tr
>> > | Fa
>> > | RAnd : ReifiedProp -> ReifiedProp -> ReifiedProp
>> > | RProp : Prop -> ReifiedProp.
>> >
>> > Fixpoint PropDenote (r : ReifiedProp) : Prop :=
>> > match r with
>> > | Tr => True
>> > | Fa => False
>> > | RAnd a b => PropDenote a /\ PropDenote b
>> > | RProp p => p
>> > end.
>> >
>> > Fixpoint PropSimplify (r : ReifiedProp) : ReifiedProp :=
>> > match r with
>> > | Tr => Tr
>> > | Fa => Fa
>> > | RAnd a b =>
>> > match (PropSimplify a, PropSimplify b) with
>> > | (Tr, b') => b'
>> > | (Fa, _) => Fa
>> > | (a', Tr) => a'
>> > | (_, Fa) => Fa
>> > | (a', b') => RAnd a' b'
>> > end
>> > | RProp p => RProp p
>> > end.
>> >
>> > Local Ltac destruct_simpl r :=
>> > let H' := fresh in
>> > set (H' := PropSimplify r) in *;
>> > clearbody H';
>> > destruct H';
>> > simpl in *;
>> > try tauto.
>> >
>> > Lemma PropSimplifyOk (r : ReifiedProp) : PropDenote r <-> PropDenote
>> > (PropSimplify r).
>> > induction r; simpl; try tauto;
>> > split; intros; simpl in *; intuition;
>> > repeat match goal with
>> > | [ H : context[PropSimplify ?r] |- _ ] => destruct_simpl r
>> > | [ |- context[PropSimplify ?r] ] => destruct_simpl r
>> > | _ => progress intuition
>> > end.
>> > Qed.
>> >
>> > (*Structure TaggedProp := Tag { untag : ReifiedProp }. *)
>> >
>> > Structure SimplifiedProp (P : Prop) :=
>> > SimplifyProp { reified_prop : (*TaggedProp*)ReifiedProp;
>> > reified_prop_ok : P <-> PropDenote
>> > (*untag*)reified_prop }.
>> >
>> > Lemma SimplifyReifiyPropOk `(S : SimplifiedProp P)
>> > : P <-> PropDenote (PropSimplify ((*untag*) (reified_prop S))).
>> > rewrite <- PropSimplifyOk.
>> > rewrite <- reified_prop_ok.
>> > reflexivity.
>> > Qed.
>> >
>> > Local Ltac t := simpl;
>> > repeat rewrite <- reified_prop_ok;
>> > reflexivity.
>> >
>> > (*Canonical Structure unchanged_prop_tag P := @Tag P.*)
>> >
>> > Canonical Structure unchanged_prop P : SimplifiedProp P :=
>> > SimplifyProp (P := P) ((*unchanged_prop_tag*) (RProp P))
>> > (RelationClasses.reflexivity _).
>> >
>> > Goal True /\ True <-> True.
>> > split.
>> > Focus 2.
>> > intro.
>> > rewrite SimplifyReifiyPropOk.
>> > Set Printing All.
>> > (* 1 focused subgoals (unfocused: 1)
>> > , subgoal 1 (ID 20459)
>> >
>> > H : True
>> > ============================
>> > PropDenote (PropSimplify (@reified_prop (and True True) ?20457)) *)
>
>
- [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/09/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/11/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Dmitry Grebeniuk, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/11/2013
Archive powered by MHonArc 2.6.18.