xlet_fixed

examples/BasicDemos/Demo_proof.v

 Set Implicit Arguments.
-Require Import LibTactics CFHeaps CFLib LibInt LibWf Demo_ml.
+Require Import LibTactics CFHeaps (* LibInt LibWf *).
+Require Import Demo_ml.
+Require Import CFLib.
 
 
 
@@ -7,30 +9,60 @@ Open Scope tag_scope.
 
 
 
+(********************************************************************)
+(* ** Let-function *)
 
 
+Lemma let_fun_poly_id_spec :
+  app let_fun_poly_id [tt] \[] \[= 3].
+Proof using.
+  xcf. xfun. xapp.
+Qed.
 
-
-
-
-(********************************************************************)
-(* ** Let-pattern *)
-
-Lemma let_pattern_pair_int () =
-   let (x,y) = (3,4) in
-   x
+Lemma let_fun_poly_pair_homogeneous () =
+  let f (x:'a) (y:'a) = (x,y) in
+  f 3 3
 Proof using.
   xcf.
 Qed.
 
-Lemma let_pattern_pair_int_wildcard () =
-   let (x,_) = (3,4) in
-   x
+Lemma let_fun_on_the_fly () =
+  (fun x f -> f x) 3 (fun x -> x+1) 
 Proof using.
   xcf.
 Qed.
 
 
+Lemma let_fun_const_spec : 
+  app let_fun_const [tt] \[] \[= 3].
+Proof using.
+  xcf. dup 9.
+  { xfun. apply Sf. xrets~. }
+  { xfun as g. apply Sg. skip. }
+  { xfun as g G. apply G. skip. }
+  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]).
+    { apply Sf. skip. } 
+    { apply Sf. } }
+  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h.
+    { apply Sh. skip. } 
+    { apply Sh. } }
+  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h H.
+    { apply H. skip. } 
+    { apply H. } }
+  { xfun (fun g => app g [tt] \[] \[=3]).
+    { xrets~. } 
+    { apply Sf. } }
+  { xfun (fun g => app g [tt] \[] \[=3]) as h.
+    { skip. } 
+    { skip. } }
+  { xfun (fun g => app g [tt] \[] \[=3]) as h H.
+    { skip. } 
+    { skip. } }
+Qed.
+
+
+
+
 
 (********************************************************************)
 (* ** Let-term *)
@@ -52,38 +84,6 @@ Proof using.
 Qed.
 
 
-(********************************************************************)
-(* ** Let-function *)
-
-Lemma let_fun_const () =
-  let f () = 3 in
-  f()
-Proof using.
-  xcf.
-Qed.
-
-Lemma let_fun_poly_id () =
-  let f x = x in
-  f 3
-Proof using.
-  xcf.
-Qed.
-
-Lemma let_fun_poly_pair_homogeneous () =
-  let f (x:'a) (y:'a) = (x,y) in
-  f 3 3
-Proof using.
-  xcf.
-Qed.
-
-Lemma let_fun_on_the_fly () =
-  (fun x f -> f x) 3 (fun x -> x+1) 
-Proof using.
-  xcf.
-Qed.
-
-
-
 
 
 
@@ -255,6 +255,20 @@ Proof using.
 Qed.
 
 
+(********************************************************************)
+(* ** Let-pattern *)
+
+Lemma let_pattern_pair_int_spec : 
+  app let_pattern_pair_int [tt] \[] \[= 3].
+Proof using. xcf. xmatch. xrets~. Qed.
+
+Lemma let_pattern_pair_int_wildcard_spec :
+  app let_pattern_pair_int_wildcard [tt] \[] \[= 3].
+Proof using. xcf. xmatch. xrets~. Qed.
+
+
+
+
 
 (********************************************************************)
 (********************************************************************)

generator/characteristic.ml

@@ -590,7 +590,7 @@ let rec cfg_exp env e =
         let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
         let cf_body = cfg_exp env' body in 
         add_used_label (fst (List.hd ncs));
-        Cf_letfunc (ncs, cf_body)
+        Cf_fun (ncs, cf_body)
         (* --todo: check what happens with recursive types *)
 
       (* let-binding of a single value *)
@@ -624,7 +624,7 @@ let rec cfg_exp env e =
            let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
            let cf = cfg_exp env' body in
            add_used_label x;
-           Cf_letval (x, fvs_strict, fvs_others, typ, v, cf)
+           Cf_val (x, fvs_strict, fvs_others, typ, v, cf)
 
         (* term let-binding *)
         end else begin

generator/formula.ml

