Add the statement for soundness cases

theories/Core/Completeness/FundamentalTheorem.v

@@ -1,14 +1,15 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import
-  Completeness.ContextCases
-  Completeness.FunctionCases
-  Completeness.NatCases
-  Completeness.SubstitutionCases
-  Completeness.TermStructureCases
-  Completeness.UniverseCases
-  Completeness.VariableCases
-  Completeness.SubtypingCases.
-From Mcltt.Core Require Export Completeness.LogicalRelation SystemOpt.
+From Mcltt.Core.Completeness Require Import
+  ContextCases
+  FunctionCases
+  NatCases
+  SubstitutionCases
+  TermStructureCases
+  UniverseCases
+  VariableCases
+  SubtypingCases.
+From Mcltt.Core.Completeness Require Export LogicalRelation.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Section completeness_fundamental.

theories/Core/Soundness.v

@@ -1,5 +1,7 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Semantic.Domain Semantic.NbE System.
+From Mcltt.Core.Semantic Require Import NbE.
+From Mcltt.Core.Soundness Require Import LogicalRelation FundamentalTheorem.
+From Mcltt.Core.Syntactic Require Import SystemOpt.
 Import Domain_Notations.
 
 Theorem soundness : forall {Γ M A},

theories/Core/Soundness/ContextCases.v

@@ -0,0 +1,25 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import LogicalRelation Realizability.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+Import Domain_Notations.
+
+Lemma glu_rel_ctx_empty : {{ ⊩ ⋅ }}.
+Proof.
+  do 2 econstructor; reflexivity.
+Qed.
+
+#[export]
+Hint Resolve glu_rel_ctx_empty : mcltt.
+
+Lemma glu_rel_ctx_extend : forall {Γ A i},
+    {{ ⊩ Γ }} ->
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ ⊩ Γ , A }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_ctx_extend : mcltt.

theories/Core/Soundness/FunctionCases.v

