The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.

-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)) *)