@@ -14,8 +14,8 @@ type cf =
   | Cf_body of var * vars * typed_vars * coq * cf
   | Cf_let of typed_var * cf * cf
   | Cf_letpure of var * vars * vars * coq * cf * cf
-  | Cf_letval of var * vars * vars * coq * coq * cf
-  | Cf_letfunc of (var * cf) list * cf
+  | Cf_val of var * vars * vars * coq * coq * cf
+  | Cf_fun of (var * cf) list * cf
   | Cf_caseif of coq * cf * cf
   | Cf_case of coq * typed_vars * coq * coq option *
       (typed_var * coq) list * cf * cf

generator/formula.mli

@@ -27,9 +27,9 @@ type cf =
     (* Let x := Q1 in Q2 *)
   | Cf_letpure of var * vars * vars * coq * cf * cf 
     (* Let x [Ai,Bi] := Q1 in Q2  // where x : forall Ai.T *)
-  | Cf_letval of var * vars * vars * coq * coq * cf 
+  | Cf_val of var * vars * vars * coq * coq * cf 
     (* Let x [Ai,Bi] := v in Q2  // where x : forall Ai.T *)
-  | Cf_letfunc of (var * cf) list * cf 
+  | Cf_fun of (var * cf) list * cf 
     (* Let fi := Qi in Q *)
   | Cf_caseif of coq * cf * cf 
     (* If v Then Q1 else Q2 *)

generator/formula_to_coq.ml

@@ -65,7 +65,7 @@ let rec coqtops_of_imp_cf cf =
       let is_spec_k = Coq_app (Coq_var ("is_spec_" ^ sarity), var_k) in
       let hyp_k = coq_foralls targs (coq_apps var_k args_of_k) in
       let concl_k = coq_apps spec_n [var_k; coq_var f] in
-      coq_tag "tag_body" (coq_forall_types fvs (coq_foralls ["K", type_of_k] (coq_impls [is_spec_k;hyp_k] concl_k)))       
+      coq_tag "tag_app_curried" (coq_forall_types fvs (coq_foralls ["K", type_of_k] (coq_impls [is_spec_k;hyp_k] concl_k)))       
       (* (!B: (forall Ai K, is_spec_2 K -> 
                  (forall x1 x2, K x1 x2 F) -> spec_2 K f)) *)
   *)
@@ -79,7 +79,7 @@ let rec coqtops_of_imp_cf cf =
       let h_body_2 = Coq_impl (h_body_hyp, h_body_conc) in
       let h_body_1 = coq_foralls [("H", hprop); ("Q", Coq_impl (typ, hprop))] h_body_2 in
       let h_body = coq_forall_types fvs (coq_foralls targs h_body_1) in
-      coq_tag "tag_body" (coq_conj h_curried h_body)
+      coq_tag "tag_app_curried" (coq_conj h_curried h_body)
       (* (!B: curried 2 f /\ 
               (forall Ai x1 x2 H Q, CF H Q -> app f [(dyn t1 x1) (dyn t2 x2)] H Q) *)
 
@@ -88,17 +88,27 @@ let rec coqtops_of_imp_cf cf =
       let type_of_q1 = Coq_impl (typ, hprop) in
       let c1 = coq_apps (coq_of_cf cf1) [h; q1] in
       let c2 = coq_foralls [x,typ] (coq_apps (coq_of_cf cf2) [(Coq_app (q1, Coq_var x)); q]) in
-      funhq "tag_let_trm" ~label:x (coq_exist "Q1" type_of_q1 (coq_conj c1 c2))
+      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_letval (x, fvs_strict, fvs_other, typ, v, cf) ->
+  | Cf_val (x, fvs_strict, fvs_other, typ, v, cf) ->
       let type_of_x = coq_forall_types fvs_strict typ in
       let equ = coq_eq (Coq_var x) (coq_fun_types fvs_strict v) in
       let conc = coq_apps (coq_of_cf cf) [h;q] in
-      funhq "tag_let_val" (*~label:x*) (Coq_forall ((x, type_of_x), Coq_impl (equ, conc)))
+      funhq "tag_val" (*~label:x*) (Coq_forall ((x, type_of_x), Coq_impl (equ, conc)))
       (*(!!L x: (fun H Q => forall (x:forall Ai,T), x = (fun Ai => v) -> F H Q)) *)
  
-  | Cf_letfunc (ncs, cf) ->
+  | Cf_fun (ncs, cf) ->
+      let ns, cs = List.split ncs in
+      let fs = List.map (fun n -> (n, val_type)) ns in
+      let chyps = List.map coq_of_cf cs in
+      let cconc = coq_apps (coq_of_cf cf) [h;q] in
+      let x = List.hd ns in
+      funhq "tag_fun" ~label:x (coq_foralls fs (coq_impls chyps cconc))
+      (* (!F a: fun H Q => forall f1 f2, B1 -> B2 -> F H Q) *)            
+
+  (* DEPRECATED
+  | Cf_fun (ncs, cf) ->
       let ns, cs = List.split ncs in
       let p_of n = "P" ^ n in
       let fs = List.map (fun n -> (n, val_type)) ns in
@@ -110,9 +120,10 @@ let rec coqtops_of_imp_cf cf =
       let c2conc = coq_apps (coq_of_cf cf) [h;q] in
       let c2 = coq_impls c2hyps c2conc in
       let x = List.hd ns in
-      funhq "tag_let_fun" ~label:x (coq_foralls fs (coq_exists ps (coq_conj c1 c2)))
+      funhq "tag_fun" ~label:x (coq_foralls fs (coq_exists ps (coq_conj c1 c2)))
       (* (!F a: fun H Q => forall f1 f2, exists P1 P2,
               (B1 -> B2 -> P1 f1 /\ P2 f2) /\ (P1 f1 -> P2 f2 -> F H Q)) *)            
+   *)
 
  (* old
    | Cf_caseif (cf0,cf1,cf2) ->

lib/coq/CFTactics.v

@@ -1217,155 +1217,117 @@ Tactic Notation "xval_st" constr(P) :=
   xval_st_anonymous_impl P.
 
 
-
 (*--------------------------------------------------------*)
-(* ** [xbody] *)
-
-(* TODO: DEPRECATED
-
-(** [xbody] applies to a goal of the form 
-    [H: (Body f x1 .. xN => Q) |- Spec_n f K]
-    where H is the last hypothesis in the goal.
-    It applies this hypothesis to prove the goal. 
-    Two subgoals are generated. The first one
-    is [is_spec_n K], and [xisspec] is called to try and solve it.
-    The second one is [forall x1 .. xN, K x1 .. xN Q].
-    The arguments are introduced automatically, unless the
-    tactic [xbody_nointro] is called.
-
-    The tactic [xbody H] can be used to specify explicitly
-    the hypothesis [H] (of the form [Body ..]) to be used for 
-    proving a goal [Spec_n f K], and it does not clear [H]. *)
+(* ** [xfun] *)
 
-Ltac xbody_core cont :=
-   let Bf := fresh "TEMP" in 
-   intros Bf; sapply Bf; clear Bf;
-   [ try xisspec | cont tt ].
 
-Ltac xbody_pre tt :=
-  let H := get_last_hyp tt in generalizes H.
+(** [xfun] applies to a goal of the form [(LetFunc f := H in F) H Q].
+    The tactic introduces an hypothesis describing the most-general
+    specification of [f], and leaves [F H Q] as goal.
+   
+    - [xfun as f] can be used to name the function.
 
-Ltac xbody_base_intro tt :=
-  xbody_core ltac:(fun _ => remove_head_unit tt; introv).
+    - [xfun as f Hf] can be used to name the function and its 
+      specification.
 
-Ltac xbody_base_nointro tt :=
-  xbody_core ltac:(fun _ => remove_head_unit tt).
+    - [xfun P] can be used to give a specification for [f], proved
+      with respect to the most-general specification. Here, [P]
+      should take the form [fun f => spec_of_f].
 
-Tactic Notation "xbody" :=
-  xbody_pre tt; xbody_base_intro tt.
-Tactic Notation "xbody_nointro" :=
-  xbody_pre tt; xbody_base_nointro tt.
+    - [xfun_no_simpl P] is like the above but does not attempt to
+      automatically exploit the most general specification for
+      proving the special specification.
 
-Tactic Notation "xbody" ident(Bf) :=
-  generalizes Bf; xbody_base_intro tt.
-Tactic Notation "xbody_nointro" ident(Bf) :=
-  generalizes Bf; xbody_base_nointro tt.
+    - Also available:
+      [xfun P as f] 
+      [xfun P as f Hf] 
+      [xfun_no_simpl P as f]
+      [xfun_no_simpl P as f Hf]
+     
+ 
 
-(* todo: add xuntag body *)
 
 *)
 
-(*--------------------------------------------------------*)
-(* ** [xfun] *)
+Ltac xfun_pre tt :=
+  xuntag tag_fun; apply local_erase.
 
-(* TODO: update:
-
-
-(** [xfun P] applies to a goal of the form [LetFunc f := F1 in F].
-    The argument [P] is the specification for [f1], which should be 
-    a predicate of type [func -> Prop]. Typically, [S] takes the form
-    [fun f => Spec f n K]. 
-    
-    By default, the tactic [xbody] is called subsequently, so as to 
-    exploit the body assumption stored in [F1]. 
-    [xfun_no_xbody P] can be used to disable the call to [xbody].
-    [xfun_no_xbody P as H] can be used to name the body assumption. *)
-
-
-Ltac xfun_common P Pf cont :=
-  exists P; split; [ cont tt | intros Pf ].
-  (* TODO: have a mode where Pf is not introduced automatically? *)
-
-Ltac xfun_core P cont :=
-  apply local_erase;
+Tactic Notation "xfun" := 
+  xfun_pre tt; 
   intro; 
-  let f := get_last_hyp tt in
-  let Pf := fresh "P" f in
-  xfun_common P Pf cont.
-
-(* TODO: factorize with above *)
-Ltac xfun_core_as f P cont :=
-  apply local_erase;
-  intro f; 
-  let Pf := fresh "P" f in
-  xfun_common P Pf cont.
-
-Ltac xfun_namebody tt :=
   let f := get_last_hyp tt in 
-  let Bf := fresh "B" f in
-  intros Bf.
-
-Ltac xfun_xbody_cont tt :=
-  first [ xbody_base_intro tt | xfun_namebody tt ].
-
-Tactic Notation "xfun" constr(P) :=
-  xfun_core P ltac:(fun tt => xfun_xbody_cont tt).
-Tactic Notation "xfun" constr(P) as ident(f) :=
-  xfun_core_as f P ltac:(fun tt => xfun_xbody_cont tt)..
+  let Hf := fresh "S" f in 
+  intros Hf.
 
-Tactic Notation "xfun_no_xbody" constr(P) :=
-  xfun_core P ltac:(xfun_namebody).
-Tactic Notation "xfun_no_xbody" constr(P) "as" ident(B) :=
-  xfun_core P ltac:(fun _ => intros B).
-   (* TODO: above, should be "as f" as well *)
-
-
-(* TODO: document these variants, if they are useful *)
-
-Tactic Notation "xfun_no_intro" constr(P) :=
-  xfun_core P ltac:(fun _ => first [ xbody_base_nointro tt | xfun_namebody tt ] ).
-
-
-(** [xfun] without argument is equivalent to calling [xfun S]
-    where [S] would be the most general specification for the
-    function, namely, the characteristic formula itself.
-    
-    This tactic is useful to simulate the inlining of the 
-    function at its call sites, and reason only on particular
-    applications of the function.
-    
-    [xfun as f] allows renaming the function. *)
-
-Ltac xfun_most_general_core tt :=
-  apply local_erase;
-  intro; let f := get_last_hyp tt in let H := fresh "P" f in
-  esplit; split; intros H; [ pattern f in H; eexact H | ].
-
-Tactic Notation "xfun" := 
-    xfun_most_general_core tt.
+Tactic Notation "xfun" "as" ident(f) := 
+  xfun_pre tt; 
+  intros f;
+  let Hf := fresh "S" f in 
+  intros Hf.
+
+Tactic Notation "xfun" "as" ident(f) ident(Hf) := 
+  xfun_pre tt; 
+  intros f Hf.
+
+(* [xfun_spec_as f P Hf cont1] applies to a goal of the form
+   [most_general_spec_of_f -> F H Q] and it produces two subgoals:
+   - [Hf: most_general_spec_of_f |- P f]
+   - [Hf: P f |- F H Q]
+   In the former goal, the continuation [cont1] is applied.
+*)
 
-Ltac xfun_most_general_core_as f := (* todo: factorize *)
-  apply local_erase; intro f; let H := fresh "P" f in
-  esplit; split; intros H; [ pattern f in H; eexact H | ].
+Ltac xfun_spec_as f P Hf cont1 :=
+  let H := fresh "B" f in
+  assert (H: P f); 
+  [ cont1 Hf
+  | clear Hf; rename H into Hf ].
 
-Tactic Notation "xfun" "as" ident(f) := 
-    xfun_most_general_core_as f.
+Ltac xfun_spec_as_0 P cont :=
+  xfun_pre tt; 
+  intro; 
+  let f := get_last_hyp tt in 
+  let Hf := fresh "S" f in 
+  intros Hf;
+  xfun_spec_as f P Hf cont.
+
+Ltac xfun_spec_as_1 P f cont :=
+  xfun_pre tt; 
+  intros f;
+  let Hf := fresh "S" f in 
+  intros Hf;
+  xfun_spec_as f P Hf cont.
+
+Ltac xfun_spec_as_2 P f Hf cont :=
+  xfun_pre tt; 
+  intros f Hf;
+  xfun_spec_as f P Hf cont.
+
+(* [xfun_simpl Hf] applies to a goal of the form 
+   [Hf: most_general_spec_of_f |- P f]  
+   and it exploits [Hf] then clears it in order to prove the goal. *)
+
+Ltac xfun_simpl Hf :=
+  eapply Hf; clear Hf. (* hnf  first? *) 
+  
+Tactic Notation "xfun" constr(P) := 
+  xfun_spec_as_0 P ltac:(fun Hf => xfun_simpl Hf).
 
+Tactic Notation "xfun" constr(P) "as" ident(f) := 
+  xfun_spec_as_1 P f ltac:(fun Hf => xfun_simpl Hf).
 
-(** [xfun P1 P2] allows to specify a pair of mutually-recursive
-    functions, be providng both their specifications. *)
+Tactic Notation "xfun" constr(P) "as" ident(f) ident(Hf) := 
+  xfun_spec_as_2 P f Hf ltac:(fun Hf => xfun_simpl Hf).
 
-Tactic Notation "xfun" constr(P1) constr(P2) :=
-  intro; let f1 := get_last_hyp tt in
-  intro; let f2 := get_last_hyp tt in
-  let Bf1 := fresh "B" f1 in let Bf2 := fresh "B" f2 in
-  let Pf1 := fresh "P" f1 in let Pf2 := fresh "P" f2 in
-  exists P1; exists P2; split; [ intros Bf1 Bf2 | intros Pf1 Pf2 ].
+Tactic Notation "xfun_no_simpl" constr(P) := 
+  xfun_spec_as_0 P ltac:(fun _ => idtac).
 
-  (* TODO: support higher number of mutually recursive functions. *)
+Tactic Notation "xfun_no_simpl" constr(P) "as" ident(f) := 
+  xfun_spec_as_1 P f ltac:(fun _ => idtac).
 
+Tactic Notation "xfun_no_simpl" constr(P) "as" ident(f) ident(Hf) := 
+  xfun_spec_as_2 P f Hf ltac:(fun _ => idtac).
 
-*)
+(* TODO: support higher number of mutually recursive functions. *)
 
 
 (*--------------------------------------------------------*)
@@ -1422,7 +1384,7 @@ Ltac xret_pre cont :=
   xextract_check_not_needed tt;
   match cfml_get_tag tt with
   | tag_ret => cont tt
-  | tag_let_trm => xlet; [ cont tt | instantiate ]
+  | tag_let => xlet; [ cont tt | instantiate ]
   end. 
 
   (* LATER: should we have a special treatment of xlet/xret
@@ -2043,7 +2005,7 @@ Tactic Notation "xspec" constr(f) :=
 
 Ltac cfml_apply_xseq_or_xlet_to_see_function cont :=
   match cfml_get_tag tt with
-  | tag_let_trm => xlet; [ cont tt | ]
+  | tag_let => xlet; [ cont tt | ]
   | tag_seq => xseq; [ cont tt | ]
   | _ => cont tt
   end.
@@ -2156,7 +2118,7 @@ Ltac xapp_prepare_goal cont :=
     | false => xgc; [ xuntag tag_apply; cont tt | ]
     | true => xuntag tag_apply; cont tt
     end
-  | tag_let_trm => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
+  | tag_let => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
   | tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
   end.
 
@@ -2222,7 +2184,7 @@ Ltac xapps_core H E cont :=
   let cont1 tt := xapp_core H E cont in
   let cont2 tt := instantiate; try xextract; try intro_subst in    
   match cfml_get_tag tt with
-  | tag_let_trm => xlet; [ cont1 tt | cont2 tt ]
+  | tag_let => xlet; [ cont1 tt | cont2 tt ]
   | tag_seq => xseq; [ cont1 tt | cont2 tt ]
   | tag_apply => xapp_core H E cont
   end.
@@ -2686,9 +2648,12 @@ Tactic Notation "xcf" constr(f) :=
     let H := fresh in intros H; hnf in H; revert H end.
 
 Ltac xcf_show_name f :=
-  let H := fresh "Spec" in intros H;
-  try match type of H with tag tag_top_val _ => hnf in H end.
-  (* TODO: can't we make a name based on f? *)
+  let H := fresh "Spec" in
+  first [ intros [_ H] 
+        | intros H ].
+  (* try match type of H with tag tag_top_val _ => hnf in H end. *)
+
+ (* LATER: maybe we want to see [curried]? *)
 
 Ltac xcf_show_core tt :=
   intros;