coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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)) *)
- [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/09/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/11/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Dmitry Grebeniuk, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Dmitry Grebeniuk, 03/14/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Jason Gross, 03/13/2013
- Re: [Coq-Club] Using Canonical Structures for proof automation, Beta Ziliani, 03/11/2013
Archive powered by MHonArc 2.6.18.