finish completeness proof (#133)

* finish completeness proof * fix one lemma
Beluga-lang · Jul 16, 2024 · a1abe3e · a1abe3e
1 parent a16c975
commit a1abe3e
Show file tree

Hide file tree

Showing 2 changed files with 50 additions and 80 deletions.
diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v
@@ -6,97 +6,60 @@ From Mcltt.Core Require Import
   Completeness.SubstitutionCases
   Completeness.TermStructureCases
   Completeness.UniverseCases
-  Completeness.VariableCases.
+  Completeness.VariableCases
+  Completeness.SubtypingCases.
 From Mcltt.Core Require Export Completeness.LogicalRelation SystemOpt.
 Import Domain_Notations.
 
 Section completeness_fundamental.
-  Let ctx_prop Γ (_ : {{ ⊢ Γ }}) : Prop := {{ ⊨ Γ }}.
-  Let ctx_eq_prop Γ Γ' (_ : {{ ⊢ Γ ≈ Γ' }}) : Prop := {{ ⊨ Γ ≈ Γ' }}.
-  Let exp_prop Γ M A (_ : {{ Γ ⊢ M : A }}) : Prop := {{ Γ ⊨ M : A }}.
-  Let exp_eq_prop Γ A M M' (_ : {{ Γ ⊢ M ≈ M' : A }}) : Prop := {{ Γ ⊨ M ≈ M' : A }}.
-  Let sub_prop Γ σ Δ (_ : {{ Γ ⊢s σ : Δ }}) : Prop := {{ Γ ⊨s σ : Δ }}.
-  Let sub_eq_prop Γ Δ σ σ' (_ : {{ Γ ⊢s σ ≈ σ' : Δ }}) : Prop := {{ Γ ⊨s σ ≈ σ' : Δ }}.
 
-  #[local]
-  Ltac unfold_prop :=
-    unfold ctx_prop, ctx_eq_prop, exp_prop, exp_eq_prop, sub_prop, sub_eq_prop in *;
-    clear ctx_prop ctx_eq_prop exp_prop exp_eq_prop sub_prop sub_eq_prop.
+  Theorem completeness_fundamental :
+    (forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}) /\
+      (forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}) /\
+      (forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\
+      (forall Γ A M M', {{ Γ ⊢ M ≈ M' : A }} -> {{ Γ ⊨ M ≈ M' : A }}) /\
+      (forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\
+      (forall Γ Δ σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊨s σ ≈ σ' : Δ }}) /\
+      (forall Γ A A', {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊨ A ⊆ A' }}).
+  Proof.
+    apply syntactic_wf_mut_ind;
+      mauto 3.
+    intros.
+    apply valid_exp_var;
+      mauto.
+  Qed.
 
   #[local]
