add preliminary proof of transl_preservation (with env_wf Γ admitted)

This commit is contained in:
Michael Sippel 2024-09-24 04:57:16 +02:00
parent ac63139c67
commit 48429c6316
Signed by: senvas
GPG key ID: F96CF119C34B64A6
5 changed files with 155 additions and 5 deletions

View file

@ -18,5 +18,5 @@ lemmas/subst_lemmas.v
lemmas/typing_weakening.v lemmas/typing_weakening.v
lemmas/typing_regular.v lemmas/typing_regular.v
soundness/translate_morph.v soundness/translate_morph.v
soundness/translate_expr.v

View file

@ -0,0 +1,146 @@
From Coq Require Import Lists.List.
Require Import Atom.
Require Import Environment.
Require Import Metatheory.
Require Import debruijn.
Require Import subtype.
Require Import env.
Require Import morph.
Require Import subst_lemmas.
Require Import typing.
Require Import typing_weakening.
Require Import typing_regular.
Require Import translate_morph.
Lemma typing_inv_tabs : forall Γ t τ,
(Γ |- [{ Λ t }] \is [< τ >]) ->
forall L x, x `notin` L ->
(Γ |- (expr_open_type (ty_fvar x) t) \is τ)
.
Proof.
Admitted.
Lemma typing_inv_abs : forall Γ σ t τ,
(Γ |- [{ λ σ t }] \is [< σ -> τ >]) ->
forall L x, x `notin` L ->
((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
.
Proof.
Admitted.
Lemma typing_inv_morph : forall Γ σ t τ,
(Γ |- [{ λ σ morph t }] \is [< σ ->morph τ >]) ->
forall L x, x `notin` L ->
((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
.
Proof.
intros.
inversion H.
subst.
Admitted.
Lemma typing_inv_let : forall Γ s σ t τ,
(Γ |- s \is σ) ->
(Γ |- [{ let s in t }] \is [< τ >]) ->
forall L x, x `notin` L ->
((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
.
Proof.
Admitted.
(*
* translated morphism path has valid typing
*)
Lemma transl_preservation : forall Γ e e' τ,
(Γ |- e \is τ) ->
(Γ |- [[ e \is τ ]] = e') ->
(Γ |- e' \is τ)
.
Proof.
intros Γ e e' τ Typing Transl.
induction Transl.
(* free var *)
- assumption.
(* let *)
- apply T_Let with (L:=L) (σ:=σ).
* apply IHTransl.
assumption.
* intros x Fr.
apply H1.
assumption.
apply typing_inv_let with (L:=L) (s:=e).
1-3:assumption.
apply typing_inv_let with (L:=L) (s:=e).
1-3:assumption.
(* type abs *)
- apply T_TypeAbs with (L:=L).
intros x Fr.
apply H0.
assumption.
apply typing_inv_tabs with (L:=L).
1-2:assumption.
apply typing_inv_tabs with (L:=L).
1-2:assumption.
(* type app *)
- apply T_TypeApp.
apply IHTransl.
assumption.
(* abs *)
- apply T_Abs with (L:=L).
intros x Fr.
apply H1.
assumption.
apply typing_inv_abs with (L:=L).
1-2:assumption.
apply typing_inv_abs with (L:=L).
1-2:assumption.
(* morph abs *)
- apply T_MorphAbs with (L:=L).
intros x Fr.
apply H1.
assumption.
apply typing_inv_morph with (L:=L).
1-2:assumption.
apply typing_inv_morph with (L:=L).
1-2:assumption.
(* app *)
- apply T_App with (σ':=σ) (σ:=σ); auto.
apply T_App with (σ':=σ') (σ:=σ'); auto.
2-3: apply id_morphism_path.
apply T_MorphFun.
apply morphism_path_correct with (τ:=σ') (τ':=σ).
3: assumption.
2:admit. (* env wf *)
apply typing_regular_type_lc with (Γ:=Γ) (e:=a).
assumption.
apply typing_regular_type_lc with (Γ:=Γ) (e:=a).
assumption.
apply morph_regular_lc with (Γ:=Γ) (τ:=σ') (τ':=σ).
admit. (* env wf *)
apply typing_regular_type_lc with (Γ:=Γ) (e:=a).
assumption.
assumption.
- auto with typing_hints.
- auto with typing_hints.
- eauto with typing_hints.
Admitted.

View file

@ -238,7 +238,8 @@ Proof.
inversion Lcτ; subst. inversion Lcτ; subst.
rewrite expr_open_lc. rewrite expr_open_lc.
apply typing_weakening with (Γ':=(x,[< σ ~ τ >])::[]). simpl_env.
apply typing_weakening.
apply T_MorphFun. apply T_MorphFun.
apply IHtranslate_morphism_path. apply IHtranslate_morphism_path.
apply type_lc_ladder_inv2 with (σ:=σ); assumption; assumption. apply type_lc_ladder_inv2 with (σ:=σ); assumption; assumption.
@ -287,7 +288,8 @@ Proof.
* apply T_App with (σ':=τ) (σ:=τ) (τ:=τ'). * apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
rewrite expr_open_lc. rewrite expr_open_lc.
apply typing_weakening with (Γ':=(x,τ)::[]). simpl_env.
apply typing_weakening.
apply T_MorphFun. apply T_MorphFun.
apply IHtranslate_morphism_path1. apply IHtranslate_morphism_path1.
3: apply env_wf_type. 3: apply env_wf_type.

View file

@ -3,6 +3,8 @@ Require Import Atom.
Require Import Environment. Require Import Environment.
Require Import debruijn. Require Import debruijn.
Open Scope list_scope.
Notation env := (list (atom * type_DeBruijn)). Notation env := (list (atom * type_DeBruijn)).
(* env is well-formed if each atom is bound at most once (* env is well-formed if each atom is bound at most once
@ -10,7 +12,7 @@ Notation env := (list (atom * type_DeBruijn)).
*) *)
Inductive env_wf : env -> Prop := Inductive env_wf : env -> Prop :=
| env_wf_empty : | env_wf_empty :
env_wf [] env_wf nil
| env_wf_type : forall Γ x τ, | env_wf_type : forall Γ x τ,
env_wf Γ -> env_wf Γ ->

View file

@ -99,7 +99,7 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru
| Expand_TypeApp : forall Γ e e' σ τ, | Expand_TypeApp : forall Γ e e' σ τ,
(Γ |- e \is [< τ >]) -> (Γ |- e \is [< τ >]) ->
(Γ |- [[ e \is τ ]] = e') -> (Γ |- [[ e \is [< τ >] ]] = e') ->
(Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }]) (Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }])
| Expand_Abs : forall Γ L σ e e' τ, | Expand_Abs : forall Γ L σ e e' τ,