From c0f3beda1d0cfca899c618fc340c57a4ec08c24c Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Thu, 9 May 2024 20:24:50 -0400 Subject: [PATCH] Prove some cases of completeness (#74) * Prove some cases of completeness * Prove some more cases --- theories/Core/Completeness/LogicalRelation.v | 22 ++- .../Core/Completeness/TermStructureCases.v | 142 ++++++++++++++++++ theories/Core/Completeness/UniverseCases.v | 52 +++++++ theories/Core/Completeness/VariableCases.v | 59 ++++++++ theories/Core/Semantic/Domain.v | 4 + .../Core/Semantic/Evaluation/Definitions.v | 2 + theories/LibTactics.v | 20 +++ theories/_CoqProject | 3 + 8 files changed, 297 insertions(+), 7 deletions(-) create mode 100644 theories/Core/Completeness/TermStructureCases.v create mode 100644 theories/Core/Completeness/UniverseCases.v create mode 100644 theories/Core/Completeness/VariableCases.v diff --git a/theories/Core/Completeness/LogicalRelation.v b/theories/Core/Completeness/LogicalRelation.v index c3558135..c71c7c24 100644 --- a/theories/Core/Completeness/LogicalRelation.v +++ b/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). diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v new file mode 100644 index 00000000..28231956 --- /dev/null +++ b/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. diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v new file mode 100644 index 00000000..9e4af774 --- /dev/null +++ b/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. diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v new file mode 100644 index 00000000..d2e1c72e --- /dev/null +++ b/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. diff --git a/theories/Core/Semantic/Domain.v b/theories/Core/Semantic/Domain.v index 3b7679f3..ea406013 100644 --- a/theories/Core/Semantic/Domain.v +++ b/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. diff --git a/theories/Core/Semantic/Evaluation/Definitions.v b/theories/Core/Semantic/Evaluation/Definitions.v index 84a4c68d..42a74b0d 100644 --- a/theories/Core/Semantic/Evaluation/Definitions.v +++ b/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 : diff --git a/theories/LibTactics.v b/theories/LibTactics.v index 5e65860b..464910a1 100644 --- a/theories/LibTactics.v +++ b/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" := diff --git a/theories/_CoqProject b/theories/_CoqProject index fda4437f..c3e016f1 100644 --- a/theories/_CoqProject +++ b/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