Commit 789ecfb3 authored by charguer's avatar charguer
Browse files

ok

parent 8ec95c50
Set Implicit Arguments.
Lemma test : True.
first [ idtac | idtac ].
first [ apply S | apply I ].
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************)
(*************************************************************************) *)
(* If demo *)
(* data base demo => tlc
Definition mydatabase := True.
Definition mykey := 3.
Lemma mylemma : True -> True. auto. Qed.
Hint Extern 1 (Register mydatabase mykey) => Provide mylemma.
Lemma ltac_database_demo : True.
ltac_database_get mydatabase mykey. intros _.
try ( ltac_database_get mydatabase 3 ). (* fails --no conversion *)
auto.
Qed.
*)
Ltac get_post tt :=
match goal with |- ?E =>
match get_fun_arg E with (_,?Q) => constr:(Q)
end end.
Ltac xapp_pre cont ::=
xextractible tt;
match ltac_get_tag tt with
| 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_let_trm => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
end.
Lemma if_demo_spec :
Spec if_demo (b:bool) |B>>
B [] (fun (x:int) => [0 <= x <= 1]).
Proof.
xcf. intros. xapps. xapps.
xcf. intros. xapp. xapps.
xseq (Hexists (x:int), r ~~> x \* [x = 0 \/ x = 1] \* s ~~> 5).
xif. xapps. hsimpl~. xrets~.
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.
Qed.
......
......@@ -159,7 +159,8 @@ Proof. auto. Qed.
(*--------------------------------------------------------*)
(* ** tools for post-conditions *)
Ltac post_is_meta tt :=
(* TODO: deprecated *)
Ltac post_is_meta tt :=
match goal with |- ?E =>
match get_fun_arg E with (_,?Q) =>
match Q with
......
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