Prove some cases of completeness (#74)

* Prove some cases of completeness

* Prove some more cases

theories/Core/Completeness/LogicalRelation.v

@@ -1,5 +1,6 @@
 From Coq Require Import Relations.
-From Mcltt Require Import Base Domain Evaluation PER.
+From Mcltt Require Import Base.
+From Mcltt Require Export Evaluation PER.
 Import Domain_Notations.
 
 Inductive rel_exp (R : relation domain) M p M' p' : Prop :=
@@ -8,10 +9,10 @@ Inductive rel_exp (R : relation domain) M p M' p' : Prop :=
 Arguments mk_rel_exp {_ _ _ _ _}.
 
 Definition rel_exp_under_ctx Γ M M' A :=
-  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i
-     (elem_rel : forall {p p'} (equiva_p_p' : {{ Dom p ≈ p' ∈ env_rel }}), relation domain),
-  forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
-    rel_typ i A p A p' (elem_rel equiv_p_p') /\ rel_exp (elem_rel equiv_p_p') M p M' p'.
+  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
+  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+  exists (elem_rel : relation domain),
+     rel_typ i A p A p' elem_rel /\ rel_exp elem_rel M p M' p'.
 
 Definition valid_exp_under_ctx Γ M A := rel_exp_under_ctx Γ M M A.
 #[global]
@@ -25,9 +26,16 @@ Arguments mk_rel_subst {_ _ _ _ _ _}.
 Definition rel_subst_under_ctx Γ σ σ' Δ :=
   exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }})
      env_rel' (_ : {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ env_rel' }}),
-  forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
-    rel_subst env_rel σ p σ' p'.
+  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+    rel_subst env_rel' σ p σ' p'.
 
 Definition valid_subst_under_ctx Γ σ Δ := rel_subst_under_ctx Γ σ σ Δ.
 #[global]
 Arguments valid_subst_under_ctx _ _ _ /.
