134 lines
4.1 KiB
Coq
134 lines
4.1 KiB
Coq
Require Import Autosubst2.core Autosubst2.unscoped compile Autosubst2.syntax ssreflect typing.
|
|
From Hammer Require Import Tactics.
|
|
|
|
Lemma Bind_Inv Γ p A B U :
|
|
Γ ⊢ TBind p A B ∈ U ->
|
|
exists i, Γ ⊢ A ∈ Univ i /\ cons A Γ ⊢ B ∈ Univ i /\ Join.R (Univ i) U.
|
|
Proof.
|
|
move E : (TBind p A B) => u hu.
|
|
move : p A B E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma Univ_Inv Γ i U :
|
|
Γ ⊢ Univ i ∈ U ->
|
|
Γ ⊢ Univ i ∈ Univ (S i) /\ Join.R (Univ (S i)) U.
|
|
Proof.
|
|
move E : (Univ i) => u hu.
|
|
move : i E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma App_Inv Γ b a U :
|
|
Γ ⊢ App b a ∈ U ->
|
|
exists A B, Γ ⊢ b ∈ TBind TPi A B /\ Γ ⊢ a ∈ A /\ Join.R (subst_Tm (scons a VarTm) B) U.
|
|
Proof.
|
|
move E : (App b a) => u hu.
|
|
move : b a E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma Abs_Inv Γ A a U :
|
|
Γ ⊢ Abs A a ∈ U ->
|
|
exists B, cons A Γ ⊢ a ∈ B /\ Join.R (TBind TPi A B) U.
|
|
Proof.
|
|
move E : (Abs A a) => u hu.
|
|
move : A a E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma Var_Inv Γ i U :
|
|
Γ ⊢ VarTm i ∈ U ->
|
|
exists A, lookup i Γ A /\ Join.R A U.
|
|
Proof.
|
|
move E : (VarTm i) => u hu.
|
|
move : i E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma Pair_Inv Γ a b U :
|
|
Γ ⊢ Pair a b ∈ U ->
|
|
exists A B, Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_Tm (scons a VarTm) B /\ Join.R (TBind TSig A B) U.
|
|
Proof.
|
|
move E : (Pair a b ) => u hu.
|
|
move : a b E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma ProjL_Inv Γ a U :
|
|
Γ ⊢ Proj PL a ∈ U ->
|
|
exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R A U.
|
|
Proof.
|
|
move E : (Proj PL a) => u hu.
|
|
move : a E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma ProjR_Inv Γ a U :
|
|
Γ ⊢ Proj PR a ∈ U ->
|
|
exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R (subst_Tm (scons (Proj PL a) VarTm) B) U.
|
|
Proof.
|
|
move E : (Proj PR a) => u hu.
|
|
move : a E.
|
|
elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
|
|
Qed.
|
|
|
|
Lemma ctx_wff_mutual :
|
|
(forall Γ, ⊢ Γ -> True) /\
|
|
(forall Γ a A, Γ ⊢ a ∈ A -> ⊢ Γ).
|
|
Proof. apply wt_mutual => //=. Qed.
|
|
|
|
Lemma lookup_deter i Γ A A0 :
|
|
lookup i Γ A ->
|
|
lookup i Γ A0 -> A = A0.
|
|
Proof.
|
|
move => h. move : A0. elim : i Γ A / h; hauto lq:on inv:lookup.
|
|
Qed.
|
|
|
|
Lemma wt_unique :
|
|
(forall Γ, ⊢ Γ -> True) /\
|
|
(forall Γ a A, Γ ⊢ a ∈ A -> forall B, Γ ⊢ a ∈ B -> Join.R A B).
|
|
Proof.
|
|
apply wt_mutual => //=.
|
|
- move => i Γ A hΓ _ hl B.
|
|
move /Var_Inv.
|
|
move => [A0 [h0 h1]].
|
|
move : hl h0.
|
|
move : lookup_deter; repeat move/[apply]. move => ?. by subst.
|
|
- move => Γ i p A B hA ihA hB ihB U.
|
|
move /Bind_Inv => [j][ih0][ih1]ih2.
|
|
apply ihB in ih1.
|
|
move /Join.UnivInj in ih1. by subst.
|
|
- move => Γ a A B i hP ihP ha iha U.
|
|
move /Abs_Inv => [B0][ha']hJ.
|
|
move /iha in ha' => {iha}.
|
|
apply : Join.transitive; eauto.
|
|
apply Join.BindCong; eauto using Join.reflexive.
|
|
- move => Γ b a A B hb ihb ha iha U.
|
|
move /App_Inv. move => [A0][B0][hb'][ha']hU.
|
|
apply ihb in hb' => {ihb}.
|
|
move /Join.BindInj : hb'.
|
|
move => [_][hJ0]hJ1.
|
|
apply : Join.transitive; eauto.
|
|
by apply Join.substing.
|
|
- move => Γ a b A B i hS ihS ha iha hb ihb U.
|
|
move /Pair_Inv.
|
|
move => [A0][B0][{}/iha ha'][{}/ihb hb']hJ.
|
|
apply : Join.transitive; eauto.
|
|
apply Join.BindCong; eauto.
|
|
admit.
|
|
- move => Γ a A B ha iha U.
|
|
move /ProjL_Inv.
|
|
move => [A0][B0][{}/iha ha0]hU.
|
|
apply Join.BindInj in ha0.
|
|
decompose record ha0.
|
|
eauto using Join.transitive.
|
|
- move => Γ a A B ha iha U /ProjR_Inv [A0][B0][{}/iha /Join.BindInj ha'].
|
|
decompose record ha'.
|
|
move => h. apply : Join.transitive; eauto.
|
|
by apply Join.substing.
|
|
- move => Γ i hΓ _ B /Univ_Inv. tauto.
|
|
- move => Γ a A B i ha iha hb ihb.
|
|
move => h0 B0 {}/iha ha'.
|
|
eauto using Join.symmetric, Join.transitive.
|
|
Admitted.
|