Commit a1e04229 authored by charguer's avatar charguer

introduce cf_let

parent 8860950f
......@@ -957,6 +957,7 @@ let order_record () =
(********************************************************************)
(* ** While loops *)
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
Proof using.
......
......@@ -87,6 +87,15 @@ let rec coqtops_of_imp_cf cf =
(* (!B: curried 2 f /\
(forall Ai x1 x2 H Q, CF H Q -> app f [(dyn t1 x1) (dyn t2 x2)] H Q) *)
| Cf_let ((x,typ), cf1, cf2) ->
let c1 = coq_of_cf cf1 in
let c2 = Coq_fun ((x, typ), coq_of_cf cf2) in
let f_core = coq_apps (coq_var "CFML.CFPrint.cf_let") [c1;c2] in
let f = Coq_app (Coq_var "CFML.CFHeaps.local", f_core) in
coq_tag "tag_let" ~label:x f
(* OLD
| Cf_let ((x,typ), cf1, cf2) ->
let q1 = Coq_var "Q1" in
let type_of_q1 = Coq_impl (typ, hprop) in
......@@ -94,6 +103,7 @@ let rec coqtops_of_imp_cf cf =
let c2 = coq_foralls [x,typ] (coq_apps (coq_of_cf cf2) [(Coq_app (q1, Coq_var x)); q]) in
funhq "tag_let" ~label:x (coq_exist "Q1" type_of_q1 (coq_conj c1 c2))
(* !L: fun H Q => exists Q1, F1 H Q1 /\ forall (x:T), F2 (Q1 x) Q *)
*)
| Cf_let_poly (x, fvs_strict, fvs_other, typ, cf1, cf2) ->
let type_of_x = coq_forall_types fvs_strict typ in
......
......@@ -631,11 +631,22 @@ Notation "'Funs' f1 ':=' K1 'and' f2 ':=' K2 'and' f3 ':=' K3 'in' F" :=
(********************************************************************)
(** Let *)
Definition cf_let (A B : Type) (F1:~~A) (F2:A->~~B) : ~~ B :=
(fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 x (Q1 x) Q).
Implicit Arguments cf_let [A B].
Notation "'Let' x ':=' F1 'in' F2" :=
(!Let (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 (Q1 x) Q))
(!Let (cf_let F1 (fun x => F2)))
(at level 69, x ident, right associativity,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
(* OLD
Notation "'Let' x ':=' F1 'in' F2" :=
(!Let (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 (Q1 x) Q))
(at level 69, x ident, right associativity, only parsing,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
*)
Notation "'Let' x ':' T ':=' F1 'in' F2" :=
(!Let (fun H Q => exists Q1, F1 H Q1 /\ forall x:T, F2 (Q1 x) Q))
(at level 69, x ident, right associativity, only parsing) : charac.
......
......@@ -1067,39 +1067,58 @@ Qed.
Ltac xlet_core cont0 cont1 cont2 :=
apply local_erase;
cont0 tt;
split; [ | cont1 tt; cont2 tt ];
xtag_pre_post.
match goal with |- cf_let ?F1 (fun x => _) ?H ?Q =>
cont0 tt;
split; [ | cont1 x; cont2 tt ];
xtag_pre_post
end.
Ltac xlet_def cont0 cont1 cont2 :=
Ltac xlet_pre tt :=
xpull_check_not_needed tt;
xuntag tag_let;
xlet_core cont0 cont1 cont2.
xuntag tag_let.
Tactic Notation "xlet" constr(Q) "as" simple_intropattern(x) :=
Ltac xlet_def cont0 cont1 cont2 :=
xlet_pre tt; xlet_core cont0 cont1 cont2.
Ltac xlet_intros_cont x :=
let a := fresh x in intros a.
Ltac xlet_spec_as Q x :=
xlet_def
ltac:(fun _ => exists Q)
ltac:(fun _ => intros x)
ltac:(fun _ => try xpull).
Tactic Notation "xlet" constr(Q) :=
Ltac xlet_spec Q :=
xlet_def
ltac:(fun _ => exists Q)
ltac:(fun _ => intro)
xlet_intros_cont
ltac:(fun _ => try xpull).
Tactic Notation "xlet" "as" simple_intropattern(x) :=
Ltac xlet_as x :=
xlet_def
ltac:(fun _ => esplit)
ltac:(fun _ => intros x)
ltac:(fun _ => idtac).
Tactic Notation "xlet" :=
Ltac xlet_basic tt :=
xlet_def
ltac:(fun _ => esplit)
ltac:(fun _ => intro)
xlet_intros_cont
ltac:(fun _ => idtac).
Tactic Notation "xlet" constr(Q) "as" simple_intropattern(x) :=
xlet_spec_as Q x.
Tactic Notation "xlet" constr(Q) :=
xlet_spec Q.
Tactic Notation "xlet" "as" simple_intropattern(x) :=
xlet_as x.
Tactic Notation "xlet" :=
xlet_basic tt.
Tactic Notation "xlet" "~" := xlet; xauto~.
Tactic Notation "xlet" "~" "as" simple_intropattern(x) := xlet as x; xauto~.
Tactic Notation "xlet" "~" constr(Q) := xlet Q; xauto~.
......@@ -1219,29 +1238,32 @@ Tactic Notation "xlet" "*" constr(Q) "as" simple_intropattern(x) := xlet Q as x;
Use [xseq_no_xpull H'] to prevent [xpull] from being
called automatically after [xseq H']. *)
Ltac xseq_core cont0 cont1 :=
apply local_erase;
cont0 tt;
split; [ | cont1 tt ];
xtag_pre_post.
Ltac xseq_pre tt :=
xpull_check_not_needed tt;
xuntag tag_seq.
Ltac xseq_noarg_core tt :=
xseq_pre tt;
xlet_core
xseq_core
ltac:(fun _ => esplit)
ltac:(fun _ => idtac)
ltac:(fun _ => idtac).
Ltac xseq_arg_core H :=
xseq_pre tt;
xlet_core
xseq_core
ltac:(fun _ => first [ exists (#H) | exists H ])
ltac:(fun _ => idtac)
ltac:(fun _ => try xpull).
Ltac xseq_no_xpull_core H :=
xseq_pre tt;
xlet_core
xseq_core
ltac:(fun _ => first [ exists (#H) | exists H ])
ltac:(fun _ => idtac)
ltac:(fun _ => idtac).
Tactic Notation "xseq" :=
......
......@@ -269,6 +269,7 @@ Definition cf_fail : formula := fun H Q =>
False.
(*------------------------------------------------------------------*)
(* ** Instance of [app] for primitive operations *)
......@@ -524,7 +525,27 @@ Notation "'Fail'" :=
(at level 69) : charac.
Open Scope charac.
(* Capturing bound names
Definition test := local (cf_let (cf_val val_unit) (fun a =>
local (cf_let (local (cf_val val_unit)) (fun b => cf_val (val_pair a b))))).
Lemma test' : forall H Q, test H Q.
Proof using.
unfolds test. intros.
apply local_erase.
match goal with |- cf_let _ (fun x => _) _ _ =>
let w := fresh x in
esplit; split; [ | intros w] end.
admit.
Qed.
*)
(*--------------------------------------------------------*)
(* ** Tactics for conducting proofs *)
......
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