refine FIXME items a bit

kth-step · Jan 23, 2024 · 992abd7 · 992abd7
1 parent 7187461
commit 992abd7
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 7 deletions.
diff --git a/src/abs.ott b/src/abs.ott
@@ -64,7 +64,7 @@ e :: e_ ::=
   | fn ( e1 , ... , en ) :: :: fn_call
     {{ com function call }}
   | e [ x1 |-> y1 , ... , xn |-> yn ] :: M :: subst_var
-    {{ coq ([[e]]) }} % FIXME
+    {{ coq (my_subst [[e]] [[x1 |-> y1 ... xn |-> yn]]) }} % FIXME
 
 sig :: sig_ ::=
      | T1 , ... , Tn -> T :: :: sig
@@ -107,7 +107,13 @@ formula :: formula_ ::=
   | G ( fn ) = sig :: M :: G_fn_eq_sig
     {{ coq (Map.find [[fn]] [[G]] = Some (ctxv_sig [[sig]])) }}
   | fresh ( x1 , ... , xn , e ) :: M :: fresh
-    {{ coq True }} % FIXME
+    {{ coq (my_fresh [[x1 ... xn]] [[e]]) }} % FIXME
+
+embed
+{{ coq
+Definition my_subst (e5:e) (l:list (x*x)) := e5. (* FIXME *)
+Definition my_fresh (l : list x) (e5 : e) := True. (* FIXME *)
+}}
 
 defns
   expression_well_typing :: typ_ ::=

diff --git a/theories/abs_defs.v b/theories/abs_defs.v
@@ -98,6 +98,9 @@ Fixpoint e_ott_ind (n:e) : P_e n :=
 end.
 
 End e_rect.
+Definition my_subst (e5:e) (l:list (x*x)) := e5.
+Definition my_fresh (l : list x) (e5 : e) := True.
+
 (** definitions *)
 
 (* defns expression_well_typing *)
@@ -132,7 +135,7 @@ Inductive red_e : list F -> s -> e -> s -> e -> Prop :=    (* defn e *)
      red_e F_list s5 e_5 s' e' ->
      red_e F_list s5 (e_fn_call fn5 ((app e_list (app (cons e_5 nil) (app e'_list nil))))) s' (e_fn_call fn5 ((app e_list (app (cons e' nil) (app e'_list nil)))))
  | red_fun_ground : forall (T_x_t_y_list:list (T*x*t*x)) (F'_list F_list:list F) (T_5:T) (fn5:fn) (e5:e) (s5:s),
-      True  ->
-     red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list))  (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5)  s5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) )   ( e5 ) .
+      (my_fresh  (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list)   e5 )  ->
+     red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list))  (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5)  s5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) )   (my_subst  e5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (x_,y_) end ) T_x_t_y_list) ) .
 
 
diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v
@@ -15,12 +15,12 @@ Definition G_vdash_s (G5 : G) (s5 : s) :=
   Map.find x5 G5 = Some (ctxv_T T5) ->
   typ_e G5 (e_t t5) T5.
 
-Lemma type_preservation : forall (G5 : G) (s5 : s), 
+Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s),
+  (* FIXME: add well-typing of all function definitions here *)
   G_vdash_s G5 s5 ->
-  forall (Flist : list F) (e5 : e) (T5 : T) (s' : s) (e' : e),
+  forall (e5 : e) (T5 : T) (s' : s) (e' : e),
     typ_e G5 e5 T5 ->
     red_e Flist s5 e5 s' e' ->
     exists G', subG G5 G' /\ G_vdash_s G' s' /\ typ_e G' e' T5.
 Proof.
 Admitted.
-