app_partial

lib/coq/CFSpec.v

@@ -6,6 +6,20 @@ Open Local Scope heap_scope_advanced.
 Hint Extern 1 (_ ===> _) => apply rel_le_refl.
 
 
+Lemma local_weaken_post : forall B Q' (F:~~B) H Q,
+  is_local F -> 
+  F H Q' -> 
+  Q' ===> Q -> 
+  F H Q.
+Proof using. intros. apply* local_weaken. Qed.
+
+Lemma local_prove : forall B (F:~~B),  
+  (forall H Q, F H Q = local F H Q) -> is_local F.
+Proof using.
+  intros. unfold is_local. apply func_ext_2. applys H.
+Qed.
+
+
 (********************************************************************)
 (* ** Axioms of CFML *)
 
@@ -76,9 +90,9 @@ Admitted. (* faster *)
 (*
 Qed.
 
-
-Hint Resolve app_basic_local.
 *)
+Hint Resolve app_basic_local.
+
 
 (** AppReturns with frame -- TODO: needed?
 
@@ -92,6 +106,8 @@ Proof using. intros. applys* local_wframe. Qed.
 (********************************************************************)
 (* ** Generic notation for list of args *)
 
+Notation "'Dyn' x" := (@dyn _ x)  (at level 0).
+
 Notation "[ x1 ]" := ((dyn x1)::nil)
   (at level 0, x1 at level 00) : arglist.
 Notation "[ x1 x2 ]" := ((dyn x1)::(dyn x2)::nil)
@@ -103,7 +119,7 @@ Delimit Scope arglist with arglist.
 
 
 (********************************************************************)
-(* ** Definition of [App]  *)
+(* ** Definition of [App] and properties *)
 
 Fixpoint AppDef (f:func) (xs:list dynamic) B (H:hprop) (Q:B->hprop) : Prop :=
   match xs with
@@ -123,6 +139,40 @@ Definition demo_arglist :=
   forall f (xs:list int) (x y:int) B H (Q:B->hprop),
   App f [ x y ] H Q.
 
+Lemma App_ge_2_unfold : 
+  forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
+  (xs <> nil) ->
+    App f ((dyn x)::xs) H Q 
+  = app_basic f x H
+       (fun g => Hexists H', H' \* \[ AppDef g xs H' Q]).
+Proof using. 
+  intros. destruct xs. false. auto.
+Qed.
+
+Lemma App_ge_2_unfold' : 
+  forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
+  (length xs >= 1)%nat ->
+    App f ((dyn x)::xs) H Q 
+  = app_basic f x H
+       (fun g => Hexists H', H' \* \[ AppDef g xs H' Q]).
+Proof using. 
+  intros. rewrite~ App_ge_2_unfold. destruct xs; rew_list in *.
+  math.
+  introv N. false.
+Qed.
+
+Lemma App_weaken : forall B f xs H (Q Q':B->hprop),  
+  App f xs H Q ->
+  Q ===> Q' -> 
+  App f xs H Q'.
+Proof using.
+  intros B f xs. gen f. induction xs as [|[A x] xs]; introv M W. false.
+  tests E: (xs = nil).
+    simpls. applys~ local_weaken_post M.
+    rewrite~ App_ge_2_unfold'. rewrite~ App_ge_2_unfold' in M.
+     applys~ local_weaken_post M. intros g. hsimpl. rew_heap. applys* IHxs. 
+Qed.
+
 
 (********************************************************************)
 (* ** Definition of [curried]  *)
@@ -133,25 +183,27 @@ Fixpoint curried (n:nat) (f:func) : Prop :=
   | S O => True
   | S n => forall A (x:A),
      app_basic f x \[]
-       (fun g => \[ curried n g /\ forall xs B H (Q:B->hprop),
-          App f ((dyn x)::xs) H Q -> App g xs H Q])
+       (fun g => \[ curried n g
+          /\ forall xs B H (Q:B->hprop), length xs = n ->
+               App f ((dyn x)::xs) H Q -> App g xs H Q])
   end.
 
+Lemma curried_ge_2_unfold : forall n f,
+  (n > 1)%nat -> 
+    curried n f
+  = forall A (x:A), app_basic f x \[]
+    (fun g => \[    curried (pred n) g 
+                 /\ forall xs B H (Q:B->hprop), length xs = (pred n) ->
+                       App f ((dyn x)::xs) H Q -> App g xs H Q]).
+Proof using.
+  introv N. destruct n. math. destruct n. math. auto.
+Qed.
+
 
 (********************************************************************)
 (* ** Lemma for over-applications *)
 
-Lemma App_hd_nonnil_unfold : 
-  forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
-  (length xs >= 1)%nat ->
-  App f ((dyn x)::xs) H Q = 
-     app_basic f x H
-       (fun g => Hexists H', H' \* \[ AppDef g xs H' Q]).
-Proof using. 
-  intros. destruct xs. rew_list in *. math. auto.
-Qed.
-
-Lemma App_over : forall xs ys f B H (Q:B->hprop), 
+Lemma App_over_app : forall xs ys f B H (Q:B->hprop), 
   (length xs > 0)%nat -> (length ys > 0)%nat ->
     App f (xs++ys) H Q 
   = App f xs H (fun g => Hexists H', H' \*
@@ -161,14 +213,14 @@ Proof using.
   destruct a as [A x].
   destruct xs.
     rew_list. simpl. destruct ys. rew_list in *. math. auto.
-  sets_eq xs': (d :: xs). do 2 (rewrite App_hd_nonnil_unfold; 
-   [ | subst; rew_list; math ]).
+  sets_eq xs': (d :: xs). do 2 (rewrite App_ge_2_unfold;
+   [ | subst; rew_list; auto_false ]).
   fequal. apply func_ext_1. intros g. 
   apply func_equal_1. auto. apply func_ext_1. intros H'.
   fequal. fequal. apply IHxs. subst. rew_list. math. math.
 Qed. 
 
-Lemma App_over' : forall n xs f B H (Q:B->hprop), 
+Lemma App_over_take : forall n xs f B H (Q:B->hprop), 
   (0 < n < length xs)%nat ->
     App f xs H Q 
   = App f (take n xs) H (fun g => Hexists H', H' \*
@@ -177,59 +229,61 @@ Proof using.
   introv N.
   forwards* (M&E1&E2): take_and_drop n xs. math.
   set (xs' := xs) at 1. change xs with xs' in M. rewrite M.
-  subst xs'. rewrite App_over; try math. auto.
+  subst xs'. rewrite App_over_app; try math. auto.
 Qed.
 
 
 (********************************************************************)
 (* ** Lemma for partial-applications *)
 
-Lemma curried_ge_2_unfold : forall n f A (x:A),
-  curried n f -> (n > 1)%nat -> 
-  app_basic f x \[]
-    (fun g => \[ curried (pred n) g /\ forall xs B H (Q:B->hprop),
-                 App f ((dyn x)::xs) H Q -> App g xs H Q]).
-Proof using.
-  introv C N. destruct n. math. destruct n. math.
-  specializes C x. simpl pred. apply C.
-Qed.
-
 Lemma App_partial : forall n xs f,
   curried n f -> (0 < length xs < n)%nat ->
-  App f xs \[] (fun g => \[ forall ys B H (Q:B->hprop),
-    App f (xs++ys) H Q -> App g ys H Q]).
+  App f xs \[] (fun g => \[ 
+    curried (n - length xs)%nat g /\
+    forall ys B H (Q:B->hprop), (length xs + length ys = n)%nat ->
+      App f (xs++ys) H Q -> App g ys H Q]).
 Proof using.
-(* TODO.
-  induction n. math. introv C N.
-  destruct xs as [|[A x] xs']. rew_list in N. math.
-  destruct n as [|n]. math.
-  lets: C x.
-  destruct xs' as [|[A' x'] xs''].
-  simpl. applys_eq H 1. apply func_ext_1.
-   intros g. fequal. 
+  intros n. induction_wf IH: lt_wf n. introv C N.
+  destruct xs as [|[A x] zs]. rew_list in N. math.
+  rewrite curried_ge_2_unfold in C; [|math]. 
+  tests E: (zs = nil).
+  { unfold AppDef at 1. eapply local_weaken_post. auto. applys (rm C).
+    intros g. hextract as [M1 M2]. hsimpl. split. 
+      rew_list. applys_eq M1 2. math.
+      introv E AK. rew_list in *. applys M2. math. auto. }
+  { asserts Pzs: (0 < length zs). { destruct zs. tryfalse. rew_list. math. }
+    rew_list in N.
+    rewrite~ App_ge_2_unfold'.
+    eapply local_weaken_post. auto. applys (rm C). clear C. (* todo: make work rm *)
+    intros h. hextract as [M1 M2]. hsimpl.
+    applys App_weaken. applys (rm IH) M1. math. math. clear IH.
+    intros g. hextract as [N1 N2]. hsimpl. split. 
+    { rew_list. applys_eq N1 2. math. }
+    { introv P1 P2. rew_list in P1. 
+      applys N2. math.
+      applys M2. rew_list; math.
+      rew_list in P2. applys P2. }
+Qed.
 
 
-  simpl.
- 
- rew_list in N. math.
 
 
-*)
-  
-(* TODO...
 
-  induction xs; introv C E. rew_list in E. math.
-  destruct a as [A x].
-  forwards M: curried_ge_2_unfold x C. math.
-  destruct xs.
-    simpl. aply M.
-*)
-   
-  
-Abort.
+(********************************************************************)
 
+(*
 
 
+Lemma App_local : forall f xs B,
+  xs <> nil -> is_local (AppDef f xs (B:=B)).
+Proof using.
+  introv N. apply local_prove. intros H Q.
+  destruct xs as [|[A1 x1] xs]; tryfalse.
+  destruct xs as [|[A2 x2] xs].
+    simpl. rewrite~ <- app_basic_local.
+    rewrite App_ge_2_unfold. rewrite app_basic_local.
+   apply func_equal_1.
+*)