Skip to content

Commit

Permalink
Type preservation (#11)
Browse files Browse the repository at this point in the history 
* All but the function base case. very much WIP

* Factoring out list utilities

* Some cleanup and minor progress

* Some reorganizing, but not much progress

* Almost there with type preservation, tho still missing the actual type (substitution lemma)

* add coq-stdpp as dependency, add abs_examples module

* Some more lemmas – still stuck

* Typing examples

* nits

* Cleanup Proof with...

* All but the function base case. very much WIP

* Factoring out list utilities

* Some cleanup and minor progress

* Some reorganizing, but not much progress

* Almost there with type preservation, tho still missing the actual type (substitution lemma)

* Some more lemmas – still stuck

* Cleanup Proof with...

* Qed! (Kinda)

---------

Co-authored-by: Karl Palmskog <palmskog@gmail.com>
  • Loading branch information
@Aqissiaq @palmskog
Aqissiaq and palmskog authored Mar 14, 2024
1 parent 11c8549 commit 8055c81
Show file tree
Hide file tree
Showing 6 changed files with 1,414 additions and 51 deletions.
1 change: 1 addition & 0 deletions _CoqProject
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,4 @@
theories/abs_defs.v
theories/abs_examples.v
theories/abs_functional_metatheory.v
theories/utils.v
60 changes: 38 additions & 22 deletions src/abs.ott
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,32 +108,35 @@ 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
| distinct ( x1 , ... , xn ) :: M :: distinct_vars
{{ coq (NoDup [[x1 ... xn]]) }}
| 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]]) }}
| disjoint ( ( x1 , ... , xi ) , ( y1 , ... , yj ) ) :: M :: disjoint
{{ coq (disjoint [[x1 ... xi]] [[y1 ... yj]]) }}
| 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.

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.
Definition disjoint {A:Type} (l1 l2: list A): Prop :=
forall a, In a l1 -> ~ In a l2.

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_
}.

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;
Expand All @@ -142,6 +145,17 @@ 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.

Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l.
}}

defns
Expand Down Expand Up @@ -175,6 +189,7 @@ defn

G ( fn ) = T1 , ... , Tn -> T
G [ x1 |-> T1 , ... , xn |-> Tn ] |- e : T
distinct (x1 , ... , xn)
------------------------------------------- :: func_decl
G |- def T fn ( T1 x1 , ... , Tn xn ) = e ;

Expand All @@ -193,6 +208,7 @@ 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)
disjoint ((y1 , ... , yn) , (x1 , ... , xn))
---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: 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 ]
48 changes: 27 additions & 21 deletions theories/abs_defs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,27 +100,20 @@ 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.

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.
Definition disjoint {A:Type} (l1 l2: list A): Prop :=
forall a, In a l1 -> ~ In a l2.

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_
}.

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;
Expand All @@ -130,6 +123,17 @@ 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.

Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l.

(** definitions *)

(* defns expression_well_typing *)
Expand All @@ -152,6 +156,7 @@ Inductive typ_F : G -> F -> Prop := (* defn F *)
| typ_func_decl : forall (T_x_list:list (T*x)) (G5:G) (T_5:T) (fn5:fn) (e5:e),
(Map.find fn5 G5 = Some (ctxv_sig (sig_sig (map (fun (pat_:(T*x)) => match pat_ with (T_,x_) => T_ end ) T_x_list) T_5) )) ->
typ_e (fold_right (fun (ax : x * T) (G5 : G) => Map.add (fst ax) (ctxv_T (snd ax)) G5) G5 (map (fun (pat_:(T*x)) => match pat_ with (T_,x_) => (x_,T_) end ) T_x_list) ) e5 T_5 ->
(NoDup (map (fun (pat_:(T*x)) => match pat_ with (T_,x_) => x_ end ) T_x_list) ) ->
typ_F G5 (F_fn T_5 fn5 T_x_list e5).
(** definitions *)

Expand All @@ -164,7 +169,8 @@ 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) ) ->
(disjoint (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => x_ 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) ) .


1 change: 1 addition & 0 deletions theories/abs_examples.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ Proof.
apply typ_func_decl.
- easy.
- apply e_const_5_T_int.
- simpl; constructor.
Qed.

Lemma e_call_const_5_T_int :
Expand Down
Loading

0 comments on commit 8055c81

Please sign in to comment.