add inversion lemmas (without proof)

This commit is contained in:
Michael Sippel 2024-09-24 05:32:59 +02:00
parent 666d14e91d
commit e0f467c848

View file

@ -10,50 +10,9 @@ Require Import subst_lemmas.
Require Import typing. Require Import typing.
Require Import typing_weakening. Require Import typing_weakening.
Require Import typing_regular. Require Import typing_regular.
Require Import typing_inv.
Require Import translate_morph. 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 * translated morphism path has valid typing