-  Ltac solve_completeness_fundamental :=
-    unfold_prop; mauto; solve [apply valid_ctx_empty | apply valid_exp_var; mauto].
+   Ltac solve_it := pose proof completeness_fundamental; firstorder.
+
+
+  Theorem completeness_fundamental_ctx : forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}.
+  Proof. solve_it. Qed.
+
+  Theorem completeness_fundamental_ctx_sub : forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}.
+  Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_ctx : forall Γ (HΓ : {{ ⊢ Γ }}), ctx_prop Γ HΓ.
-  (* Proof with solve_completeness_fundamental using. *)
-  (*   induction 1 using wf_ctx_mut_ind *)
-  (*     with *)
-  (*     (P0 := ctx_eq_prop) *)
-  (*     (P1 := exp_prop) *)
-  (*     (P2 := exp_eq_prop) *)
-  (*     (P3 := sub_prop) *)
-  (*     (P4 := sub_eq_prop)... *)
-  (* Qed. *)
-  Admitted.
+  Theorem completeness_fundamental_exp : forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}.
+  Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_ctx_eq : forall Γ Γ' (HΓΓ' : {{ ⊢ Γ ≈ Γ' }}), ctx_eq_prop Γ Γ' HΓΓ'.
-  (* Proof with solve_completeness_fundamental using. *)
-  (*   induction 1 using wf_ctx_eq_mut_ind *)
-  (*     with *)
-  (*     (P := ctx_prop) *)
-  (*     (P1 := exp_prop) *)
-  (*     (P2 := exp_eq_prop) *)
-  (*     (P3 := sub_prop) *)
-  (*     (P4 := sub_eq_prop)... *)
-  (* Qed. *)
-  Admitted.
+  Theorem completeness_fundamental_exp_eq : forall Γ A M M', {{ Γ ⊢ M ≈ M' : A }} -> {{ Γ ⊨ M ≈ M' : A }}.
+  Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_exp : forall Γ M A (HM : {{ Γ ⊢ M : A }}), exp_prop Γ M A HM.
-  (* Proof with solve_completeness_fundamental using. *)
-  (*   induction 1 using wf_exp_mut_ind *)
-  (*     with *)
-  (*     (P := ctx_prop) *)
-  (*     (P0 := ctx_eq_prop) *)
-  (*     (P2 := exp_eq_prop) *)
-  (*     (P3 := sub_prop) *)
-  (*     (P4 := sub_eq_prop)... *)
-  (* Qed. *)
-  Admitted.
+  Theorem completeness_fundamental_sub : forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}.
+  Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_exp_eq : forall Γ M M' A (HMM' : {{ Γ ⊢ M ≈ M' : A }}), exp_eq_prop Γ A M M' HMM'.
-  (* Proof with solve_completeness_fundamental using. *)
-  (*   induction 1 using wf_exp_eq_mut_ind *)
-  (*     with *)
-  (*     (P := ctx_prop) *)
-  (*     (P0 := ctx_eq_prop) *)
-  (*     (P1 := exp_prop) *)
-  (*     (P3 := sub_prop) *)
-  (*     (P4 := sub_eq_prop)... *)
-  (* Qed. *)
-  Admitted.
+  Theorem completeness_fundamental_sub_eq : forall Γ Δ σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊨s σ ≈ σ' : Δ }}.
+  Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_sub : forall Γ σ Δ (Hσ : {{ Γ ⊢s σ : Δ }}), sub_prop Γ σ Δ Hσ.
-  (* Proof with solve_completeness_fundamental using. *)
-  (*   induction 1 using wf_sub_mut_ind *)
-  (*     with *)
-  (*     (P := ctx_prop) *)
-  (*     (P0 := ctx_eq_prop) *)
-  (*     (P1 := exp_prop) *)
-  (*     (P2 := exp_eq_prop) *)
-  (*     (P4 := sub_eq_prop)... *)
-  (* Qed. *)
-  Admitted.
+  Theorem completeness_fundamental_subtyp : forall Γ A A', {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊨ A ⊆ A' }}.
+  Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_sub_eq : forall Γ σ σ' Δ (Hσσ' : {{ Γ ⊢s σ ≈ σ' : Δ }}), sub_eq_prop Γ Δ σ σ' Hσσ'.
-  (* Proof with solve_completeness_fundamental using. *)
-  (*   induction 1 using wf_sub_eq_mut_ind *)
-  (*     with *)
-  (*     (P := ctx_prop) *)
-  (*     (P0 := ctx_eq_prop) *)
-  (*     (P1 := exp_prop) *)
-  (*     (P2 := exp_eq_prop) *)
-  (*     (P3 := sub_prop)... *)
-  (* Qed. *)
-  Admitted.
+  Theorem completeness_fundamental_ctx_eq : forall Γ Γ', {{ ⊢ Γ ≈ Γ' }} -> {{ ⊨ Γ ≈ Γ' }}.
+  Proof.
+    induction 1.
+    - apply valid_ctx_empty.
+    - apply completeness_fundamental_exp_eq in H2.
+      mauto.
+  Qed.
 
 End completeness_fundamental.
diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
@@ -324,7 +324,14 @@ with wf_exp_eq_mut_ind := Induction for wf_exp_eq Sort Prop
 with wf_sub_mut_ind := Induction for wf_sub Sort Prop
 with wf_sub_eq_mut_ind := Induction for wf_sub_eq Sort Prop
 with wf_subtyping_mut_ind := Induction for wf_subtyping Sort Prop.
-
+Combined Scheme syntactic_wf_mut_ind from
+  wf_ctx_mut_ind,
+  wf_ctx_sub_mut_ind,
+  wf_exp_mut_ind,
+  wf_exp_eq_mut_ind,
+  wf_sub_mut_ind,
+  wf_sub_eq_mut_ind,
+  wf_subtyping_mut_ind.
 
 Inductive wf_ctx_eq : ctx -> ctx -> Prop :=
 | wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}