partialapps

lib/coq/CFSpec.v

@@ -184,6 +184,33 @@ 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 xs n 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]).
+Proof using.
+(* 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.
+
 
 
 
@@ -192,6 +219,16 @@ Qed.
 
 
 
+(********************************************************************)
+(* ** CF GENERATOR *)
+
+(* Characteristic formula for "f x y z" is "App f [x y z]".
+ 
+   Hypothesis for function declaration "let f x y z = t" is:
+   "curried 3 f /\ (forall x y z H Q, CF(t) H Q -> App f [x y z] H Q)"
+
+*)
+
 
 
 
@@ -205,6 +242,11 @@ Qed.
 
 
 
+(********************************************************************)
+(********************************************************************)
+(********************************************************************)
+(********************************************************************)
+(* DEPRECATED *)