xfor

TODO

@@ -23,8 +23,12 @@ MAJOR TODAY
 
 - for downto
 
+- inline CFHeader.pred  as -1
+
 MAJOR NEXT
 
+- xchanges
+
 - record with
 
 - when clauses
@@ -35,6 +39,8 @@ MAJOR NEXT
 
 - open no scope in CF.
 
+- add support for pure records
+
 
 MAJOR NEXT NEXT
 
@@ -51,10 +57,6 @@ MAJOR POSTPONED
 
 - support float
 
-- add support for pure records
-  => need type information for normalization
-  => how to shared typed/untyped AST
-
 - implement the work around for type abbreviations:
    type typerecb1 = | Typerecb_1 of typerecb2
     and typerecb2 = typerecb1 list

examples/BasicDemos/Demo_proof.v

@@ -6,22 +6,36 @@ Require Import Stdlib.
 
 
 
-(********************************************************************)
-(* ** For loops 
-
-(*
 
-   (a > b /\  H ==> Q tt )
-\/ (a <= b+1 /\  H ==> I a  /\ (forall i ...) /\  I (b+1) ==> (Q tt))
-*)
 
+(********************************************************************)
+(* ** For loops *)
+
+Lemma for_to_incr_spec : forall (r:int), r >= 0 ->
+  app for_to_incr [r] \[] \[= r].
+Proof using.
+  xcf. xapps. unfolds CFHeader.pred. dup 7. 
+  { xfor. intros S LS HS.
+    cuts PS: (forall i, (i <= r) -> S i (n ~~> i) (# n ~~> r)).
+    { applys PS. math. }
+    { intros i. induction_wf IH: (upto r) i. intros Li.
+      applys (rm HS). xif.
+      { xapps. applys IH. hnf. skip. skip. (* math. *) }
+      { xrets. skip. (* math. *) } } 
+    xapps. xsimpl~. } 
+  { xfor as S. skip. skip. }
+  { xfor_inv (fun (i:int) => n ~~> i). skip. skip. skip. skip. } 
+  { xseq (# n ~~> r). xfor_inv (fun (i:int) => n ~~> i). skip. skip. skip. skip. skip. }
+  { xseq (# n ~~> r). xfor_inv_void. skip. skip. skip. }
+  { xfor_inv_void. skip. skip. }
+  { xseq (# n ~~> r). 
+    xfor_inv_case (fun (i:int) => n ~~> i); intros C.
+    { exists \[]. splits. skip. skip. skip. } 
+    { false. skip. (* math. *) }
+    { xapps. xsimpl~. } }
+Qed.
 
-let for_to_incr r =
-   let n = ref 0 in
-   for i = 0 to pred r do
-      incr n;
-   done;
-   !n
+(* TODO
 
 let for_downto r =
    let n = ref 0 in
@@ -29,6 +43,7 @@ let for_downto r =
       incr n;
    done;
    !n
+
 *)
 
 
@@ -701,12 +716,16 @@ Proof using.
   xcf. xif. xrets~.
 Qed.
 
+(*
+Ltac xauto_tilde ::= xauto_tilde_default ltac:(fun _ => auto_tilde).
+*)
+
 Lemma lazyop_term_spec : 
   app lazyop_term [tt] \[] \[= 1].
 Proof using.
   xcf. xfun (fun f => forall (x:int), 
     app f [x] \[] \[= isTrue (x = 0)]). 
-  { xrets~. }
+  { xrets*. }
   xapps.
   xlet. 
   { dup 3. 
@@ -725,7 +744,7 @@ Lemma lazyop_mixex_spec :
 Proof using.
   xcf. xfun (fun f => forall (x:int), 
     app f [x] \[] \[= isTrue (x = 0)]). 
-  { xrets~. }
+  { xrets*. }
   xlet \[= true].
   { xif. xapps. xlet \[= true].
     { xif. xapps. xlet \[= true]. 
@@ -804,7 +823,7 @@ Proof using.
   dup 2.
   { => k. induction_wf IH: (downto 0) k. xcf.
     xif.
-    { xrets~. }
+    { xrets. math. }
     { xif.
       { xfail. math. }
       { xapps (k-1). 
@@ -827,7 +846,7 @@ Proof using.
   intros. cuts G: (forall (m:int),
      (forall x, x <= m -> x >= 0 -> app rec_mutual_f [x] \[] \[= x])
   /\ (forall x, x+1 <= m -> x >= -1 -> app rec_mutual_g [x] \[] \[= x+1])). 
-  { split; intros x P; specializes G (x+1); destruct G as [G1 G2]; xapp~. }
+  { split; intros x P; specializes G (x+1); destruct G as [G1 G2]; xapp; try math. }
   => m. induction_wf IH: (downto 0) m. split; intros x Lx Px.
   { xcf. xif. xrets~. xapp (x-1).
     unfolds. skip. (* TODO *) skip. skip.  

generator/formula_to_coq.ml

@@ -178,6 +178,29 @@ let rec coqtops_of_imp_cf cf =
       (* (!S: fun H Q => exists Q', F1 H Q /\ F2 (Q' tt) Q *)
 
   | Cf_for (i_name,v1,v2,cf) ->
+      let s = Coq_var "S" in
+      let i = Coq_var i_name in
+      let typs = Coq_impl (coq_int,formula_type) in
+      let locals = Coq_app (Coq_var "CFML.CFHeaps.is_local_pred", s) in
+      let snext = coq_apps s [ coq_plus i (Coq_int 1) ] in
+      let cf_step = Cf_seq (cf, Cf_manual snext) in 
+      let cf_ret = Cf_ret coq_tt in
+      let cond = coq_apps (Coq_var "TLC.LibReflect.isTrue") [ coq_le i v2 ] in
+      let cf_if = Cf_caseif (cond, cf_step, cf_ret) in
+      let bodys = coq_of_cf cf_if in
+      let hypr = coq_foralls [(i_name, coq_int); ("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (coq_apps bodys [h;q], (coq_apps s [i;h;q]))) in
+      funhq "tag_for" (Coq_forall (("S",typs), coq_impls [locals; hypr] (coq_apps s [v1;h;q])))
+
+      (* (!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
+        (forall i H Q,  
+            (If_ i <= v2       
+               Then Seq (F1 ;; S (i+1)) H Q))
+               Else Ret tt) H Q
+           -> S i H Q) 
+         -> S v1 H Q)  *)
+         (*--todo:optimize using rec calls *)
+     
+      (* DEPRECATED
       let s = Coq_var "S" in
       let i = Coq_var i_name in
       let typs = Coq_impl (coq_int,formula_type) in
@@ -192,20 +215,14 @@ let rec coqtops_of_imp_cf cf =
       let bodys = coq_conj ple pgt in
       let hypr = coq_foralls [(i_name, coq_int); ("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (bodys,(coq_apps s [i;h;q]))) in
       funhq "tag_for" (Coq_forall (("S",typs), coq_impls [locals; hypr] (coq_apps s [v1;h;q])))
-      (* (!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
-        (forall i H Q,  
-               ((i <= v2 -> !Seq (fun H Q => exists Q', Q1 H Q' /\ S (i+1) (Q' tt) Q) H Q))
-             /\ (i > v2 -> !Ret: (fun H Q => H ==> Q tt) H Q) )) 
-           -> S i H Q) 
-         -> S v1 H Q)  *)
-         (*--todo:optimize using rec calls *)
+      *)
 
   | Cf_while (cf1,cf2) -> 
       let r = Coq_var "R" in
       let typr = formula_type in
-      let cfseq = Cf_seq (cf2, Cf_manual r) in
-      let cfret = Cf_ret coq_tt in
-      let cfif = Cf_caseif (Coq_var "_c", cfseq, cfret) in
+      let cf_step = Cf_seq (cf2, Cf_manual r) in
+      let cf_ret = Cf_ret coq_tt in
+      let cfif = Cf_caseif (Coq_var "_c", cf_step, cf_ret) in
       let bodyr = coq_of_cf (Cf_let (("_c",coq_bool), cf1, cfif)) in
       let hypr = coq_foralls [("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (coq_apps bodyr [h;q],(coq_apps r [h;q]))) in
       let localr = Coq_app (Coq_var "CFML.CFHeaps.is_local", r) in

lib/coq/CFPrint.v

@@ -631,10 +631,11 @@ Notation "'LetIf' F0 'Then' F1 'Else' F2" :=
   (Let x := F0 in If_ x Then F1 Else F2)
   (at level 69, only parsing) : charac.
 
+(* DEPRECATED
 Notation "'IfProp' P 'Then' F1 'Else' F2" :=
   (!If (fun H Q => (P -> F1 H Q) /\ (~ P -> F2 H Q)))
   (at level 69, P at level 0) : charac.
-
+*)
 
 (********************************************************************)
 (** Case *)
@@ -786,8 +787,7 @@ Notation "'While' F1 'Do' F2 'Done_'" :=
 Notation "'For' i '=' a 'To' b 'Do' F1 'Done_'" :=
   (!For (fun H Q => forall S:int->~~unit, CFHeaps.is_local_pred S ->
         (forall i H Q,  
-             (i <= (b)%Z -> (F1 ;; S (i+1)) H Q)
-          /\ (i > b%Z -> (Ret tt) H Q) 
+             (If_ isTrue (i <= (b)%Z) Then (F1 ;; S (i+1)) Else (Ret tt)) H Q
           -> S i H Q)
        -> S a H Q))
   (at level 69, i ident, a at level 0, b at level 0) : charac.

lib/coq/CFTactics.v

@@ -2021,9 +2021,9 @@ Tactic Notation "xfail" "*" constr(C) :=
     [forall H' Q', (If_ F1 Then (Seq_ F2 ;; S) Else (Ret tt)) H' Q' -> S H' Q'].
 
     After [xwhile], the typical proof pattern is to generalize the goal
-    by calling [assert (forall X, S (I X) Q)] for some predicate [I], 
-    and then performing a well-founded induction on [X] w.r.t. wf relation.
-    (Or, using [xind_skip] to skip the termination proof.)
+    by calling [assert (forall X, S (Hof X) (Qof X)] for some predicate [Hof]
+    and [Qof] and then performing a well-founded induction on [X] w.r.t. wf 
+    relation. (Or, using [xind_skip] to skip the termination proof.)
 
     Alternatively, one can call one of the [xwhile_inv] tactics described 
     below to automatically set up the induction. The use of an invariant
@@ -2033,7 +2033,7 @@ Tactic Notation "xfail" "*" constr(C) :=
 
     - [xwhile] is the basic form, described above.
     
-    - [xwhile as S] is equivalent to [xwhile; intros S LR HS].
+    - [xwhile as S] is equivalent to [xwhile; intros S LS HS].
    
     - [xwhile_inv I R]  where [R] is a well-founded relation on
       type [A] and then invariant [I] has the form 
@@ -2183,118 +2183,146 @@ Tactic Notation "xwhile_inv_basic_skip" constr(I)  :=
 
 
 (*--------------------------------------------------------*)
-(* ** [xfor] 
+(* ** [xfor] *)
+
+(** [xfor] applies to a goal of the form [(For i = a To b Do F) H Q].
+    It introduces an abstract local predicate [S] such that [S i]
+    denotes the behavior of the loop starting from index [i]. 
+    The initial goal is [S a H Q]. An assumption is provided to unfold
+    the loop:
+    [forall i H' Q', 
+     (If_ i <= b Then (Seq_ F ;; S (i+1)) Else (Ret tt)) H' Q' -> S i H' Q'].
+
+    After [xfor], the typical proof pattern is to generalize the goal
+    by calling [assert (forall X i, i <= b -> S i (Hof i X) (Qof i X))], 
+    and then performing an induction on [i].
+    (Or, using [xind_skip] to skip the termination proof.)
+
+    Alternatively, one can call one of the [xfor_inv] tactics described 
+    below to automatically set up the induction. The use of an invariant
+    makes the proof simpler but 
+
+    Forms:
+
+    - [xfor] is the basic form, described above.
+    
+    - [xfor as S] is equivalent to [xwhile; intros S LS HS].
+
+    - [xfor_inv I] specializes the goal for the case [a <= b+1].
+      It requests to prove [H ==> I a] and [I (b+1) ==> Q], and 
+      [forall i, a <= i <= b, F (I i) (# I (i+1))] for iterations.
+      Note that the goal will not be provable if [a > b+1].
 
-(** TODO: document *)
+    - [xfor_inv_void] simplifies the goal in case the loops runs
+      no iteration, that is, when [a > b]. 
 
-Lemma for_loop_cf_to_inv : 
-   forall I H',
+    - [xfor_inv_case I] provides two sub goals, one for the case
+      [a > b] and one for the case [a <= b]. 
+*)
+
+
+Lemma xfor_inv_case_lemma : forall (I:int->hprop),
    forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop),
-   (a > (b)%Z -> H ==> (Q tt)) ->
-   (a <= (b)%Z ->
+   ((a <= b) -> exists H',
           (H ==> I a \* H') 
-       /\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) 
-       /\ (I ((b)%Z+1) \* H' ==> Q tt)) ->
+       /\ (forall i, a <= i <= b -> F i (I i) (# I(i+1))) 
+       /\ (I (b+1) \* H' ==> Q tt \* \GC)) ->
+   ((a > b) -> 
+          (H ==> Q tt \* \GC)) ->
   (For i = a To b Do F i Done_) H Q.
 Proof.
-(* TODO
   introv M1 M2. apply local_erase. intros S LS HS.
-  tests C: (a > b). 
-  apply (rm HS). split; intros C'. math. xret_no_gc~.
-  forwards (Ma&Mb&Mc): (rm M2). math.
+  tests: (a <= b).
+  { forwards (H'&(Ma&Mb&Mc)): (rm M1). math.
     cuts P: (forall i, a <= i <= b+1 -> S i (I i) (# I (b+1))).
-     xapply P. math. hchanges Ma. hchanges Mc.
-   intros i. induction_wf IH: (int_upto_wf (b+1)) i. intros Bnd.
-   applys (rm HS). split; intros C'.
-     xseq. eapply Mb. math. xapply IH; auto with maths; hsimpl.
-  xret_no_gc. math_rewrite~ (i = b +1).  
+    { xapply P. math. hchanges Ma. hchanges Mc. }
+    { intros i. induction_wf IH: (upto (b+1)) i. intros Hi.
+      applys (rm HS). xif.  
+      { xseq. applys Mb. math. xapply IH; auto with maths. xsimpl. }
+      { xret. math_rewrite (i = b +1). xsimpl. } } }
+  { applys (rm HS). xif. { math. } { xret. applys M2. math. } }
 Qed.
-*)
 
-Admitted.
+Lemma xfor_inv_lemma : forall (I:int->hprop),
+  forall (a:int) (b:int) (F:int->~~unit) H H',
+  (a <= b+1) ->
+  (H ==> I a \* H') ->
+  (forall i, a <= i <= b -> F i (I i) (# I(i+1))) -> 
+  (For i = a To b Do F i Done_) H (# I (b+1) \* H').
+Proof. 
+  introv ML MH MI. applys xfor_inv_case_lemma I; intros C.
+  { exists H'. splits~. xsimpl. }
+  { xchange MH. math_rewrite (a = b + 1). xsimpl. } 
+Qed.
 
-Lemma for_loop_cf_to_inv_gen' : 
-   forall I H',
+Lemma xfor_inv_void_lemma : 
   forall (a:int) (b:int) (F:int->~~unit) H,
-   (a <= (b)%Z ->
-          (H ==> I a \* H') 
-       /\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1)))) ->
-   (a > (b)%Z -> H ==> I ((b)%Z+1) \* H') ->
-  (For i = a To b Do F i Done_) H (# I ((b)%Z+1) \* H').
-Proof. intros. applys* for_loop_cf_to_inv. Qed.
-
-Lemma for_loop_cf_to_inv_gen : 
-   forall I H',
-   forall (a:int) (b:int) (F:int->~~unit) H Q,
-   (a <= (b)%Z -> H ==> I a \* H') ->
-   (forall i, a <= i <= (b)%Z -> F i (I i) (# I(i+1))) ->
-   (a > (b)%Z -> H ==> I ((b)%Z+1) \* H') ->  
-   (# (I ((b)%Z+1) \* H')) ===> Q ->
-  (For i = a To b Do F i Done_) H Q.
+  (a > b) ->
+  (For i = a To b Do F i Done_) H (# H).
 Proof. 
-  intros. applys* for_loop_cf_to_inv. intros C.
-  hchange (H2 C). hchange (H3 tt). hsimpl. 
+  introv ML.
+  applys xfor_inv_case_lemma (fun (i:int) => \[]); intros C.
+  { false. math. }
+  { xsimpl. } 
 Qed.
 
+Ltac xfor_ensure_evar_post cont :=
+  match cfml_postcondition_is_evar tt with
+  | true => cont tt
+  | false => xgc_post; [ cont tt | ]
+  end.
+
+Ltac xfor_pre cont :=
+  let aux tt := xuntag tag_for; cont tt in
+  match cfml_get_tag tt with
+  | tag_for => aux tt
+  | tag_seq => xseq; [ aux tt | instantiate; try xextract ]
+  end.
 
-Lemma for_loop_cf_to_inv_up : 
-   forall I H',
-   forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop),
-   (a <= (b)%Z) ->
-   (H ==> I a \* H') ->
-   (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) ->
-   ((# I ((b)%Z+1) \* H') ===> Q) ->
-   (For i = a To b Do F i Done_) H Q.
-Proof. intros. applys* for_loop_cf_to_inv. intros. math. Qed.
+Ltac xfor_pre_ensure_evar_post cont :=
+  xfor_pre ltac:(fun _ => 
+    xfor_ensure_evar_post ltac:(fun _ => cont tt)).
+
+Tactic Notation "xfor" :=  
+  xfor_pre ltac:(fun _ => apply local_erase).
 
-Ltac xfor_intros tt :=
-  let S := fresh "S" in let LS := fresh "L" S in
+Tactic Notation "xfor" "as" ident(S) :=  
+  xfor_pre ltac:(fun _ => 
+    let LS := fresh "L" S in
     let HS := fresh "H" S in 
-  apply local_erase; intros S LS HS.
+    apply local_erase;
+    intros S LS HS).
 
-Ltac xfor_pre cont :=
-  xextract_check_not_needed tt;
+Ltac xfor_inv_case_check_post_instantiated tt :=
+  lazymatch cfml_postcondition_is_evar tt with
+  | true => fail 2 "xfor_inv_case requires a post-condition; use [xpost Q] to set it, or [xseq Q] if the loop is behind a Seq."
+  | false => idtac
+  end.
+
+Ltac xfor_inv_case_core I :=
   match cfml_get_tag tt with
-  | tag_seq => xseq; [ cont tt | ]
-  | tag_for => cont tt
+  | tag_seq => 
+       fail 1 "xfor_inv_case requires a post-condition; use [xseq Q] to assign it."
+  | tag_for => 
+       xfor_inv_case_check_post_instantiated tt;
+       xfor_pre ltac:(fun _ => apply (@xfor_inv_case_lemma I)) 
   end.
 
-Tactic Notation "xfor" :=
-  xfor_pre ltac:(fun _ => xfor_intros tt).
-Tactic Notation "xfor" constr(E) :=
-  xfor_pre ltac:(fun _ => xfor_intros tt; xgeneralize E).
-
-
-(** TODO: document *)
-
-Ltac xfor_inv_gen_base I i C :=
-  eapply (@for_loop_cf_to_inv_gen I); 
-  [ intros C
-  | intros i C
-  | intros C
-  | apply rel_le_refl ].
-
-Tactic Notation "xfor_inv_gen" constr(I) "as" ident(i) ident(C) :=
-  xfor_inv_gen_base I i C.
-Tactic Notation "xfor_inv_gen" constr(I) "as" ident(i) :=
-  let C := fresh "C" i in xfor_inv_gen I as i C.
-Tactic Notation "xfor_inv_gen" constr(I) :=
-  let i := fresh "i" in xfor_inv_gen I as i.
-
-Ltac xfor_inv_base I i C :=
-  eapply (@for_loop_cf_to_inv_up I); 
-  [ 
-  | 
-  | intros i C
-  | apply rel_le_refl ].
-
-Tactic Notation "xfor_inv" constr(I) "as" ident(i) ident(C) :=
-  xfor_inv_gen_base I i C.
-Tactic Notation "xfor_inv" constr(I) "as" ident(i) :=
-  let C := fresh "C" i in xfor_inv I as i C.
+Tactic Notation "xfor_inv_case" constr(I) :=
+  xfor_inv_case_core I.
+
+Ltac xfor_inv_core I :=
+  xfor_pre_ensure_evar_post ltac:(fun _ => apply (@xfor_inv_lemma I)).
+
 Tactic Notation "xfor_inv" constr(I) :=
-  let i := fresh "i" in xfor_inv I as i.
-*)
+  xfor_inv_core I.
+
+Ltac xfor_inv_void_core tt :=
+  xfor_pre_ensure_evar_post ltac:(fun _ => apply (@xfor_inv_void_lemma)).
+
+Tactic Notation "xfor_inv_void" :=
+  xfor_inv_void_core tt.
+
 
 
 (********************************************************************)