Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Using Canonical Structures for proof automation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Using Canonical Structures for proof automation


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Using Canonical Structures for proof automation
  • Date: Sat, 9 Mar 2013 17:46:55 -0500

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



Archive powered by MHonArc 2.6.18.

Top of Page