The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

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