examples complete

attic/ModelExtra.v

@@ -651,3 +651,50 @@ Proof using.
 
 Abort.
 
+
+
+
+
+
+(*------------------------------------------------------------------*)
+(* ** Specialize version of [cf_fix] for small arities *)
+
+Definition cf_fix0 (F1of : val -> formula) 
+                   (F2of : val -> formula) : formula := fun H Q =>
+  forall (F:val), 
+  (F1of F ===> app F nil) -> 
+  (F2of F) H Q.
+
+Definition cf_fix1 (F1of : val -> val -> formula) 
+                  (F2of : val -> formula) : formula := fun H Q =>
+  forall (F:val), 
+  (forall X1, (F1of F X1) ===> app F [X1]) -> 
+  (F2of F) H Q.
+
+(* LATER
+Definition cf_fix2 (F1of : val -> val -> val -> formula) 
+                  (F2of : val -> formula) : formula := fun H Q =>
+  forall (F:val), 
+  (forall X1 X2, (F1of F X1 X2) ===> app F [X1;X2]) -> 
+  (F2of F) H Q.
+*)
+
+Lemma cf_fix_specialize_0 : forall (F1of : val -> formula) (F2of : val -> formula),
+  cf_fix0 F1of F2of ===>
+  cf_fix 0 F1of F2of
+
+cf_fix0 (fun F => let E := List.combine (f::nil) (F::nil) in cf (subst_Trm E t1))  
+
+
+      let G := match xs with
+        | nil => 
+        | x::nil => cf_fix1 (fun F X => let E := List.combine (f::x::nil) (F::X::nil) in cf (subst_Trm E t1))
+        | xs => cf_fix (List.length xs) (fun F Xs => let E := List.combine (f::xs) (F::Xs) in cf (subst_Trm E t1))
+
+
+Definition cf_fix (n:nat) (F1of : val -> vals -> formula) 
+                  (F2of : val -> formula) : formula := fun H Q =>
+Definition cf_fix0 (F1of : val -> formula) 
+                   (F2of : val -> formula) : formula := fun H Q =>
+
+

model/MLCFLifted.v

@@ -21,8 +21,6 @@ Open Scope charac.
 Ltac auto_star ::= jauto.
 
 
-
-
 (********************************************************************)
 (* CF with Lifting *)
 
@@ -445,6 +443,7 @@ Tactic Notation "xfail" :=
 (********************************************************************)
 (* * Even number axiomatization for demos *)
 
+(* LATER
 Fixpoint even_nat (n:nat) :=
   match n with
   | O => true 
@@ -455,12 +454,13 @@ Definition even (n:Z) := even_nat (Z.to_nat n).
 
 Lemma even_minus_two : forall n, even n -> even (n - 2).
 Admitted.
-
+*)
 
 
 (********************************************************************)
 (* * Himpl demos *)
 
+(* LATER
 Lemma hsimpl_demo_1 : forall r,
   (r ~~~> 6) ==>
   (Hexists (n:int), (r ~~~> n) \* \[even n]).
@@ -478,6 +478,7 @@ Proof using.
   applys even_minus_two. auto.
 Qed.
 
+*)
 
 
 

model/LambdaExamples.v → model/MLExamples.v

@@ -196,14 +196,45 @@ Qed.
 
 End ProofWithTriples.
 
+(********************************************************************)
+(* * Mutable list increment verification, using characteristic formulae, 
+     without tactics. *)
+
+(** Observe how, in the proof below, the deep embedding is never revealed. *)
+
+Lemma mlist_incr_spec' : forall L p, 
+  app mlist_length [val_loc p]
+    (p ~> MList L)
+    (fun r => \[r = val_int (length L)] \* p ~> MList L).
+Proof using.
+  intros L. induction_wf: list_sub_wf L. intros p. 
+  applys cf_sound_app1 20%nat. reflexivity.
+  simpl; fold mlist_length.
+  applys local_erase. esplit. split. 
+  { applys local_erase. xapplys rule_neq. }
+  intros X. xpull. intros EX.
+  subst X. applys local_erase.
+  split; intros C; case_if as C'; clear C.
+  { xchange (MList_not_null p). { auto. } 
+    xpull. intros x p' L' EL.
+    applys local_erase. esplit. split.
+    { applys local_erase. xapplys rule_get_tl. }
+    intros p''. xpull. intros E. subst p''.
+    applys local_erase. esplit. split.
+    { applys local_erase. xapplys IH. { subst~. } }
+    { intros r. xpull. intros Er. xchange (MList_uncons p). 
+      subst r. applys local_erase. xapplys rule_add.
+      subst. rew_length. fequals. math. } }  
+  { applys local_erase. unfolds. inverts C'. xchange MList_null_keep.  
+    hpull. intros EL. hsimpl. subst~. }
+Qed.
+
 
 (********************************************************************)
 (* * Mutable list increment verification, using characteristic formulae *)
 
 (** Remark: in Ltac script below, "=>" is an alias for "intros" *)
 
-(** Observe how, in the proof below, the deep embedding is never revealed. *)
-
 Lemma mlist_incr_spec' : forall L p, 
   app mlist_length [val_loc p]
     (p ~> MList L)

model/Makefile

@@ -15,9 +15,9 @@ include $(CFML)/Makefile.common
 SRC := $(shell cat FILES)
 
 ifeq ($(ARTHUR),1)
-	# LibState SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits LambdaExamples
+	# LibState SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits
 	# LambdaExamples
-	SRC := LibState SepFunctor MLSemantics MLSep MLSepLifted MLCF MLCFLifted
+	SRC := LibState SepFunctor MLSemantics MLSep MLSepLifted MLCF MLCFLifted MLExamples
 endif
 
 PWD := $(shell pwd)

model/export.sh

@@ -38,7 +38,7 @@ mkdir $ARCHIVE/TLC
 echo "Copying CFML/model..."
 mkdir $ARCHIVE/model
 if [ ! -z ${ARTHUR+x} ]; then
-  FILES="LibState SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits LambdaExamples MLSemantics MLSep MLSepLifted MLCF MLCFLifted"
+  FILES="LibState SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits MLSemantics MLSep MLSepLifted MLCF MLCFLifted MLExamples"
   # LambdaCFComplete
 else
   FILES=`grep -v -e "^ *#" FILES` ;