Commit f61104e1 authored by charguer's avatar charguer
Browse files

ok

parent 789ecfb3
Set Implicit Arguments.
Lemma test : True.
first [ idtac | idtac ].
Set Implicit Arguments.
first [ apply S | apply I ].
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************) *)
(*************************************************************************)
(* If demo *)
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
| apply app_local_1
| match goal with H: is_local_1 ?S |- is_local (?S _) => apply H end ].
(* data base demo => tlc
Definition mydatabase := True.
Definition mykey := 3.
......@@ -38,9 +42,7 @@ Ltac xapp_pre cont ::=
| tag_apply =>
let Q := get_post tt in
is_evar Q; xuntag tag_apply; cont tt
| tag_apply =>
let Q := get_post tt in
xgc; [ xuntag tag_apply; cont tt ]
| tag_apply => xgc; [ xuntag tag_apply; cont tt | ]
| tag_let_trm => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
end.
......@@ -55,37 +57,10 @@ Lemma if_demo_spec :
Proof.
xcf. intros. xapp. xapps.
xseq (Hexists (x:int), r ~~> x \* [x = 0 \/ x = 1] \* s ~~> 5).
xif.
xuntag.
xextractible tt.
eapply local_gc_post.
first [ assumption | apply local_is_local ].
Ltac xlocal_core tt ::=
first [ assumption
|
|
[ xlocal | | ].
Ltac xapp_pre cont ::=
xextractible tt;
match ltac_get_tag tt with
| tag_apply =>
xgc; [ xuntag tag_apply; cont tt ]
| tag_let_trm => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
end.
xgc.
xapp. xapps. hsimpl~. xrets~.
introv C. xapps. hsimpl. subst. invert~ C.
xif. xapp~. hsimpl~. xrets~.
introv C. xgc. xapps. intros M. hsimpl.
...
subst. invert~ C.
Qed.
(*
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment