overapps

lib/coq/CFSpec.v

@@ -72,7 +72,7 @@ Proof using.
       do 2 rewrite <- heap_union_assoc. fequal.
       rewrite heap_union_comm. rewrite~ <- heap_union_assoc. rew_disjoint*.
 *)
-Admitted.
+Admitted. (* faster *)
 (*
 Qed.
 
@@ -90,7 +90,143 @@ Proof using. intros. applys* local_wframe. Qed.
 
 
 (********************************************************************)
-(* ** Generic of [app N]  *)
+(* ** Generic notation for list of args *)
+
+Notation "[ x1 ]" := ((dyn x1)::nil)
+  (at level 0, x1 at level 00) : arglist.
+Notation "[ x1 x2 ]" := ((dyn x1)::(dyn x2)::nil)
+  (at level 0, x1 at level 0, x2 at level 0) : arglist.
+Notation "[ x1 x2 x3 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::nil)
+  (at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : arglist.
+
+Delimit Scope arglist with arglist.
+
+
+(********************************************************************)
+(* ** Definition of [App]  *)
+
+Fixpoint AppDef (f:func) (xs:list dynamic) B (H:hprop) (Q:B->hprop) : Prop :=
+  match xs with
+  | nil => False
+  | (dyn x)::nil => app_basic f x H Q
+  | (dyn x)::xs => 
+     app_basic f x H
+       (fun g => Hexists H', H' \* \[ AppDef g xs H' Q])
+  end.
+
+Notation "'App' f xs" :=
+  (@AppDef f (xs)%arglist _)
+  (at level 68, f at level 0, xs at level 0) : charac.
+Open Scope charac.
+
+Definition demo_arglist := 
+  forall f (xs:list int) (x y:int) B H (Q:B->hprop),
+  App f [ x y ] H Q.
+
+
+(********************************************************************)
+(* ** Definition of [curried]  *)
+
+Fixpoint curried (n:nat) (f:func) : Prop :=
+  match n with
+  | O => False
+  | 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])
+  end.
+
+
+(********************************************************************)
+(* ** 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), 
+  (length xs > 0)%nat -> (length ys > 0)%nat ->
+    App f (xs++ys) H Q 
+  = App f xs H (fun g => Hexists H', H' \*
+                                   \[ App g ys H' Q ]).
+Proof using.
+  induction xs. rew_list. math. introv N1 N2. rew_list.
+  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 ]).
+  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), 
+  (0 < n < length xs)%nat ->
+    App f xs H Q 
+  = App f (take n xs) H (fun g => Hexists H', H' \*
+                                   \[ App g (drop n xs) H' Q ]).
+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.
+Qed.
+
+
+(********************************************************************)
+(* ** Lemma for partial-applications *)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+(* bug...
+Axiom App : forall (f:func) (xs:list dynamic) B (H:hprop) (Q:B->hprop), Prop.
+Implicit Arguments App [[B]].
+Print App.
+Arguments App f%heap_scope xs%arglist H%heap_scope Q%heap_scope.
+*)
+
+
+(* TODO: why not
+  Coercion id (P:Prop) : hprop := \[P].
+  Error: Sortclass cannot be a source class.
+*)
+
+
+
+
+
+
+(*
 
 Inductive arglist : nat -> Type :=
   | arglist_nil : arglist 0
@@ -104,7 +240,7 @@ Fixpoint app (n : nat) (X : arglist n) (f:func) (B:Type) (H:hprop) (Q:B->hprop)
      app_basic f x H
        (fun g : func => Hexists H', H' \* \[ app xs g H' Q])
   end.
-
+*)
 
 
 (* [app n xs f B H Q]
@@ -119,7 +255,7 @@ Definition app
 Proof.
   induction 1; intros f B H Q.
   (* exact (H ==> Q f). *)
-  exact True.
+  exact True. 
   exact (app_basic f x H (fun g => Hexists H', H' \* \[
       IHX g B H' Q])).
 Defined.