+
+Notation "⊨ Γ ≈ Γ'" := (per_ctx Γ Γ')  (in custom judg at level 80, Γ custom exp, Γ' custom exp).
+Notation "⊨ Γ" := (valid_ctx Γ) (in custom judg at level 80, Γ custom exp).
+Notation "Γ ⊨ M ≈ M' : A" := (rel_exp_under_ctx Γ M M' A) (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
+Notation "Γ ⊨ M : A" := (valid_exp_under_ctx Γ M A) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
+Notation "Γ ⊨s σ ≈ σ' : Δ" := (rel_subst_under_ctx Γ σ σ' Δ) (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
+Notation "Γ ⊨s σ : Δ" := (valid_subst_under_ctx Γ σ Δ) (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).

theories/Core/Completeness/TermStructureCases.v

@@ -0,0 +1,142 @@
+From Coq Require Import Relations RelationClasses.
+From Mcltt Require Import Base LibTactics LogicalRelation System.
+Import Domain_Notations.
+
+Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
+    {{ Δ ⊨ M ≈ M' : A }} ->
+    {{ Γ ⊨s σ ≈ σ' : Δ }} ->
+    {{ Γ ⊨ M[σ] ≈ M'[σ'] : A[σ] }}.
+Proof.
+  intros * [env_relΔ] [env_relΓ].
+  destruct_conjs.
+  per_ctx_env_irrel_rewrite.
+  eexists.
+  eexists; try eassumption.
+  eexists.
+  intros.
+  assert (env_relΓ p' p) by (eapply per_env_sym; eauto).
+  assert (env_relΓ p p) by (eapply per_env_trans; eauto).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+  per_univ_elem_irrel_rewrite.
+  assert (env_relΔ o o0) by (eapply per_env_trans; [eauto | | eapply per_env_sym]; revgoals; eauto).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΔ H).
+  destruct_by_head rel_exp.
+  destruct_by_head rel_typ.
+  per_univ_elem_irrel_rewrite.
+  eexists.
+  split; [> econstructor; only 1-2: econstructor; eauto ..].
+Qed.
+
+Lemma rel_exp_sub_id : forall {Γ M A},
+    {{ Γ ⊨ M : A }} ->
+    {{ Γ ⊨ M[Id] ≈ M : A }}.
+Proof.
+  intros * [env_relΓ].
+  destruct_conjs.
+  eexists.
+  eexists; try eassumption.
+  eexists.
+  intros.
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+  destruct_by_head rel_exp.
+  destruct_by_head rel_typ.
+  eexists.
+  split; econstructor; eauto.
+  repeat econstructor; mauto.
+Qed.
+
+Lemma rel_exp_sub_compose : forall {Γ τ Γ' σ Γ'' M A},
+    {{ Γ ⊨s τ : Γ' }} ->
+    {{ Γ' ⊨s σ : Γ'' }} ->
+    {{ Γ'' ⊨ M : A }} ->
+    {{ Γ ⊨ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }}.
+Proof.
+  intros * [env_relΓ [? [env_relΓ']]] [? [? [env_relΓ'']]] [].
+  destruct_conjs.
+  per_ctx_env_irrel_rewrite.
+  eexists.
+  eexists; try eassumption.
+  eexists.
+  intros.
+  assert (env_relΓ p' p) by (eapply per_env_sym; eauto).
+  assert (env_relΓ p p) by (eapply per_env_trans; eauto).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+  per_univ_elem_irrel_rewrite.
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ' H).
+  per_univ_elem_irrel_rewrite.
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ'' H).
+  destruct_by_head rel_exp.
+  destruct_by_head rel_typ.
+  per_univ_elem_irrel_rewrite.
+  eexists.
+  split; [> econstructor; only 1-2: repeat econstructor; mauto ..].
+Qed.
+
+Lemma rel_exp_conv : forall {Γ M M' A A' i},
+    {{ Γ ⊨ M ≈ M' : A }} ->
+    {{ Γ ⊨ A ≈ A' : Type@i }} ->
+    {{ Γ ⊨ M ≈ M' : A' }}.
+Proof.
+  intros * [env_relΓ] [env_relΓ'].
+  destruct_conjs.
+  per_ctx_env_irrel_rewrite.
+  eexists.
+  eexists; try eassumption.
+  eexists.
+  intros.
+  assert (env_relΓ p p) by (eapply per_env_trans; eauto; eapply per_env_sym; eauto).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+  destruct_by_head rel_exp.
+  destruct_by_head rel_typ.
+  inversion_by_head (eval_exp {{{ Type@i }}}); subst.
+  per_univ_elem_irrel_rewrite.
+  match_by_head1 per_univ_elem ltac:(fun H => invert_per_univ_elem H; let n := numgoals in guard n <= 1); clear_refl_eqs.
+  destruct_conjs.
+  per_univ_elem_irrel_rewrite.
+  eexists.
+  split; econstructor; eauto.
+  eapply per_univ_trans; [eapply per_univ_sym |]; eauto.
+Qed.
+
+Lemma rel_exp_sym : forall {Γ M M' A},
+    {{ Γ ⊨ M ≈ M' : A }} ->
+    {{ Γ ⊨ M' ≈ M : A }}.
+Proof.
+  intros * [env_relΓ].
+  destruct_conjs.
+  econstructor.
+  eexists; try eassumption.
+  eexists.
+  intros ? ? equiv_p_p'.
+  assert (env_relΓ p' p) by (eapply per_env_sym; eauto).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H); destruct_conjs.
+  destruct_by_head rel_exp.
+  destruct_by_head rel_typ.
+  per_univ_elem_irrel_rewrite.
+  eexists.
+  split; econstructor; eauto.
+  eapply per_elem_sym; eauto.
+Qed.
+
+Lemma rel_exp_trans : forall {Γ M1 M2 M3 A},
+    {{ Γ ⊨ M1 ≈ M2 : A }} ->
+    {{ Γ ⊨ M2 ≈ M3 : A }} ->
+    {{ Γ ⊨ M1 ≈ M3 : A }}.
+Proof.
+  intros * [env_relΓ] [env_relΓ'].
+  destruct_conjs.
+  per_ctx_env_irrel_rewrite.
+  econstructor.
+  eexists; try eassumption.
+  eexists.
+  intros ? ? equiv_p_p'.
+  assert (env_relΓ p' p) by (eapply per_env_sym; eauto).
+  assert (env_relΓ p' p') by (eapply per_env_trans; eauto).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H); destruct_conjs.
+  destruct_by_head rel_exp.
+  destruct_by_head rel_typ.
+  per_univ_elem_irrel_rewrite.
+  eexists.
+  split; econstructor; eauto.
+  eapply per_elem_trans; eauto.
+Qed.

theories/Core/Completeness/UniverseCases.v

@@ -0,0 +1,52 @@
+From Mcltt Require Import Base LibTactics LogicalRelation.
+Import Domain_Notations.
+
+Lemma valid_typ : forall {i Γ},
+    {{ ⊨ Γ }} ->
+    {{ Γ ⊨ Type@i : Type@(S i) }}.
+Proof.
+  intros * [].
+  econstructor.
+  eexists; try eassumption.
+  eexists.
+  intros.
+  exists (per_univ (S i)).
+  unshelve (split; repeat econstructor); mauto.
+Qed.
+
+Lemma rel_exp_typ_sub : forall {i Γ σ Δ},
+    {{ Γ ⊨s σ : Δ }} ->
+    {{ Γ ⊨ Type@i[σ] ≈ Type@i : Type@(S i) }}.
+Proof.
+  intros * [env_rel].
+  destruct_conjs.
+  econstructor.
+  eexists; try eassumption.
+  eexists.
+  intros.
+  exists (per_univ (S i)).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_rel H).
+  unshelve (split; repeat econstructor); only 4: eauto; mauto.
+Qed.
+
+Lemma rel_exp_cumu : forall {i Γ A A'},
+    {{ Γ ⊨ A ≈ A' : Type@i }} ->
+    {{ Γ ⊨ A ≈ A' : Type@(S i) }}.
+Proof.
+  intros * [env_rel].
+  destruct_conjs.
+  econstructor.
+  eexists; try eassumption.
+  exists (S (S i)).
+  intros.
+  exists (per_univ (S i)).
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_rel H).
+  inversion_by_head rel_typ.
+  inversion_by_head rel_exp.
+  inversion_by_head (eval_exp {{{ Type@i }}}); subst.
+  match_by_head per_univ_elem ltac:(fun H => invert_per_univ_elem H); subst.
+  destruct_conjs.
+  per_univ_elem_irrel_rewrite.
+  match_by_head per_univ_elem ltac:(fun H => apply per_univ_elem_cumu in H).
+  split; econstructor; try eassumption; repeat econstructor; mauto.
+Qed.

theories/Core/Completeness/VariableCases.v

@@ -0,0 +1,59 @@
+From Coq Require Import Relations.
+From Mcltt Require Import Base LibTactics LogicalRelation System.
+Import Domain_Notations.
+
+Lemma valid_lookup : forall {Γ x A env_rel}
+                        (equiv_Γ_Γ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}),
+    {{ #x : A ∈ Γ }} ->
+    exists i,
+    forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+    exists elem_rel,
+      rel_typ i A p A p' elem_rel /\ rel_exp elem_rel {{{ #x }}} p {{{ #x }}} p'.
+Proof with solve [repeat econstructor; mauto].
+  intros.
+  assert {{ #x : A ∈ Γ }} as HxinΓ by mauto.
+  remember Γ as Δ eqn:HΔΓ in HxinΓ, equiv_Γ_Γ at 2. clear HΔΓ. rename equiv_Γ_Γ into equiv_Γ_Δ.
+  remember A as A' eqn:HAA' in HxinΓ |- * at 2. clear HAA'.
+  gen Δ A' env_rel.
+  induction H; intros * equiv_Γ_Δ H0; inversion H0; subst; clear H0; inversion_clear equiv_Γ_Δ; subst;
+    try (specialize (IHctx_lookup _ _ _ equiv_Γ_Γ' H2) as [j ?]; destruct_conjs);
+    eexists; intros ? ? [];
+    (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H); destruct_conjs;
+    eexists.
+  - split; econstructor...
+  - destruct_by_head rel_typ.
+    destruct_by_head rel_exp.
+    inversion_by_head (eval_exp {{{ #n }}}); subst.
+    split; econstructor; simpl...
+Qed.
+
+Lemma valid_var : forall {Γ x A},
+    {{ ⊨ Γ }} ->
+    {{ #x : A ∈ Γ }} ->
+    {{ Γ ⊨ #x : A }}.
+Proof.
+  intros * [? equiv_Γ_Γ] ?.
+  econstructor.
+  unshelve epose proof (valid_lookup equiv_Γ_Γ _); mauto.
+Qed.
+
+Lemma rel_exp_var_weaken : forall {Γ B x A},
+    {{ ⊨ Γ , B }} ->
+    {{ #x : A ∈ Γ }} ->
+    {{ Γ , B ⊨ #x[Wk] ≈ #(S x) : A[Wk] }}.
+Proof.
+  intros * [] HxinΓ.
+  match_by_head1 per_ctx_env ltac:(fun H => inversion H); subst.
+  unshelve epose proof (valid_lookup _ HxinΓ); revgoals; mauto.
+  destruct_conjs.
+  eexists.
+  eexists; try eassumption.
+  eexists.
+  intros ? ? [].
+  (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+  destruct_by_head rel_typ.
+  destruct_by_head rel_exp.
+  inversion_by_head (eval_exp {{{ #x }}}); subst.
+  eexists.
+  split; [> econstructor; only 1-2: repeat econstructor; mauto ..].
+Qed.

theories/Core/Semantic/Domain.v

@@ -23,14 +23,18 @@ with domain_nf : Set :=
 where "'env'" := (nat -> domain).
 
 Definition empty_env : env := fun x => d_zero.
+Arguments empty_env _ /.
+
 Definition extend_env (p : env) (d : domain) : env :=
   fun n =>
     match n with
     | 0 => d
     | S n' => p n'
     end.
+Arguments extend_env _ _ _ /.
 
 Definition drop_env (p : env) : env := fun n => p (S n).
+Arguments drop_env _ _ /.
 
 #[global] Declare Custom Entry domain.
 #[global] Bind Scope mcltt_scope with domain.

theories/Core/Semantic/Evaluation/Definitions.v

@@ -12,6 +12,8 @@ Generalizable All Variables.
 Inductive eval_exp : exp -> env -> domain -> Prop :=
 | eval_exp_typ :
   `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
+| eval_exp_var :
+  `( {{ ⟦ # x ⟧ p ↘ ~(p x) }} )
 | eval_exp_nat :
   `( {{ ⟦ ℕ ⟧ p ↘ ℕ }} )
 | eval_exp_zero :

theories/LibTactics.v

@@ -103,6 +103,26 @@ Ltac clean_replace_by exp0 exp1 tac :=
 
 Tactic Notation "clean" "replace" uconstr(exp0) "with" uconstr(exp1) "by" tactic3(tac) := clean_replace_by exp0 exp1 tac.
 
+Ltac match_by_head1 head tac :=
+  match goal with
+  | [ H : ?X _ _ _ _ _ _ _ _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ _ _ _ _ _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ _ _ _ _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ _ _ _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ _ _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ _ |- _ ] => unify X head; tac H
+  | [ H : ?X _ |- _ ] => unify X head; tac H
+  | [ H : ?X |- _ ] => unify X head; tac H
+  end.
+Ltac match_by_head head tac := repeat (match_by_head1 head ltac:(fun H => tac H; try mark H)); unmark_all.
+
+Ltac inversion_by_head head := match_by_head head ltac:(fun H => inversion H).
+Ltac inversion_clear_by_head head := match_by_head head ltac:(fun H => inversion_clear H).
+Ltac destruct_by_head head := match_by_head head ltac:(fun H => destruct H).
+
 (** McLTT automation *)
 
 Tactic Notation "mauto" :=

theories/_CoqProject

@@ -5,6 +5,9 @@
 ./Core/Axioms.v
 ./Core/Base.v
 ./Core/Completeness/LogicalRelation.v
+./Core/Completeness/TermStructureCases.v
+./Core/Completeness/UniverseCases.v
+./Core/Completeness/VariableCases.v
 ./Core/Semantic/Domain.v
 ./Core/Semantic/Evaluation.v
 ./Core/Semantic/Evaluation/Definitions.v