The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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