demo1

examples/BasicDemos/Demo_proof.v

@@ -8,28 +8,52 @@ Require Import Stdlib.
 
 
 
+Ltac xapply_core H cont1 cont2 ::=
+  forwards_nounfold_then H ltac:(fun K =>
+    match cfml_postcondition_is_evar tt with
+    | true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try xok ]
+    | false => eapply local_frame_gc; [ xlocal | sapply K | cont1 tt | cont2 tt ]
+    end).
 
-Lemma max_spec' : forall (n m:int),
-  app max [n m] 
-    PRE \[] 
-    POST \[= Coq.ZArith.BinInt.Zmax n m ].
-Abort.
 
-Lemma max_spec'' : forall (n m:int),
-  app max [n m] 
-    PRE \[] 
-    RET x ST \[x = Coq.ZArith.BinInt.Zmax n m ].
-Abort.
+(** [xassert] applies to a goal of the form [(Assert F) H Q],
+    (or, more generally, of the form [(Seq_ (Assert F) ;; F') H Q],
+    in which case [xseq] is called first.).
 
+    It produces two subgoals: [F H (fun (b:bool) => \[b = true] \* H)]
+    and [H ==> Q tt]. The second one is discharged automatically
+    if [Q] is not instantiated---this is the case whenever. *) 
 
+Ltac xassert_core tt :=
+  xuntag tag_assert;
+  apply local_erase;
+  split; [ | try xok ].
 
+Ltac xassert_pre cont := 
+  xextract_check_not_needed tt;
+  match cfml_get_tag tt with
+  | tag_assert => cont tt
+  | tag_seq => xseq; [ cont tt | instantiate ]
+  end. 
 
+Tactic Notation "xassert" :=  
+  xassert_pre ltac:(fun _ => xassert_core tt).
 
 
+(********************************************************************)
+(* ** Type annotations *)
 
+let annot_let () =
+   let x : int = 3 in x
 
+let annot_tuple_arg () =
+   (3, ([] : int list))
 
+let annot_pattern_var x =
+   match (x : int list) with [] -> 1 | _ -> 0
 
+let annot_pattern_constr () =
+   match ([] : int list) with [] -> 1 | _ -> 0
 
 
 (********************************************************************)
@@ -118,8 +142,8 @@ Proof using.
   { xapp3. }
   dup 4.
   { xseq. xapp. xapp. xsimpl~. }
-  { xapp. intro_subst. xapp. xsimpl~. }
-  { xapps. xapps. xsimpl~. }
+  { xapp. intro_subst. xapp. }
+  { xapps. xapps. }
   { xapps. xapps~. }
 Qed.
 
@@ -150,9 +174,9 @@ Lemma let_val_poly_spec :
   app let_val_poly [tt] \[] \[= 3].
 Proof using.
   xcf. dup 3.
-  xval. x ret. xsimpl. auto.
-  xval as r. xrets~.
-  xvals. xrets~.
+  { xval. xret. xsimpl. auto. }
+  { xval as r. xrets~. } 
+  { xvals. xrets~. }
 Qed.
 
 
@@ -194,12 +218,11 @@ Proof using.
   { xapp1.
     xapp2.
     dup 5. 
-    { apply Spec. xret. }
-    { xapp3_no_apply. Focus 2. apply S. xret. }
-    { xapp3_no_simpl. xret. }
-    { xapp3. xret. }
-    { xapp. xret. xsimpl~. }
-    xsimpl~.
+    { apply Spec. xrets. auto. }
+    { xapp3_no_apply. Focus 2. apply S. xrets. auto. }
+    { xapp3_no_simpl. xrets~. }
+    { xapp3. xrets~. }
+    { xapp. xret. xsimpl~. } }
 Qed.
 
 Lemma let_fun_poly_pair_homogeneous_spec : 
@@ -224,10 +247,16 @@ Proof using.
   xsimpl~.
 Qed.
 
-let let_fun_in_let () =
-  let f = (assert (true); fun x -> x) in
-  f
-
+Lemma let_fun_in_let_spec :
+  app let_fun_in_let [tt] \[] 
+    (fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
+Proof using.
+  xcf. xlet (fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
+    (* TODO: could we get away by typing just [xlet] above? *)
+  { xassert. { xret. }
+    xfun. xrets. =>>. xapp. xrets~. }
+  { =>> M. xrets~. }
+Qed. 
 
 
 (********************************************************************)
@@ -237,7 +266,7 @@ Lemma let_term_nested_id_calls_spec :
   app let_term_nested_id_calls [tt] \[] \[= 2].
 Proof using.
   xcf.
-  xfun (fun f => forall (x:int), app f [x] \[] \[= x]). { xret~. }
+  xfun (fun f => forall (x:int), app f [x] \[] \[= x]). { xrets~. }
   xapps. 
   xapps.
   xapps.
@@ -248,7 +277,7 @@ Lemma let_term_nested_pairs_calls_spec :
   app let_term_nested_pairs_calls [tt] \[] \[= ((1,2),(3,(4,5))) ].
 Proof using.
   xcf. 
-  xfun (fun f => forall A B (x:A) (y:B), app f [x y] \[] \[= (x,y)]). { xret~. }
+  xfun (fun f => forall A B (x:A) (y:B), app f [x y] \[] \[= (x,y)]). { xrets~. }
   xapps.
   xapps.
   xapps.
@@ -268,7 +297,7 @@ Proof using.
   { xmatch_no_alias. xalias. xalias as L. skip. }
   { xmatch_no_cases. dup 6. 
     { xmatch_case.
-      { xrets~. } 
+      { xrets*. } 
       { xmatch_case. } }
     { xcase_no_simpl.
       { dup 3.
@@ -294,11 +323,11 @@ Lemma match_nested_spec :
 Proof using.
   xcf. xval. dup 3.
   { xmatch_no_simpl.  
-    { xrets~. } 
+    { xrets*. } 
     { false. (* note: [xrets] would produce a ununified [hprop]. 
      caused by [tryfalse] in [hextract_cleanup]. TODO: avoid this. *) } }
   { xmatch.
-    xrets~. 
+    xrets*. 
     (* second case is killed by [xcase_post] *) }
   { xmatch_no_intros. skip. skip. }
 Qed.
@@ -847,19 +876,5 @@ let (top_val_pair_fun_1,top_val_pair_fun_2) = (fun x -> x), (fun x -> x)
 
 
 
-(********************************************************************)
-(* ** Type annotations *)
-
-let annot_let () =
-   let x : int = 3 in x
-
-let annot_tuple_arg () =
-   (3, ([] : int list))
-
-let annot_pattern_var x =
-   match (x : int list) with [] -> 1 | _ -> 0
-
-let annot_pattern_constr () =
-   match ([] : int list) with [] -> 1 | _ -> 0
 
 *)
\ No newline at end of file

generator/characteristic.ml

@@ -1463,7 +1463,7 @@ and cfg_module id m =
 let cfg_file str =
    [ Cftop_coqs ([ 
       Coqtop_set_implicit_args; 
-      Coqtop_require [ "Coq.ZArith.BinInt"; "LibLogic"; "LibRelation"; "LibInt"; "Shared"; "CFHeaps"; "CFApp" ];  
+      Coqtop_require [ "Coq.ZArith.BinInt"; "TLC.LibLogic"; "TLC.LibRelation"; "TLC.LibInt"; "TLC.LibListZ"; "CFML.Shared"; "CFML.CFHeaps"; "CFML.CFApp" ];  
       Coqtop_require_import ["CFHeader"];
       Coqtop_require ["CFPrint"];
       Coqtop_custom "Open Scope list_scope.";

lib/coq/CFTactics.v

@@ -1574,14 +1574,26 @@ Tactic Notation "xfun_ind" constr(R) constr(S) :=
 (*--------------------------------------------------------*)
 (* ** [xret] and [xret_no_gc] and [xrets] *)
 
-(** [xret] applies to a goal of the form [(Ret v) H Q].
+(** [xret] applies to a goal of the form [(Ret v) H Q],
+    (or, more generally, on goals of the from 
+    [(Let x := (Ret V) in F) H Q] in which case
+    [xlet] is called first).
 
     It changes the goal to [H ==> Q v \* \GC],
     where [\GC] can be instantiated with garbage.
     Use [xret_no_gc] to only produce the goal [H ==> Q v].
 
-    [xret] automatically calls [xclean].
-    [xret_no_clean] may be used to disable [xclean]. *)
+    Note that [xret] automatically calls [xclean].
+
+    Variants:
+
+    - [xret_no_clean] may be used to disable [xclean].
+    
+    - [xret_no_gc] can be used to not introduce an existentially-
+      quantified heap for garbage collection.
+
+    - [xrets] is short for [xret; xsimpl].
+*)
 
 (* Lemma used by [xret] *)
 
@@ -1613,11 +1625,11 @@ Proof using.
 Qed.
 
 
-Ltac xret_core :=
+Ltac xret_core tt :=
   first [ apply xret_lemma_unify
         | eapply xret_lemma ].
 
-Ltac xret_no_gc_core :=
+Ltac xret_no_gc_core tt :=
   first [ apply xret_lemma_unify
         | eapply xret_no_gc_lemma ].
 
@@ -1636,28 +1648,22 @@ Ltac xret_pre cont :=
     end. *)
 
 Tactic Notation "xret_no_clean" := 
-  xret_pre ltac:(fun _ => xret_core).
+  xret_pre ltac:(fun _ => xret_core tt).
 
 Tactic Notation "xret" := 
-  xret_pre ltac:(fun _ => xret_core; xclean).
+  xret_pre ltac:(fun _ => xret_core tt; xclean).
 Tactic Notation "xret" "~" :=  
   xret; xauto~.
 Tactic Notation "xret" "*" :=  
   xret; xauto*.
 
-
-(** [xret_no_gc] can be used to not introduce an existentially-
-    quantified heap for garbage collection. *)
-
 Tactic Notation "xret_no_gc" := 
-  xret_no_gc_core.
+  xret_no_gc_core tt.
 Tactic Notation "xret_no_gc" "~" :=  
   xret_no_gc; xauto~.
 Tactic Notation "xret_no_gc" "*" :=  
   xret_no_gc; xauto*.
 
-(** [xrets] is short for [xret; xsimpl].*)
-
 Ltac xrets_base :=
   xret; xsimpl.
 

lib/stdlib/Makefile

@@ -102,6 +102,8 @@ Pervasives.cmj: Pervasives.ml $(CFML_MLV)
 	
 Array_ml.vo List_ml.vo: Pervasives_ml.vo
 Array_ml.vio List_ml.vio: Pervasives_ml.vio
+Stdlib.vo: Array_ml.vo List_ml.vo Pervasives_ml.vo
+Stdlib.vio: Array_ml.vio List_ml.vio Pervasives_ml.vio
 
 %_ml.vo: %.cmj
 # Needed only when developing CFML. Ideally, should be removed.