@@ -0,0 +1,37 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import LogicalRelation Realizability.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+Import Domain_Notations.
+
+Lemma glu_rel_exp_pi : forall {Γ A B i},
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ, A ⊩ B : Type@i }} ->
+    {{ Γ ⊩ Π A B : Type@i }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_pi : mcltt.
+
+Lemma glu_rel_exp_fn : forall {Γ M A B i},
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ, A ⊩ M : B }} ->
+    {{ Γ ⊩ λ A M : Π A B }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_fn : mcltt.
+
+Lemma glu_rel_exp_app : forall {Γ M N A B i},
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ, A ⊩ B : Type@i }} ->
+    {{ Γ ⊩ M : Π A B }} ->
+    {{ Γ ⊩ N : A }} ->
+    {{ Γ ⊩ M N : B[Id,,N] }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_app : mcltt.

theories/Core/Soundness/FundamentalTheorem.v

@@ -0,0 +1,45 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Soundness Require Import
+  ContextCases
+  FunctionCases
+  NatCases
+  SubstitutionCases
+  SubtypingCases
+  TermStructureCases
+  UniverseCases.
+From Mcltt.Core.Soundness Require Export LogicalRelation.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
+Import Domain_Notations.
+
+Section soundness_fundamental.
+
+  Theorem soundness_fundamental :
+    (forall Γ, {{ ⊢ Γ }} -> {{ ⊩ Γ }}) /\
+      (forall Γ A M, {{ Γ ⊢ M : A }} -> {{ Γ ⊩ M : A }}) /\
+      (forall Γ Δ σ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊩s σ : Δ }}).
+  Proof.
+    apply syntactic_wf_mut_ind'; mauto 3.
+
+    - intros.
+      assert (exists i, {{ Γ ⊩ A' : Type@i }}) as [] by admit. (* this should be added to the syntactic judgement *)
+      mauto.
+    - intros.
+      assert {{ ⊩ Δ' }} by admit. (* this should be added to the syntactic judgement *)
+      mauto.
+  Admitted.
+
+  #[local]
+  Ltac solve_it := pose proof soundness_fundamental; firstorder.
+
+  Theorem soundness_fundamental_ctx : forall Γ, {{ ⊢ Γ }} -> {{ ⊩ Γ }}.
+  Proof. solve_it. Qed.
+
+  Theorem soundness_fundamental_exp : forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊩ M : A }}.
+  Proof. solve_it. Qed.
+
+  Theorem soundness_fundamental_sub : forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊩s σ : Δ }}.
+  Proof. solve_it. Qed.
+
+End soundness_fundamental.

theories/Core/Soundness/NatCases.v

@@ -0,0 +1,43 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import LogicalRelation Realizability.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+Import Domain_Notations.
+
+Lemma glu_rel_exp_nat : forall {Γ i},
+    {{ ⊩ Γ }} ->
+    {{ Γ ⊩ ℕ : Type@i }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_nat : mcltt.
+
+Lemma glu_rel_exp_zero : forall {Γ},
+    {{ ⊩ Γ }} ->
+    {{ Γ ⊩ zero : ℕ }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_zero : mcltt.
+
+Lemma glu_rel_exp_succ : forall {Γ M},
+    {{ Γ ⊩ M : ℕ }} ->
+    {{ Γ ⊩ succ M : ℕ }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_succ : mcltt.
+
+Lemma glu_rel_exp_natrec : forall {Γ A i MZ MS M},
+    {{ Γ , ℕ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ MZ : A[Id,,zero] }} ->
+    {{ Γ , ℕ , A ⊩ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ ⊩ M : ℕ }} ->
+    {{ Γ ⊩ rec M return A | zero -> MZ | succ -> MS end : A[Id,,M] }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_natrec : mcltt.

theories/Core/Soundness/SubstitutionCases.v

@@ -0,0 +1,43 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import LogicalRelation Realizability.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+Import Domain_Notations.
+
+Lemma glu_rel_sub_id : forall {Γ},
+    {{ ⊩ Γ }} ->
+    {{ Γ ⊩s Id : Γ }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_sub_id : mcltt.
+
+Lemma glu_rel_sub_weaken : forall {Γ A},
+    {{ ⊩ Γ, A }} ->
+    {{ Γ, A ⊩s Wk : Γ }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_sub_weaken : mcltt.
+
+Lemma glu_rel_sub_compose : forall {Γ1 σ2 Γ2 σ1 Γ3},
+    {{ Γ1 ⊩s σ2 : Γ2 }} ->
+    {{ Γ2 ⊩s σ1 : Γ3 }} ->
+    {{ Γ1 ⊩s σ1 ∘ σ2 : Γ3 }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_sub_compose : mcltt.
+
+Lemma glu_rel_sub_extend : forall {Γ σ Δ M A i},
+    {{ Γ ⊩s σ : Δ }} ->
+    {{ Δ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ M : A[σ] }} ->
+    {{ Γ ⊩s (σ ,, M) : Δ , A }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_sub_extend : mcltt.

theories/Core/Soundness/TermStructureCases.v

@@ -0,0 +1,26 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import LogicalRelation Realizability.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+Import Domain_Notations.
+
+Lemma glu_rel_exp_vlookup : forall {Γ x A},
+    {{ ⊩ Γ }} ->
+    {{ #x : A ∈ Γ }} ->
+    {{ Γ ⊩ #x : A }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_vlookup : mcltt.
+
+Lemma glu_rel_exp_sub : forall {Γ σ Δ M A},
+    {{ Γ ⊩s σ : Δ }} ->
+    {{ Δ ⊩ M : A }} ->
+    {{ Γ ⊩ M[σ] : A[σ] }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_sub : mcltt.

theories/Core/Soundness/UniverseCases.v

@@ -0,0 +1,16 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import LogicalRelation Realizability.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+Import Domain_Notations.
+
+Lemma glu_rel_exp_typ : forall {Γ i},
+    {{ ⊩ Γ }} ->
+    {{ Γ ⊩ Type@i : Type@(S i) }}.
+Admitted.
+
+#[export]
+Hint Resolve glu_rel_exp_typ : mcltt.

theories/Core/Syntactic/System/Definitions.v

@@ -333,6 +333,14 @@ Combined Scheme syntactic_wf_mut_ind from
   wf_sub_eq_mut_ind,
   wf_subtyping_mut_ind.
 
+Scheme wf_ctx_mut_ind' := Induction for wf_ctx Sort Prop
+with wf_exp_mut_ind' := Induction for wf_exp Sort Prop
+with wf_sub_mut_ind' := Induction for wf_sub Sort Prop.
+Combined Scheme syntactic_wf_mut_ind' from
+  wf_ctx_mut_ind',
+  wf_exp_mut_ind',
+  wf_sub_mut_ind'.
+
 Inductive wf_ctx_eq : ctx -> ctx -> Prop :=
 | wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}
 | wf_ctx_eq_extend :
@@ -344,7 +352,6 @@ Inductive wf_ctx_eq : ctx -> ctx -> Prop :=
      {{ ⊢ Γ , A ≈ Δ , A' }} )
 where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope.
 
-
 #[export]
 Hint Constructors wf_ctx wf_ctx_eq wf_ctx_sub wf_exp wf_sub wf_exp_eq wf_sub_eq wf_subtyping ctx_lookup : mcltt.
 

theories/_CoqProject

@@ -52,14 +52,21 @@
 ./Core/Syntactic/System/Tactics.v
 ./Core/Syntactic/SystemOpt.v
 ./Core/Soundness.v
+./Core/Soundness/ContextCases.v
+./Core/Soundness/FunctionCases.v
+./Core/Soundness/FundamentalTheorem.v
 ./Core/Soundness/LogicalRelation.v
 ./Core/Soundness/LogicalRelation/Core.v
 ./Core/Soundness/LogicalRelation/CoreLemmas.v
 ./Core/Soundness/LogicalRelation/CoreTactics.v
 ./Core/Soundness/LogicalRelation/Definitions.v
 ./Core/Soundness/LogicalRelation/Lemmas.v
+./Core/Soundness/NatCases.v
 ./Core/Soundness/Realizability.v
+./Core/Soundness/SubstitutionCases.v
 ./Core/Soundness/SubtypingCases.v
+./Core/Soundness/TermStructureCases.v
+./Core/Soundness/UniverseCases.v
 ./Core/Soundness/Weakening.v
 ./Core/Soundness/Weakening/Definition.v
 ./Core/Soundness/Weakening/Lemmas.v