The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

That works, thanks so much!

-Jason

On Wed, Mar 13, 2013 at 7:14 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:

On Wed, Mar 13, 2013 at 6:32 AM, Jason Gross <jasongross9 AT gmail.com> wrote:
> Hi,

> Thanks so much!  I've been able to mostly fix my problem with your help,
> 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.
>

I think "apply" is the culprit. Try replacing the line 336
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)) *)
>
>