From 48429c6316753c3014602cc054333eea64cc8f60 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 24 Sep 2024 04:57:16 +0200
Subject: [PATCH] =?UTF-8?q?add=20preliminary=20proof=20of=20transl=5Fprese?=
=?UTF-8?q?rvation=20(with=20env=5Fwf=20=CE=93=20admitted)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
coq/_CoqProject | 2 +-
coq/soundness/translate_expr.v | 146 ++++++++++++++++++++++++++++++++
coq/soundness/translate_morph.v | 6 +-
coq/typing/env.v | 4 +-
coq/typing/typing.v | 2 +-
5 files changed, 155 insertions(+), 5 deletions(-)
create mode 100644 coq/soundness/translate_expr.v
diff --git a/coq/_CoqProject b/coq/_CoqProject
index b925f8f..1c1e5b6 100644
--- a/coq/_CoqProject
+++ b/coq/_CoqProject
@@ -18,5 +18,5 @@ lemmas/subst_lemmas.v
lemmas/typing_weakening.v
lemmas/typing_regular.v
soundness/translate_morph.v
-
+soundness/translate_expr.v
diff --git a/coq/soundness/translate_expr.v b/coq/soundness/translate_expr.v
new file mode 100644
index 0000000..07d58ae
--- /dev/null
+++ b/coq/soundness/translate_expr.v
@@ -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.
diff --git a/coq/soundness/translate_morph.v b/coq/soundness/translate_morph.v
index 5c908d5..e195241 100644
--- a/coq/soundness/translate_morph.v
+++ b/coq/soundness/translate_morph.v
@@ -238,7 +238,8 @@ Proof.
inversion Lcτ; subst.
rewrite expr_open_lc.
- apply typing_weakening with (Γ':=(x,[< σ ~ τ >])::[]).
+ simpl_env.
+ apply typing_weakening.
apply T_MorphFun.
apply IHtranslate_morphism_path.
apply type_lc_ladder_inv2 with (σ:=σ); assumption; assumption.
@@ -287,7 +288,8 @@ Proof.
* apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
rewrite expr_open_lc.
- apply typing_weakening with (Γ':=(x,τ)::[]).
+ simpl_env.
+ apply typing_weakening.
apply T_MorphFun.
apply IHtranslate_morphism_path1.
3: apply env_wf_type.
diff --git a/coq/typing/env.v b/coq/typing/env.v
index 251fb16..3fce468 100644
--- a/coq/typing/env.v
+++ b/coq/typing/env.v
@@ -3,6 +3,8 @@ Require Import Atom.
Require Import Environment.
Require Import debruijn.
+Open Scope list_scope.
+
Notation env := (list (atom * type_DeBruijn)).
(* 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 :=
| env_wf_empty :
- env_wf []
+ env_wf nil
| env_wf_type : forall Γ x τ,
env_wf Γ ->
diff --git a/coq/typing/typing.v b/coq/typing/typing.v
index 12e9549..ec19fe0 100644
--- a/coq/typing/typing.v
+++ b/coq/typing/typing.v
@@ -99,7 +99,7 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru
| Expand_TypeApp : forall Γ e e' σ τ,
(Γ |- e \is [< ∀ τ >]) ->
- (Γ |- [[ e \is τ ]] = e') ->
+ (Γ |- [[ e \is [< ∀ τ >] ]] = e') ->
(Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }])
| Expand_Abs : forall Γ L σ e e' τ,