Type preservation

_CoqProject

@@ -4,3 +4,4 @@
 
 theories/abs_defs.v
 theories/abs_functional_metatheory.v
+theories/utils.v

src/abs.ott

@@ -108,32 +108,30 @@ formula :: formula_ ::=
     {{ coq (Map.find [[x]] [[s]] = Some ([[t]])) }}
   | G ( fn ) = sig :: M :: G_fn_eq_sig
     {{ coq (Map.find [[fn]] [[G]] = Some (ctxv_sig [[sig]])) }}
-  | fresh ( x1 , ... , xn , e ) :: M :: fresh
+  | fresh ( x1 , ... , xn , e ) :: M :: fresh_e
     {{ coq (fresh_vars_e [[x1 ... xn]] [[e]]) }}
+  | fresh ( x1 , ... , xn , s ) :: M :: fresh_s
+    {{ coq (fresh_vars_s [[x1 ... xn]] [[s]]) }}
+  | fresh ( x1 , ... , xn , e , s ) :: M :: fresh
+    {{ coq (fresh_vars [[x1 ... xn]] [[e]] [[s]]) }}
+  | well_formed ( x1 , ... , xn , e , s ) :: M :: well_formed
+    {{ coq (well_formed [[e]] [[s]] [[x1 ... xn]]) }}
 
 embed
 {{ coq
-Fixpoint get_val (k:x) (l:list(x*x)): option x :=
-  match l with
-  | nil => None
-  | (k', v) :: l' =>
-      match eq_x k k' with
-      | left _ => Some v
-      | _ => get_val k l'
-      end
-  end.
+Equations e_var_subst_one (e5:e) (x_ y_: x) : e := {
+ e_var_subst_one (e_t t) _ _ := e_t t;
+ e_var_subst_one (e_var x0) x_ y_ := if (eq_x x0 x_) then (e_var y_) else (e_var x0);
+ e_var_subst_one (e_fn_call fn0 arg_list) x_ y_ := e_fn_call fn0 (e_list_subst_one arg_list x_ y_) }
+where e_list_subst_one (es:list e) (x_ y_: x) : list e := {
+ e_list_subst_one nil _ _ := nil;
+ e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_
+}.
 
-Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e :=
-  match e5 with
-  | e_t t => e_t t
-  | e_var x =>
-      match get_val x l with
-              | None => e_var x
-              | Some y => e_var y
-              end
-  | e_fn_call fn e_list =>
-      e_fn_call fn (map (fun e => e_var_subst e l) e_list)
-  end.
+(* I would prefer not doing this, but sometimes I need it to compute *)
+Global Transparent e_var_subst_one.
+
+Definition e_var_subst (e5:e) (l:list (x*x)) : e := fold_right (fun '(x', y') e' => e_var_subst_one e' x' y') e5 l.
 
 Equations fresh_vars_e (l : list x) (e0 : e) : Prop := {
  fresh_vars_e _ (e_t _) := True;
@@ -142,6 +140,24 @@ Equations fresh_vars_e (l : list x) (e0 : e) : Prop := {
 where fresh_vars_el (l : list x) (el0 : list e) : Prop := {
  fresh_vars_el l nil := True;
  fresh_vars_el l (e1::el0) := fresh_vars_e l e1 /\ fresh_vars_el l el0 }.
+
+Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop :=
+  match l with
+  | nil => True
+  | (y::ys) => ~ Map.In y s0 /\ fresh_vars_s ys s0
+  end.
+
+Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop :=
+  fresh_vars_s l s0 /\ fresh_vars_e l e0.
+
+Inductive distinct: list x -> Prop :=
+ | distinct_nil: distinct nil
+ | distinct_cons: forall y ys,
+      ~ In y ys ->
+     distinct ys ->
+     distinct (y::ys).
+
+Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l.
 }}
 
 defns
@@ -193,6 +209,6 @@ defn
   ------------------------------------------------------------------------------------------------------------- :: fun_exp
   F1 ... Fn , s |- fn ( e1 , ... , ei , e , e'1 , ... , e'j ) ~> s' |- fn ( e1 , ... , ei , e' , e'1 , ... , e'j )
 
-  fresh ( y1 , ... , yn , e )
+  well_formed (y1 , ... , yn , e, s)
   ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: fun_ground
   F1 ... Fi def T fn ( T1 x1 , ... , Tn xn ) = e ; F'1 ... F'j , s |- fn ( t1 , ... , tn ) ~> s [ y1 |-> t1 , ... , yn |-> tn ] |- e [ x1 |-> y1 , ... , xn |-> yn ]

theories/abs_defs.v

@@ -100,27 +100,19 @@ Fixpoint e_ott_ind (n:e) : P_e n :=
 end.
 
 End e_rect.
-Fixpoint get_val (k:x) (l:list(x*x)): option x :=
-  match l with
-  | nil => None
-  | (k', v) :: l' =>
-      match eq_x k k' with
-      | left _ => Some v
-      | _ => get_val k l'
-      end
-  end.
+Equations e_var_subst_one (e5:e) (x_ y_: x) : e := {
+ e_var_subst_one (e_t t) _ _ := e_t t;
+ e_var_subst_one (e_var x0) x_ y_ := if (eq_x x0 x_) then (e_var y_) else (e_var x0);
+ e_var_subst_one (e_fn_call fn0 arg_list) x_ y_ := e_fn_call fn0 (e_list_subst_one arg_list x_ y_) }
+where e_list_subst_one (es:list e) (x_ y_: x) : list e := {
+ e_list_subst_one nil _ _ := nil;
+ e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_
+}.
 
-Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e :=
-  match e5 with
-  | e_t t => e_t t
-  | e_var x =>
-      match get_val x l with
-              | None => e_var x
-              | Some y => e_var y
-              end
-  | e_fn_call fn e_list =>
-      e_fn_call fn (map (fun e => e_var_subst e l) e_list)
-  end.
+(* I would prefer not doing this, but sometimes I need it to compute *)
+Global Transparent e_var_subst_one.
+
+Definition e_var_subst (e5:e) (l:list (x*x)) : e := fold_right (fun '(x', y') e' => e_var_subst_one e' x' y') e5 l.
 
 Equations fresh_vars_e (l : list x) (e0 : e) : Prop := {
  fresh_vars_e _ (e_t _) := True;
@@ -130,6 +122,24 @@ where fresh_vars_el (l : list x) (el0 : list e) : Prop := {
  fresh_vars_el l nil := True;
  fresh_vars_el l (e1::el0) := fresh_vars_e l e1 /\ fresh_vars_el l el0 }.
 
+Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop :=
+  match l with
+  | nil => True
+  | (y::ys) => ~ Map.In y s0 /\ fresh_vars_s ys s0
+  end.
+
+Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop :=
+  fresh_vars_s l s0 /\ fresh_vars_e l e0.
+
+Inductive distinct: list x -> Prop :=
+ | distinct_nil: distinct nil
+ | distinct_cons: forall y ys,
+      ~ In y ys ->
+     distinct ys ->
+     distinct (y::ys).
+
+Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l.
+
 (** definitions *)
 
 (* defns expression_well_typing *)
@@ -164,7 +174,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),
-      (fresh_vars_e  (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list)   e5 )  ->
+      (well_formed  e5   s5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) )  ->
      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) )   (e_var_subst  e5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (x_,y_) end ) T_x_t_y_list) ) .