From b333fa835dd9ff3a1b0dff0ce8142a2f03c368c7 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Tue, 21 May 2024 04:22:22 -0400
Subject: [PATCH 1/8] Clean up proofs
---
theories/Core/Completeness/FunctionCases.v | 70 ++++++---------
theories/Core/Completeness/LogicalRelation.v | 2 +-
.../Completeness/LogicalRelation/Tactics.v | 10 +++
.../Core/Completeness/TermStructureCases.v | 88 ++++++++-----------
theories/Core/Completeness/UniverseCases.v | 39 ++++----
theories/Core/Completeness/VariableCases.v | 74 +++++++++++++---
theories/_CoqProject | 3 +-
7 files changed, 155 insertions(+), 131 deletions(-)
create mode 100644 theories/Core/Completeness/LogicalRelation/Tactics.v
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
index 8ae92b3f..7e142ee5 100644
--- a/theories/Core/Completeness/FunctionCases.v
+++ b/theories/Core/Completeness/FunctionCases.v
@@ -1,4 +1,4 @@
-From Coq Require Import Morphisms_Relations RelationClasses SetoidTactics.
+From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases System.
Import Domain_Notations.
@@ -52,11 +52,9 @@ Proof with intuition.
pose (env_relΓA0 := env_relΓA).
inversion_by_head (per_ctx_env env_relΓA); subst.
handle_per_ctx_env_irrel.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ Type@i }}}); subst.
match goal with
@@ -104,13 +102,11 @@ Proof with intuition.
pose (env_relΔA0 := env_relΔA).
inversion_by_head (per_ctx_env env_relΔA); subst.
handle_per_ctx_env_irrel.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
assert {{ Dom o' ≈ o' ∈ tail_rel }} by (etransitivity; [symmetry|]; eassumption).
- (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ Type@i }}}); subst.
match goal with
@@ -159,11 +155,9 @@ Proof with intuition.
pose (env_relΓA0 := env_relΓA).
inversion_by_head (per_ctx_env env_relΓA); subst.
handle_per_ctx_env_irrel.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ Type@i }}}); subst.
match goal with
@@ -209,12 +203,10 @@ Proof with intuition.
pose (env_relΔA0 := env_relΔA).
inversion_by_head (per_ctx_env env_relΔA); subst.
handle_per_ctx_env_irrel.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
- (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
eexists ?[elem_rel].
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
- per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |]; eauto with typeclass_instances.
@@ -248,12 +240,10 @@ Proof with intuition.
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
handle_per_ctx_env_irrel.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
assert (equiv_p'_p' : env_relΓ p' p') by (etransitivity; [symmetry |]; eauto).
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ Π A B }}}); subst.
match goal with
@@ -264,12 +254,12 @@ Proof with intuition.
destruct_by_head rel_exp.
functional_eval_rewrite_clear.
assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eauto).
- (on_all_hyp: fun H => destruct_rel_by_assumption in_rel H).
- (on_all_hyp_rev: fun H => destruct_rel_by_assumption in_rel H).
+ (on_all_hyp: destruct_rel_by_assumption in_rel).
+ (on_all_hyp_rev: destruct_rel_by_assumption in_rel).
handle_per_univ_elem_irrel.
eexists ?[elem_rel].
split; [> econstructor; only 1-2: econstructor ..].
- 1,3: repeat econstructor; eauto.
+ 1,3: repeat econstructor.
all: eauto.
Qed.
@@ -286,12 +276,10 @@ Proof with intuition.
pose (env_relΓ0 := env_relΓ).
pose (env_relΔ0 := env_relΔ).
handle_per_ctx_env_irrel.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΔ H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ (on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ Π A B }}}); subst.
match goal with
@@ -301,11 +289,11 @@ Proof with intuition.
handle_per_univ_elem_irrel.
destruct_by_head rel_exp.
functional_eval_rewrite_clear.
- (on_all_hyp_rev: fun H => destruct_rel_by_assumption in_rel H).
+ (on_all_hyp_rev: destruct_rel_by_assumption in_rel).
eexists ?[elem_rel].
split; [> econstructor; only 1-2: econstructor ..].
- 1,3,8,9: repeat econstructor; eauto.
- 5: econstructor.
+ 1,3,8,9: repeat econstructor.
+ 15: econstructor.
all: eauto.
Qed.
@@ -322,11 +310,9 @@ Proof with intuition.
pose (env_relΓA0 := env_relΓA).
inversion_by_head (per_ctx_env env_relΓA); subst.
handle_per_ctx_env_irrel.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
handle_per_univ_elem_irrel.
destruct_by_head rel_exp.
@@ -345,11 +331,9 @@ Proof with intuition.
intros * [env_relΓ].
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ Π A B }}}); subst.
match goal with
@@ -361,7 +345,7 @@ Proof with intuition.
eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption in_rel H).
+ (on_all_hyp: destruct_rel_by_assumption in_rel).
econstructor; eauto.
do 2 econstructor; eauto; econstructor; eauto.
econstructor.
diff --git a/theories/Core/Completeness/LogicalRelation.v b/theories/Core/Completeness/LogicalRelation.v
index 5c8daddf..7bf4b691 100644
--- a/theories/Core/Completeness/LogicalRelation.v
+++ b/theories/Core/Completeness/LogicalRelation.v
@@ -1 +1 @@
-From Mcltt.Core.Completeness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas.
+From Mcltt.Core.Completeness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas LogicalRelation.Tactics.
diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v
new file mode 100644
index 00000000..89400fc2
--- /dev/null
+++ b/theories/Core/Completeness/LogicalRelation/Tactics.v
@@ -0,0 +1,10 @@
+Ltac eexists_rel_exp :=
+ eexists;
+ eexists; [eassumption |];
+ eexists.
+
+Ltac eexists_rel_subst :=
+ eexists;
+ eexists; [eassumption |];
+ eexists;
+ eexists; [eassumption |].
diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v
index bfd8c44d..db0a81b7 100644
--- a/theories/Core/Completeness/TermStructureCases.v
+++ b/theories/Core/Completeness/TermStructureCases.v
@@ -1,5 +1,6 @@
From Coq Require Import Morphisms_Relations RelationClasses.
-From Mcltt Require Import Base LibTactics LogicalRelation System.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness.LogicalRelation System.
Import Domain_Notations.
Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
@@ -13,21 +14,19 @@ Proof.
destruct_conjs.
pose (env_relΔ0 := env_relΔ).
handle_per_ctx_env_irrel.
- eexists.
- eexists; try eassumption.
- eexists.
+ eexists_rel_exp.
intros.
- assert (env_relΓ p' p) by (symmetry; eauto).
- assert (env_relΓ p p) by (etransitivity; eauto).
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+ assert (env_relΓ p' p) by (symmetry; eassumption).
+ assert (env_relΓ p p) by (etransitivity; eassumption).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
handle_per_univ_elem_irrel.
- assert (env_relΔ o o0) by (etransitivity; [|symmetry; intuition]; intuition).
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΔ H).
+ assert (env_relΔ o o0) by (etransitivity; [|symmetry; eassumption]; eassumption).
+ (on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_exp.
destruct_by_head rel_typ.
handle_per_univ_elem_irrel.
eexists.
- split; [> econstructor; only 1-2: econstructor; eauto ..].
+ split; [> econstructor; only 1-2: econstructor; eassumption ..].
Qed.
Lemma rel_exp_sub_id : forall {Γ M A},
@@ -36,16 +35,14 @@ Lemma rel_exp_sub_id : forall {Γ M A},
Proof.
intros * [env_relΓ].
destruct_conjs.
- eexists.
- eexists; try eassumption.
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_exp.
destruct_by_head rel_typ.
eexists.
- split; econstructor; eauto.
- repeat econstructor; mauto.
+ split; econstructor; try eassumption.
+ repeat econstructor; eassumption.
Qed.
Lemma rel_exp_sub_compose : forall {Γ τ Γ' σ Γ'' M A},
@@ -61,23 +58,21 @@ Proof.
pose (env_relΓ'0 := env_relΓ').
pose (env_relΓ''0 := env_relΓ'').
handle_per_ctx_env_irrel.
- eexists.
- eexists; try eassumption.
- eexists.
+ eexists_rel_exp.
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).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
handle_per_univ_elem_irrel.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ' H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ').
handle_per_univ_elem_irrel.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ'' H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ'').
handle_per_univ_elem_irrel.
destruct_by_head rel_exp.
destruct_by_head rel_typ.
handle_per_univ_elem_irrel.
eexists.
- split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
+ split; [> econstructor; only 1-2: repeat econstructor; eassumption ..].
Qed.
Lemma rel_exp_conv : forall {Γ M M' A A' i},
@@ -91,12 +86,10 @@ Proof.
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
handle_per_ctx_env_irrel.
- eexists.
- eexists; try eassumption.
- eexists.
+ eexists_rel_exp.
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).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_exp.
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ Type@i }}}); subst.
@@ -110,8 +103,8 @@ Proof.
destruct_conjs.
handle_per_univ_elem_irrel.
eexists.
- split; econstructor; eauto.
- etransitivity; [symmetry |]; eauto.
+ split; econstructor; try eassumption.
+ etransitivity; [symmetry |]; eassumption.
Qed.
Lemma rel_exp_sym : forall {Γ M M' A},
@@ -122,18 +115,16 @@ Proof.
pose proof (@relation_equivalence_pointwise env).
intros * [env_relΓ].
destruct_conjs.
- econstructor.
- eexists; try eassumption.
- eexists.
- intros ? ? equiv_p_p'.
+ eexists_rel_exp.
+ intros.
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.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ); destruct_conjs.
destruct_by_head rel_exp.
destruct_by_head rel_typ.
handle_per_univ_elem_irrel.
eexists.
- split; econstructor; eauto.
- eapply per_elem_sym; eauto.
+ split; econstructor; try eassumption.
+ symmetry; eassumption.
Qed.
Lemma rel_exp_trans : forall {Γ M1 M2 M3 A},
@@ -147,19 +138,17 @@ Proof.
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
handle_per_ctx_env_irrel.
- econstructor.
- eexists; try eassumption.
- eexists.
- intros ? ? equiv_p_p'.
+ eexists_rel_exp.
+ intros.
assert (env_relΓ p' p) by (symmetry; eauto).
assert (env_relΓ p' p') by (etransitivity; eauto).
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H); destruct_conjs.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ); destruct_conjs.
destruct_by_head rel_exp.
destruct_by_head rel_typ.
handle_per_univ_elem_irrel.
eexists.
- split; econstructor; eauto.
- etransitivity; eauto.
+ split; econstructor; try eassumption.
+ etransitivity; eassumption.
Qed.
#[export]
@@ -183,22 +172,19 @@ Proof.
try solve [intuition]; clear Hpart;
destruct Hrel as [env_relΓ];
destruct_conjs.
- - eexists; eauto.
+ - eexists; eassumption.
- destruct_by_head valid_exp_under_ctx.
destruct_conjs.
eexists.
- eexists.
- eexists; [eassumption |].
- eexists.
+ eexists_rel_exp.
intros.
- (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
evar (j : nat).
eexists (per_univ j).
subst j.
split.
- + econstructor; only 1-2: repeat econstructor; eauto.
+ + econstructor; only 1-2: repeat econstructor; try eassumption.
per_univ_elem_econstructor; eauto.
- unfold per_univ.
- reflexivity.
+ apply Equivalence_Reflexive.
+ eapply rel_typ_implies_rel_exp; eassumption.
Qed.
diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v
index 6b55077c..62c8b4ec 100644
--- a/theories/Core/Completeness/UniverseCases.v
+++ b/theories/Core/Completeness/UniverseCases.v
@@ -1,5 +1,6 @@
-From Coq Require Import Morphisms_Relations.
-From Mcltt Require Import Base LibTactics LogicalRelation.
+From Coq Require Import Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness.LogicalRelation.
Import Domain_Notations.
Lemma valid_typ : forall {i Γ},
@@ -7,13 +8,11 @@ Lemma valid_typ : forall {i Γ},
{{ Γ ⊨ Type@i : Type@(S i) }}.
Proof.
intros * [].
- econstructor.
- eexists; try eassumption.
- eexists.
+ eexists_rel_exp.
intros.
- exists (per_univ (S i)).
- split; [> econstructor; only 1-2: econstructor; eauto ..]; [| exists (per_univ i)];
- per_univ_elem_econstructor; mauto; reflexivity.
+ eexists (per_univ _).
+ split; [> econstructor; only 1-2: econstructor; eauto ..]; [| eexists (per_univ _)];
+ per_univ_elem_econstructor; eauto; apply Equivalence_Reflexive.
Qed.
Lemma rel_exp_typ_sub : forall {i Γ σ Δ},
@@ -22,14 +21,12 @@ Lemma rel_exp_typ_sub : forall {i Γ σ Δ},
Proof.
intros * [env_rel].
destruct_conjs.
- econstructor.
- eexists; try eassumption.
- eexists.
+ eexists_rel_exp.
intros.
- exists (per_univ (S i)).
- (on_all_hyp: fun H => destruct_rel_by_assumption env_rel H).
- split; [> econstructor; only 1-2: repeat econstructor; eauto ..]; [| exists (per_univ i)];
- per_univ_elem_econstructor; mauto; reflexivity.
+ eexists (per_univ _).
+ (on_all_hyp: destruct_rel_by_assumption env_rel).
+ split; [> econstructor; only 1-2: repeat econstructor; eauto ..]; [| eexists (per_univ _)];
+ per_univ_elem_econstructor; eauto; apply Equivalence_Reflexive.
Qed.
Lemma rel_exp_cumu : forall {i Γ A A'},
@@ -40,20 +37,18 @@ Proof.
pose proof (@relation_equivalence_pointwise env).
intros * [env_rel].
destruct_conjs.
- econstructor.
- eexists; try eassumption.
- exists (S (S i)).
+ eexists_rel_exp.
intros.
- exists (per_univ (S i)).
- (on_all_hyp: fun H => destruct_rel_by_assumption env_rel H).
+ eexists (per_univ _).
+ (on_all_hyp: destruct_rel_by_assumption env_rel).
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.
+ match_by_head per_univ_elem invert_per_univ_elem; subst.
handle_per_univ_elem_irrel.
destruct_conjs.
match_by_head per_univ_elem ltac:(fun H => apply per_univ_elem_cumu in H).
split; [> econstructor; only 1-2: repeat econstructor; eauto ..]; [| eexists; eauto].
- per_univ_elem_econstructor; mauto.
+ per_univ_elem_econstructor; eauto.
reflexivity.
Qed.
diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v
index 3d3d04e8..c47beb3c 100644
--- a/theories/Core/Completeness/VariableCases.v
+++ b/theories/Core/Completeness/VariableCases.v
@@ -1,5 +1,6 @@
-From Coq Require Import Morphisms_Relations Relations.
-From Mcltt Require Import Base LibTactics LogicalRelation System.
+From Coq Require Import Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness.LogicalRelation System.
Import Domain_Notations.
Lemma valid_lookup : forall {Γ x A env_rel}
@@ -21,7 +22,7 @@ Proof with solve [repeat econstructor; mauto].
[|specialize (IHHxinΓ _ _ _ equiv_Γ_Γ' H2) as [j ?]; destruct_conjs];
apply_relation_equivalence;
eexists; intros ? ? [];
- (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H); destruct_conjs;
+ (on_all_hyp: destruct_rel_by_assumption tail_rel); destruct_conjs;
eexists.
- split; econstructor...
- destruct_by_head rel_typ.
@@ -36,8 +37,57 @@ Lemma valid_var : forall {Γ x A},
{{ Γ ⊨ #x : A }}.
Proof.
intros * [? equiv_Γ_Γ] ?.
- econstructor.
- unshelve epose proof (valid_lookup equiv_Γ_Γ _); mauto.
+ unshelve epose proof (valid_lookup equiv_Γ_Γ _) as []; try eassumption.
+ eexists_rel_exp; eassumption.
+Qed.
+
+Lemma rel_exp_var_0_sub : forall {Γ M σ Δ A},
+ {{ Γ ⊨s σ : Δ }} ->
+ {{ Γ ⊨ M : A[σ] }} ->
+ {{ Γ ⊨ #0[σ ,, M] ≈ M : A[σ] }}.
+Proof.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ [? [env_relΔ]]] [].
+ destruct_conjs.
+ pose (env_relΓ0 := env_relΓ).
+ handle_per_ctx_env_irrel.
+ eexists_rel_exp.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ destruct_by_head rel_typ.
+ destruct_by_head rel_exp.
+ inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
+ functional_eval_rewrite_clear.
+ eexists.
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eassumption.
+Qed.
+
+Lemma rel_exp_var_S_sub : forall {Γ M σ Δ A x B},
+ {{ Γ ⊨s σ : Δ }} ->
+ {{ Γ ⊨ M : A[σ] }} ->
+ {{ #x : B ∈ Δ }} ->
+ {{ Γ ⊨ #(S x)[σ ,, M] ≈ #x[σ] : B[σ] }}.
+Proof.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ [? [env_relΔ]]] [] HxinΓ.
+ destruct_conjs.
+ pose (env_relΓ0 := env_relΓ).
+ handle_per_ctx_env_irrel.
+ unshelve epose proof (valid_lookup _ HxinΓ); revgoals; try eassumption.
+ destruct_conjs.
+ eexists_rel_exp.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ (on_all_hyp: destruct_rel_by_assumption env_relΔ).
+ destruct_by_head rel_typ.
+ destruct_by_head rel_exp.
+ inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
+ inversion_by_head (eval_exp {{{ # x }}}); subst.
+ functional_eval_rewrite_clear.
+ eexists.
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eassumption.
Qed.
Lemma rel_exp_var_weaken : forall {Γ B x A},
@@ -47,19 +97,17 @@ Lemma rel_exp_var_weaken : forall {Γ B x A},
Proof.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [] HxinΓ.
- match_by_head1 per_ctx_env ltac:(fun H => inversion H); subst.
- unshelve epose proof (valid_lookup _ HxinΓ); revgoals; mauto.
+ intros * [env_relΓB] HxinΓ.
+ inversion_by_head (per_ctx_env env_relΓB); subst.
+ unshelve epose proof (valid_lookup _ HxinΓ); revgoals; try eassumption.
destruct_conjs.
- eexists.
- eexists; try eassumption.
- eexists.
+ eexists_rel_exp.
apply_relation_equivalence.
intros ? ? [].
- (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
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 ..].
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eassumption.
Qed.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 85235f52..a13a6832 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -4,10 +4,11 @@
./Core/Axioms.v
./Core/Base.v
+./Core/Completeness/FunctionCases.v
./Core/Completeness/LogicalRelation/Definitions.v
./Core/Completeness/LogicalRelation/Lemmas.v
+./Core/Completeness/LogicalRelation/Tactics.v
./Core/Completeness/LogicalRelation.v
-./Core/Completeness/FunctionCases.v
./Core/Completeness/TermStructureCases.v
./Core/Completeness/UniverseCases.v
./Core/Completeness/VariableCases.v
From 12f0cb063114679313fd1f8fdfb2bccdb5db2a82 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Tue, 21 May 2024 16:25:18 -0400
Subject: [PATCH 2/8] Fix a tactic
---
theories/Core/Semantic/PER/Lemmas.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 5fcbb9ef..351a2e3c 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -220,7 +220,7 @@ Ltac rewrite_relation_equivalence_left :=
Ltac rewrite_relation_equivalence_right :=
repeat match goal with
| H : ?R1 <~> ?R2 |- _ =>
- try setoid_rewrite H;
+ try setoid_rewrite <- H;
(on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite <- H in H');
let T := type of H in
fold (id T) in H
From 588d8293996cb30dbf54f0050a45a296ca623f84 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Tue, 21 May 2024 04:22:37 -0400
Subject: [PATCH 3/8] Finish context and subst
---
theories/Core/Completeness/ContextCases.v | 48 ++++
.../Core/Completeness/SubstitutionCases.v | 238 ++++++++++++++++++
theories/_CoqProject | 2 +
3 files changed, 288 insertions(+)
create mode 100644 theories/Core/Completeness/ContextCases.v
create mode 100644 theories/Core/Completeness/SubstitutionCases.v
diff --git a/theories/Core/Completeness/ContextCases.v b/theories/Core/Completeness/ContextCases.v
new file mode 100644
index 00000000..2129ea1f
--- /dev/null
+++ b/theories/Core/Completeness/ContextCases.v
@@ -0,0 +1,48 @@
+From Coq Require Import Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness.LogicalRelation System.
+Import Domain_Notations.
+
+Proposition valid_ctx_empty :
+ {{ ⊨ ⋅ }}.
+Proof.
+ do 2 econstructor.
+ apply Equivalence_Reflexive.
+Qed.
+
+Lemma rel_ctx_extend : forall {Γ Γ' A A' i},
+ {{ ⊨ Γ ≈ Γ' }} ->
+ {{ Γ ⊨ A ≈ A' : Type@i }} ->
+ {{ ⊨ Γ, A ≈ Γ', A' }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓΓ'] [env_relΓ].
+ pose (env_relΓ0 := env_relΓ).
+ destruct_conjs.
+ handle_per_ctx_env_irrel.
+ eexists.
+ econstructor; eauto with typeclass_instances.
+ - instantiate (1 := fun p p' (equiv_p_p' : env_relΓ p p') m m' =>
+ forall i a a' R,
+ {{ ⟦ A ⟧ p ↘ a }} ->
+ {{ ⟦ A' ⟧ p' ↘ a' }} ->
+ per_univ_elem i R a a' ->
+ R m m').
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ Type@i }}}); subst.
+ match goal with
+ | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
+ invert_per_univ_elem H;
+ apply_relation_equivalence;
+ clear_refl_eqs
+ end.
+ destruct_by_head rel_exp.
+ destruct_conjs.
+ econstructor; eauto.
+ apply -> per_univ_elem_morphism_iff; eauto.
+ split; intros; handle_per_univ_elem_irrel...
+ - apply Equivalence_Reflexive.
+Qed.
diff --git a/theories/Core/Completeness/SubstitutionCases.v b/theories/Core/Completeness/SubstitutionCases.v
new file mode 100644
index 00000000..c38d3952
--- /dev/null
+++ b/theories/Core/Completeness/SubstitutionCases.v
@@ -0,0 +1,238 @@
+From Coq Require Import Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness.ContextCases Completeness.LogicalRelation System.
+Import Domain_Notations.
+
+Lemma rel_subst_id : forall {Γ},
+ {{ ⊨ Γ }} ->
+ {{ Γ ⊨s Id ≈ Id : Γ }}.
+Proof with intuition.
+ intros * [].
+ eexists_rel_subst.
+ econstructor; only 1-2: repeat econstructor...
+Qed.
+
+Lemma rel_subst_weaken : forall {Γ A},
+ {{ ⊨ Γ, A }} ->
+ {{ Γ, A ⊨s Wk ≈ Wk : Γ }}.
+Proof with intuition.
+ intros * [env_relΓA].
+ inversion_by_head (per_ctx_env env_relΓA); subst.
+ eexists_rel_subst.
+ econstructor; only 1-2: repeat econstructor...
+Qed.
+
+Lemma rel_subst_compose_cong : forall {Γ τ τ' Γ' σ σ' Γ''},
+ {{ Γ ⊨s τ ≈ τ' : Γ' }} ->
+ {{ Γ' ⊨s σ ≈ σ' : Γ'' }} ->
+ {{ Γ ⊨s σ ∘ τ ≈ σ' ∘ τ' : Γ'' }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ [? [env_relΓ']]] [].
+ destruct_conjs.
+ pose (env_relΓ'0 := env_relΓ').
+ handle_per_ctx_env_irrel.
+ eexists_rel_subst.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ').
+ econstructor; only 1-2: repeat econstructor...
+Qed.
+
+Lemma rel_subst_extend_cong : forall {i Γ M M' σ σ' Δ A},
+ {{ Γ ⊨s σ ≈ σ' : Δ }} ->
+ {{ Δ ⊨ A : Type@i }} ->
+ {{ Γ ⊨ M ≈ M' : A[σ] }} ->
+ {{ Γ ⊨s σ ,, M ≈ σ' ,, M' : Δ, A }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ [? [env_relΔ]]] HA [].
+ destruct_conjs.
+ pose (env_relΓ0 := env_relΓ).
+ pose (env_relΔ0 := env_relΔ).
+ assert {{ ⊨ Δ, A }} as [env_relΔA] by (eapply rel_ctx_extend; eauto; eexists; eassumption).
+ destruct_conjs.
+ pose (env_relΔA0 := env_relΔA).
+ handle_per_ctx_env_irrel.
+ eexists_rel_subst.
+ inversion_by_head (per_ctx_env env_relΔA); subst.
+ handle_per_ctx_env_irrel.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
+ handle_per_univ_elem_irrel.
+ destruct_by_head rel_exp.
+ econstructor; only 1-2: repeat econstructor; eauto.
+Qed.
+
+Lemma rel_subst_id_compose_right : forall {Γ σ Δ},
+ {{ Γ ⊨s σ : Δ }} ->
+ {{ Γ ⊨s Id ∘ σ ≈ σ : Δ }}.
+Proof with intuition.
+ intros * [env_relΓ].
+ destruct_conjs.
+ eexists_rel_subst.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ econstructor; only 1-2: repeat econstructor...
+Qed.
+
+Lemma rel_subst_id_compose_left : forall {Γ σ Δ},
+ {{ Γ ⊨s σ : Δ }} ->
+ {{ Γ ⊨s σ ∘ Id ≈ σ : Δ }}.
+Proof with intuition.
+ intros * [env_relΓ].
+ destruct_conjs.
+ eexists_rel_subst.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ econstructor; only 1-2: repeat econstructor...
+Qed.
+
+Lemma rel_subst_compose_assoc : forall {Γ σ Γ' σ' Γ'' σ'' Γ'''},
+ {{ Γ' ⊨s σ : Γ }} ->
+ {{ Γ'' ⊨s σ' : Γ' }} ->
+ {{ Γ''' ⊨s σ'' : Γ'' }} ->
+ {{ Γ''' ⊨s (σ ∘ σ') ∘ σ'' ≈ σ ∘ (σ' ∘ σ'') : Γ }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ' [? [env_relΓ]]] [env_relΓ'' [? []]] [env_relΓ'''].
+ destruct_conjs.
+ pose (env_relΓ'0 := env_relΓ').
+ pose (env_relΓ''0 := env_relΓ'').
+ handle_per_ctx_env_irrel.
+ eexists_rel_subst.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ''').
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ'').
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ').
+ econstructor; only 1-2: repeat econstructor...
+Qed.
+
+Lemma rel_subst_extend_compose : forall {Γ τ Γ' M σ Γ'' A i},
+ {{ Γ' ⊨s σ : Γ'' }} ->
+ {{ Γ'' ⊨ A : Type@i }} ->
+ {{ Γ' ⊨ M : A[σ] }} ->
+ {{ Γ ⊨s τ : Γ' }} ->
+ {{ Γ ⊨s (σ ,, M) ∘ τ ≈ (σ ∘ τ) ,, M[τ] : Γ'', A }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ' [? [env_relΓ'']]] HA [] [env_relΓ].
+ destruct_conjs.
+ pose (env_relΓ'0 := env_relΓ').
+ pose (env_relΓ''0 := env_relΓ'').
+ assert {{ ⊨ Γ'', A }} as [env_relΓ''A] by (eapply rel_ctx_extend; eauto; eexists; eassumption).
+ destruct_conjs.
+ pose (env_relΓ''A0 := env_relΓ''A).
+ handle_per_ctx_env_irrel.
+ eexists_rel_subst.
+ inversion_by_head (per_ctx_env env_relΓ''A); subst.
+ handle_per_ctx_env_irrel.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ').
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
+ handle_per_univ_elem_irrel.
+ destruct_by_head rel_exp.
+ econstructor; only 1-2: repeat econstructor; try eexists...
+Qed.
+
+Lemma rel_subst_p_extend : forall {Γ' M σ Γ A},
+ {{ Γ' ⊨s σ : Γ }} ->
+ {{ Γ' ⊨ M : A[σ] }} ->
+ {{ Γ' ⊨s Wk ∘ (σ ,, M) ≈ σ : Γ }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ' [? [env_relΓ]]] [].
+ destruct_conjs.
+ pose (env_relΓ0 := env_relΓ).
+ pose (env_relΓ'0 := env_relΓ').
+ handle_per_ctx_env_irrel.
+ eexists_rel_subst.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ').
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
+ handle_per_univ_elem_irrel.
+ destruct_by_head rel_exp.
+ econstructor; only 1-2: repeat econstructor...
+Qed.
+
+Lemma rel_subst_extend : forall {Γ' σ Γ A},
+ {{ Γ' ⊨s σ : Γ, A }} ->
+ {{ Γ' ⊨s σ ≈ (Wk ∘ σ) ,, #0[σ] : Γ, A }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ' [? [env_relΓA]]].
+ destruct_conjs.
+ pose (env_relΓA0 := env_relΓA).
+ pose (env_relΓ'0 := env_relΓ').
+ inversion_by_head (per_ctx_env env_relΓA); subst.
+ rename tail_rel into env_relΓ.
+ handle_per_ctx_env_irrel.
+ eexists_rel_subst.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ').
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ econstructor; only 1-2: repeat econstructor; try eexists...
+Qed.
+
+Lemma rel_subst_sym : forall {Γ σ σ' Δ},
+ {{ Γ ⊨s σ ≈ σ' : Δ }} ->
+ {{ Γ ⊨s σ' ≈ σ : Δ }}.
+Proof with intuition.
+ intros * [env_relΓ].
+ destruct_conjs.
+ eexists_rel_subst.
+ intros.
+ assert (env_relΓ p' p) by (symmetry; eassumption).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ econstructor; only 1-2: repeat econstructor; try symmetry...
+Qed.
+
+Lemma rel_subst_trans : forall {Γ σ σ' σ'' Δ},
+ {{ Γ ⊨s σ ≈ σ' : Δ }} ->
+ {{ Γ ⊨s σ' ≈ σ'' : Δ }} ->
+ {{ Γ ⊨s σ ≈ σ'' : Δ }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ] [].
+ destruct_conjs.
+ pose (env_relΓ0 := env_relΓ).
+ handle_per_ctx_env_irrel.
+ eexists_rel_subst.
+ intros.
+ assert (env_relΓ p' p') by (etransitivity; [symmetry |]; eassumption).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ functional_eval_rewrite_clear.
+ econstructor; only 1-2: repeat econstructor; try etransitivity...
+Qed.
+
+Lemma rel_subst_conv : forall {Γ σ σ' Δ Δ'},
+ {{ Γ ⊨s σ ≈ σ' : Δ }} ->
+ {{ ⊨ Δ ≈ Δ' }} ->
+ {{ Γ ⊨s σ ≈ σ' : Δ' }}.
+Proof with intuition.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓ [? [env_relΔ]]] [].
+ destruct_conjs.
+ pose (env_relΔ0 := env_relΔ).
+ handle_per_ctx_env_irrel.
+ assert {{ EF Δ' ≈ Δ' ∈ per_ctx_env ↘ env_relΔ }} by (etransitivity; [symmetry |]; eassumption).
+ eexists_rel_subst.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ econstructor; only 1-2: repeat econstructor...
+Qed.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index a13a6832..f4b23c16 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -4,11 +4,13 @@
./Core/Axioms.v
./Core/Base.v
+./Core/Completeness/ContextCases.v
./Core/Completeness/FunctionCases.v
./Core/Completeness/LogicalRelation/Definitions.v
./Core/Completeness/LogicalRelation/Lemmas.v
./Core/Completeness/LogicalRelation/Tactics.v
./Core/Completeness/LogicalRelation.v
+./Core/Completeness/SubstitutionCases.v
./Core/Completeness/TermStructureCases.v
./Core/Completeness/UniverseCases.v
./Core/Completeness/VariableCases.v
From 268068e5bd5cd940706152067acc5a72f4cdb13d Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Tue, 21 May 2024 04:22:47 -0400
Subject: [PATCH 4/8] Add some cases for nat
---
theories/Core/Completeness/NatCases.v | 108 ++++++++++++++++++++++++++
theories/_CoqProject | 1 +
2 files changed, 109 insertions(+)
create mode 100644 theories/Core/Completeness/NatCases.v
diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v
new file mode 100644
index 00000000..fc12a768
--- /dev/null
+++ b/theories/Core/Completeness/NatCases.v
@@ -0,0 +1,108 @@
+From Coq Require Import Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness.LogicalRelation System.
+Import Domain_Notations.
+
+Lemma valid_exp_nat : forall {Γ i},
+ {{ ⊨ Γ }} ->
+ {{ Γ ⊨ ℕ : Type@i }}.
+Proof.
+ intros * [env_relΓ].
+ eexists_rel_exp.
+ intros.
+ eexists (per_univ _).
+ split; [> econstructor; only 1-2: repeat econstructor ..]; [| eexists];
+ per_univ_elem_econstructor; eauto; apply Equivalence_Reflexive.
+Qed.
+
+Lemma rel_exp_nat_sub : forall {Γ σ i Δ},
+ {{ Γ ⊨s σ : Δ }} ->
+ {{ Γ ⊨ ℕ[σ] ≈ ℕ : Type@i }}.
+Proof.
+ intros * [env_relΓ].
+ destruct_conjs.
+ eexists_rel_exp.
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ eexists (per_univ _).
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eauto; [| eexists];
+ per_univ_elem_econstructor; eauto; apply Equivalence_Reflexive.
+Qed.
+
+Lemma valid_exp_zero : forall {Γ},
+ {{ ⊨ Γ }} ->
+ {{ Γ ⊨ zero : ℕ }}.
+Proof.
+ intros * [env_relΓ].
+ unshelve eexists_rel_exp; [constructor |].
+ intros.
+ eexists.
+ split; [> econstructor; only 1-2: repeat econstructor ..].
+ - per_univ_elem_econstructor; reflexivity.
+ - econstructor.
+Qed.
+
+Lemma rel_exp_zero_sub : forall {Γ σ Δ},
+ {{ Γ ⊨s σ : Δ }} ->
+ {{ Γ ⊨ zero[σ] ≈ zero : ℕ }}.
+Proof.
+ intros * [env_relΓ].
+ destruct_conjs.
+ unshelve eexists_rel_exp; [constructor |].
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ eexists.
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eauto.
+ - per_univ_elem_econstructor; reflexivity.
+ - econstructor.
+Qed.
+
+Lemma rel_exp_succ_sub : forall {Γ σ Δ M},
+ {{ Γ ⊨s σ : Δ }} ->
+ {{ Δ ⊨ M : ℕ }} ->
+ {{ Γ ⊨ (succ M)[σ] ≈ succ (M[σ]) : ℕ }}.
+Proof.
+ intros * [env_relΓ] [env_relΔ].
+ destruct_conjs.
+ pose (env_relΔ0 := env_relΔ).
+ handle_per_ctx_env_irrel.
+ unshelve eexists_rel_exp; [constructor |].
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ (on_all_hyp: destruct_rel_by_assumption env_relΔ).
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ ℕ }}}); subst.
+ match goal with
+ | H : per_univ_elem _ _ d{{{ ℕ }}} d{{{ ℕ }}} |- _ =>
+ invert_per_univ_elem H;
+ apply_relation_equivalence
+ end.
+ destruct_by_head rel_exp.
+ eexists.
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eauto.
+ - per_univ_elem_econstructor; reflexivity.
+ - econstructor; eassumption.
+Qed.
+
+Lemma rel_exp_succ_cong : forall {Γ M M'},
+ {{ Γ ⊨ M ≈ M' : ℕ }} ->
+ {{ Γ ⊨ succ M ≈ succ M' : ℕ }}.
+Proof.
+ intros * [env_relΓ].
+ destruct_conjs.
+ unshelve eexists_rel_exp; [constructor |].
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ ℕ }}}); subst.
+ match goal with
+ | H : per_univ_elem _ _ d{{{ ℕ }}} d{{{ ℕ }}} |- _ =>
+ invert_per_univ_elem H;
+ apply_relation_equivalence
+ end.
+ destruct_by_head rel_exp.
+ eexists.
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eauto.
+ - per_univ_elem_econstructor; reflexivity.
+ - econstructor; eassumption.
+Qed.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index f4b23c16..d5e5a6d9 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -10,6 +10,7 @@
./Core/Completeness/LogicalRelation/Lemmas.v
./Core/Completeness/LogicalRelation/Tactics.v
./Core/Completeness/LogicalRelation.v
+./Core/Completeness/NatCases.v
./Core/Completeness/SubstitutionCases.v
./Core/Completeness/TermStructureCases.v
./Core/Completeness/UniverseCases.v
From 2093d66c9075dbbe4e601080fc744a9b773bcd07 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Tue, 21 May 2024 14:59:00 -0400
Subject: [PATCH 5/8] Improve completeness proofs
---
theories/Core/Completeness/ContextCases.v | 8 +-
theories/Core/Completeness/FunctionCases.v | 96 ++++++-------------
.../Completeness/LogicalRelation/Tactics.v | 12 +++
theories/Core/Completeness/NatCases.v | 14 +--
.../Core/Completeness/TermStructureCases.v | 13 +--
theories/Core/Completeness/UniverseCases.v | 3 +-
theories/Core/Completeness/VariableCases.v | 9 +-
theories/LibTactics.v | 16 +++-
8 files changed, 64 insertions(+), 107 deletions(-)
diff --git a/theories/Core/Completeness/ContextCases.v b/theories/Core/Completeness/ContextCases.v
index 2129ea1f..4221c87c 100644
--- a/theories/Core/Completeness/ContextCases.v
+++ b/theories/Core/Completeness/ContextCases.v
@@ -32,13 +32,7 @@ Proof with intuition.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence;
- clear_refl_eqs
- end.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
destruct_conjs.
econstructor; eauto.
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
index 7e142ee5..e43f20bb 100644
--- a/theories/Core/Completeness/FunctionCases.v
+++ b/theories/Core/Completeness/FunctionCases.v
@@ -31,7 +31,7 @@ Proof with intuition.
pose proof (@relation_equivalence_pointwise env).
intros.
subst.
- (on_all_hyp: fun H => pose proof (H _ _ equiv_c_c')).
+ (on_all_hyp: destruct_rel_by_assumption (head_rel p p' equiv_p_p')).
destruct_by_head rel_exp.
econstructor; mauto.
destruct_by_head per_univ.
@@ -56,17 +56,11 @@ Proof with intuition.
intros.
(on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence;
- clear_refl_eqs
- end.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
destruct_conjs.
handle_per_univ_elem_irrel.
- exists (per_univ i).
+ eexists (per_univ _).
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
eexists.
per_univ_elem_econstructor; eauto with typeclass_instances.
@@ -76,16 +70,10 @@ Proof with intuition.
clear dependent c'.
intros.
extract_output_info_with p c p' c' env_relΓA.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence;
- clear_refl_eqs
- end.
+ invert_rel_typ_body.
econstructor...
+ reflexivity.
- - (* `reflexivity` does not work as it uses a "wrong" instance. *)
+ - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
apply Equivalence_Reflexive.
Qed.
@@ -108,18 +96,12 @@ Proof with intuition.
assert {{ Dom o' ≈ o' ∈ tail_rel }} by (etransitivity; [symmetry|]; eassumption).
(on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence;
- clear_refl_eqs
- end.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
destruct_conjs.
handle_per_univ_elem_irrel.
- eexists; split;
- [> econstructor; only 1-2: repeat econstructor; eauto ..].
+ eexists.
+ split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
eexists.
per_univ_elem_econstructor; eauto with typeclass_instances.
- intros.
@@ -128,17 +110,12 @@ Proof with intuition.
clear dependent c'.
intros.
extract_output_info_with o c o' c' env_relΔA.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence;
- clear_refl_eqs
- end.
+ invert_rel_typ_body.
+ destruct_conjs.
econstructor; eauto.
repeat econstructor...
+ reflexivity.
- - (* `reflexivity` does not work as it uses a "wrong" instance. *)
+ - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
apply Equivalence_Reflexive.
Qed.
@@ -159,18 +136,13 @@ Proof with intuition.
intros.
(on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence;
- clear_refl_eqs
- end.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
functional_eval_rewrite_clear.
- eexists ?[elem_rel].
+ eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
- - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |]; eauto with typeclass_instances.
+ - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |];
+ eauto with typeclass_instances.
+ intros.
eapply rel_exp_pi_core; eauto.
* clear dependent c.
@@ -207,9 +179,10 @@ Proof with intuition.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
(on_all_hyp: destruct_rel_by_assumption tail_rel).
- eexists ?[elem_rel].
+ eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
- - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |]; eauto with typeclass_instances.
+ - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |];
+ eauto with typeclass_instances.
+ intros.
eapply rel_exp_pi_core; eauto.
* clear dependent c.
@@ -245,22 +218,22 @@ Proof with intuition.
assert (equiv_p'_p' : env_relΓ p' p') by (etransitivity; [symmetry |]; eauto).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Π A B }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ Π ~?a ~?p B }}} d{{{ Π ~?a' ~?p' B }}} |- _ =>
- invert_per_univ_elem H
- end.
+ functional_eval_rewrite_clear.
+ invert_rel_typ_body.
handle_per_univ_elem_irrel.
destruct_by_head rel_exp.
functional_eval_rewrite_clear.
- assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eauto).
+ assert (in_rel0 m1 m2) by (etransitivity; [| symmetry]; eauto).
+ assert (in_rel m1 m'2) by intuition.
+ assert (in_rel m1 m2) by intuition.
(on_all_hyp: destruct_rel_by_assumption in_rel).
- (on_all_hyp_rev: destruct_rel_by_assumption in_rel).
+ (on_all_hyp: destruct_rel_by_assumption in_rel0).
+ (on_all_hyp_rev: destruct_rel_by_assumption in_rel0).
handle_per_univ_elem_irrel.
- eexists ?[elem_rel].
+ eexists.
split; [> econstructor; only 1-2: econstructor ..].
1,3: repeat econstructor.
- all: eauto.
+ all: intuition.
Qed.
Lemma rel_exp_app_sub : forall {Γ σ Δ M A B N},
@@ -281,16 +254,12 @@ Proof with intuition.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
(on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Π A B }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ Π ~?a ~?p B }}} d{{{ Π ~?a' ~?p' B }}} |- _ =>
- invert_per_univ_elem H
- end.
+ invert_rel_typ_body.
handle_per_univ_elem_irrel.
destruct_by_head rel_exp.
functional_eval_rewrite_clear.
(on_all_hyp_rev: destruct_rel_by_assumption in_rel).
- eexists ?[elem_rel].
+ eexists.
split; [> econstructor; only 1-2: econstructor ..].
1,3,8,9: repeat econstructor.
15: econstructor.
@@ -335,12 +304,7 @@ Proof with intuition.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Π A B }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ Π ~?a ~?p B }}} d{{{ Π ~?a' ~?p' B }}} |- _ =>
- invert_per_univ_elem H
- end.
- apply_relation_equivalence.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v
index 89400fc2..439d2aec 100644
--- a/theories/Core/Completeness/LogicalRelation/Tactics.v
+++ b/theories/Core/Completeness/LogicalRelation/Tactics.v
@@ -1,3 +1,8 @@
+From Coq Require Import Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Evaluation PER System.
+Import Domain_Notations.
+
Ltac eexists_rel_exp :=
eexists;
eexists; [eassumption |];
@@ -8,3 +13,10 @@ Ltac eexists_rel_subst :=
eexists; [eassumption |];
eexists;
eexists; [eassumption |].
+
+Ltac invert_rel_typ_body :=
+ dir_inversion_by_head eval_exp; subst;
+ match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H); subst;
+ clear_refl_eqs;
+ handle_per_univ_elem_irrel;
+ try rewrite <- per_univ_elem_equation_1 in *.
diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v
index fc12a768..46b015b9 100644
--- a/theories/Core/Completeness/NatCases.v
+++ b/theories/Core/Completeness/NatCases.v
@@ -71,12 +71,7 @@ Proof.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
(on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ ℕ }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ ℕ }}} d{{{ ℕ }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence
- end.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
eexists.
split; [> econstructor; only 1-2: repeat econstructor ..]; eauto.
@@ -94,12 +89,7 @@ Proof.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ ℕ }}}); subst.
- match goal with
- | H : per_univ_elem _ _ d{{{ ℕ }}} d{{{ ℕ }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence
- end.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
eexists.
split; [> econstructor; only 1-2: repeat econstructor ..]; eauto.
diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v
index db0a81b7..fe408384 100644
--- a/theories/Core/Completeness/TermStructureCases.v
+++ b/theories/Core/Completeness/TermStructureCases.v
@@ -92,14 +92,7 @@ Proof.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_exp.
destruct_by_head rel_typ.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- handle_per_univ_elem_irrel.
- match goal with
- | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
- invert_per_univ_elem H;
- apply_relation_equivalence;
- clear_refl_eqs
- end.
+ invert_rel_typ_body.
destruct_conjs.
handle_per_univ_elem_irrel.
eexists.
@@ -179,9 +172,7 @@ Proof.
eexists_rel_exp.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
- evar (j : nat).
- eexists (per_univ j).
- subst j.
+ eexists (per_univ _).
split.
+ econstructor; only 1-2: repeat econstructor; try eassumption.
per_univ_elem_econstructor; eauto.
diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v
index 62c8b4ec..6a42d11a 100644
--- a/theories/Core/Completeness/UniverseCases.v
+++ b/theories/Core/Completeness/UniverseCases.v
@@ -43,8 +43,7 @@ Proof.
(on_all_hyp: destruct_rel_by_assumption env_rel).
inversion_by_head rel_typ.
inversion_by_head rel_exp.
- inversion_by_head (eval_exp {{{ Type@i }}}); subst.
- match_by_head per_univ_elem invert_per_univ_elem; subst.
+ invert_rel_typ_body.
handle_per_univ_elem_irrel.
destruct_conjs.
match_by_head per_univ_elem ltac:(fun H => apply per_univ_elem_cumu in H).
diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v
index c47beb3c..cfa6f568 100644
--- a/theories/Core/Completeness/VariableCases.v
+++ b/theories/Core/Completeness/VariableCases.v
@@ -27,7 +27,7 @@ Proof with solve [repeat econstructor; mauto].
- split; econstructor...
- destruct_by_head rel_typ.
destruct_by_head rel_exp.
- inversion_by_head (eval_exp {{{ #n }}}); subst.
+ dir_inversion_by_head eval_exp; subst.
split; econstructor; simpl...
Qed.
@@ -57,7 +57,7 @@ Proof.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
- inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
+ dir_inversion_by_head eval_exp; subst.
functional_eval_rewrite_clear.
eexists.
split; [> econstructor; only 1-2: repeat econstructor ..]; eassumption.
@@ -83,8 +83,7 @@ Proof.
(on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
- inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
- inversion_by_head (eval_exp {{{ # x }}}); subst.
+ dir_inversion_by_head eval_exp; subst.
functional_eval_rewrite_clear.
eexists.
split; [> econstructor; only 1-2: repeat econstructor ..]; eassumption.
@@ -107,7 +106,7 @@ Proof.
(on_all_hyp: destruct_rel_by_assumption tail_rel).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
- inversion_by_head (eval_exp {{{ #x }}}); subst.
+ dir_inversion_by_head eval_exp; subst.
eexists.
split; [> econstructor; only 1-2: repeat econstructor ..]; eassumption.
Qed.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 5f7225e4..6b7ae520 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -98,12 +98,17 @@ Ltac clear_dups :=
repeat find_dup_hyp ltac:(fun H H' _ => clear H || clear H')
ltac:(idtac).
-Ltac progressive_invert H :=
+Ltac directed tac :=
let ng := numgoals in
- (* dependent destruction is more general than inversion *)
- dependent destruction H;
+ tac;
let ng' := numgoals in
- guard ng = ng'.
+ guard ng' <= ng.
+
+Tactic Notation "directed" tactic2(tac) := directed tac.
+
+Ltac progressive_invert H :=
+ (* dependent destruction is more general than inversion *)
+ directed dependent destruction H.
Ltac clean_replace_by exp0 exp1 tac :=
tryif unify exp0 exp1
@@ -133,8 +138,11 @@ Ltac match_by_head1 head tac :=
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 dir_inversion_by_head head := match_by_head head ltac:(fun H => directed inversion H).
Ltac inversion_clear_by_head head := match_by_head head ltac:(fun H => inversion_clear H).
+Ltac dir_inversion_clear_by_head head := match_by_head head ltac:(fun H => directed inversion_clear H).
Ltac destruct_by_head head := match_by_head head ltac:(fun H => destruct H).
+Ltac dir_destruct_by_head head := match_by_head head ltac:(fun H => directed destruct H).
(** McLTT automation *)
From 501808eed8c72175a008324af6288443ff5b539e Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Tue, 21 May 2024 18:50:43 -0400
Subject: [PATCH 6/8] Update proofs
---
theories/Core/Completeness/FunctionCases.v | 45 ++++++++++---------
.../Core/Completeness/SubstitutionCases.v | 12 +++--
.../Core/Completeness/TermStructureCases.v | 4 +-
theories/Core/Completeness/UniverseCases.v | 13 +++---
theories/Core/Completeness/VariableCases.v | 6 ++-
theories/Core/Semantic/PER/Lemmas.v | 34 ++++++++++++++
6 files changed, 79 insertions(+), 35 deletions(-)
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
index e43f20bb..5fefea0d 100644
--- a/theories/Core/Completeness/FunctionCases.v
+++ b/theories/Core/Completeness/FunctionCases.v
@@ -48,13 +48,13 @@ Proof with intuition.
pose proof (@relation_equivalence_pointwise env).
intros * [env_relΓ] [env_relΓA].
destruct_conjs.
- pose (env_relΓ0 := env_relΓ).
pose (env_relΓA0 := env_relΓA).
- inversion_by_head (per_ctx_env env_relΓA); subst.
- handle_per_ctx_env_irrel.
+ match_by_head (per_ctx_env env_relΓA)
+ ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ destruct_conjs.
eexists_rel_exp.
intros.
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
invert_rel_typ_body.
destruct_by_head rel_exp.
@@ -85,16 +85,18 @@ Lemma rel_exp_pi_sub : forall {i Γ σ Δ A B},
Proof with intuition.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [env_relΓ] [] [env_relΔA].
+ intros * [env_relΓ] [env_relΔ] [env_relΔA].
destruct_conjs.
pose (env_relΔA0 := env_relΔA).
- inversion_by_head (per_ctx_env env_relΔA); subst.
+ match_by_head (per_ctx_env env_relΔA)
+ ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ destruct_conjs.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
- assert {{ Dom o' ≈ o' ∈ tail_rel }} by (etransitivity; [symmetry|]; eassumption).
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ assert {{ Dom o' ≈ o' ∈ env_relΔ }} by (etransitivity; [symmetry|]; eassumption).
+ (on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
invert_rel_typ_body.
destruct_by_head rel_exp.
@@ -128,13 +130,14 @@ Proof with intuition.
pose proof (@relation_equivalence_pointwise env).
intros * [env_relΓ] [env_relΓA].
destruct_conjs.
- pose (env_relΓ0 := env_relΓ).
pose (env_relΓA0 := env_relΓA).
- inversion_by_head (per_ctx_env env_relΓA); subst.
+ match_by_head (per_ctx_env env_relΓA)
+ ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ destruct_conjs.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
invert_rel_typ_body.
destruct_by_head rel_exp.
@@ -169,16 +172,17 @@ Lemma rel_exp_fn_sub : forall {Γ σ Δ A M B},
Proof with intuition.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [env_relΓ] [env_relΔA].
+ intros * [env_relΓ [? [env_relΔ]]] [env_relΔA].
destruct_conjs.
- pose (env_relΓ0 := env_relΓ).
pose (env_relΔA0 := env_relΔA).
- inversion_by_head (per_ctx_env env_relΔA); subst.
+ match_by_head (per_ctx_env env_relΔA)
+ ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ destruct_conjs.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ (on_all_hyp: destruct_rel_by_assumption env_relΔ).
eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
- per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |];
@@ -209,7 +213,7 @@ Lemma rel_exp_app_cong : forall {Γ M M' A B N N'},
Proof with intuition.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [env_relΓ] [env_relΓ'].
+ intros * [env_relΓ] [].
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
handle_per_ctx_env_irrel.
@@ -244,7 +248,7 @@ Lemma rel_exp_app_sub : forall {Γ σ Δ M A B N},
Proof with intuition.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [env_relΓ] [env_relΔ] [env_relΔ'].
+ intros * [env_relΓ] [env_relΔ] [].
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
pose (env_relΔ0 := env_relΔ).
@@ -275,13 +279,14 @@ Proof with intuition.
pose proof (@relation_equivalence_pointwise env).
intros * [env_relΓA] [env_relΓ].
destruct_conjs.
- pose (env_relΓ0 := env_relΓ).
pose (env_relΓA0 := env_relΓA).
- inversion_by_head (per_ctx_env env_relΓA); subst.
+ match_by_head (per_ctx_env env_relΓA)
+ ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ destruct_conjs.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
handle_per_univ_elem_irrel.
destruct_by_head rel_exp.
diff --git a/theories/Core/Completeness/SubstitutionCases.v b/theories/Core/Completeness/SubstitutionCases.v
index c38d3952..88a841bc 100644
--- a/theories/Core/Completeness/SubstitutionCases.v
+++ b/theories/Core/Completeness/SubstitutionCases.v
@@ -57,11 +57,13 @@ Proof with intuition.
pose (env_relΔA0 := env_relΔA).
handle_per_ctx_env_irrel.
eexists_rel_subst.
- inversion_by_head (per_ctx_env env_relΔA); subst.
+ match_by_head (per_ctx_env env_relΔA)
+ ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ destruct_conjs.
handle_per_ctx_env_irrel.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ (on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
handle_per_univ_elem_irrel.
@@ -132,12 +134,14 @@ Proof with intuition.
pose (env_relΓ''A0 := env_relΓ''A).
handle_per_ctx_env_irrel.
eexists_rel_subst.
- inversion_by_head (per_ctx_env env_relΓ''A); subst.
+ match_by_head (per_ctx_env env_relΓ''A)
+ ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ destruct_conjs.
handle_per_ctx_env_irrel.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
(on_all_hyp: destruct_rel_by_assumption env_relΓ').
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ'').
destruct_by_head rel_typ.
inversion_by_head (eval_exp {{{ A[σ] }}}); subst.
handle_per_univ_elem_irrel.
diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v
index fe408384..f28b1a80 100644
--- a/theories/Core/Completeness/TermStructureCases.v
+++ b/theories/Core/Completeness/TermStructureCases.v
@@ -82,7 +82,7 @@ Lemma rel_exp_conv : forall {Γ M M' A A' i},
Proof.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [env_relΓ] [env_relΓ'].
+ intros * [env_relΓ] [].
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
handle_per_ctx_env_irrel.
@@ -127,7 +127,7 @@ Lemma rel_exp_trans : forall {Γ M1 M2 M3 A},
Proof.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [env_relΓ] [env_relΓ'].
+ intros * [env_relΓ] [].
destruct_conjs.
pose (env_relΓ0 := env_relΓ).
handle_per_ctx_env_irrel.
diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v
index 6a42d11a..8011da0b 100644
--- a/theories/Core/Completeness/UniverseCases.v
+++ b/theories/Core/Completeness/UniverseCases.v
@@ -19,12 +19,12 @@ Lemma rel_exp_typ_sub : forall {i Γ σ Δ},
{{ Γ ⊨s σ : Δ }} ->
{{ Γ ⊨ Type@i[σ] ≈ Type@i : Type@(S i) }}.
Proof.
- intros * [env_rel].
+ intros * [env_relΓ].
destruct_conjs.
eexists_rel_exp.
intros.
eexists (per_univ _).
- (on_all_hyp: destruct_rel_by_assumption env_rel).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
split; [> econstructor; only 1-2: repeat econstructor; eauto ..]; [| eexists (per_univ _)];
per_univ_elem_econstructor; eauto; apply Equivalence_Reflexive.
Qed.
@@ -35,19 +35,18 @@ Lemma rel_exp_cumu : forall {i Γ A A'},
Proof.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
- intros * [env_rel].
+ intros * [env_relΓ].
destruct_conjs.
eexists_rel_exp.
intros.
- eexists (per_univ _).
- (on_all_hyp: destruct_rel_by_assumption env_rel).
+ exists (per_univ (S i)).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
inversion_by_head rel_typ.
inversion_by_head rel_exp.
invert_rel_typ_body.
- handle_per_univ_elem_irrel.
destruct_conjs.
match_by_head per_univ_elem ltac:(fun H => apply per_univ_elem_cumu in H).
- split; [> econstructor; only 1-2: repeat econstructor; eauto ..]; [| eexists; eauto].
+ split; [> econstructor; only 1-2: repeat econstructor ..]; eauto; [| eexists; eauto].
per_univ_elem_econstructor; eauto.
reflexivity.
Qed.
diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v
index cfa6f568..8442e1db 100644
--- a/theories/Core/Completeness/VariableCases.v
+++ b/theories/Core/Completeness/VariableCases.v
@@ -102,8 +102,10 @@ Proof.
destruct_conjs.
eexists_rel_exp.
apply_relation_equivalence.
- intros ? ? [].
- (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ intros.
+ destruct_conjs.
+ rename tail_rel into env_relΓ.
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
dir_inversion_by_head eval_exp; subst.
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 351a2e3c..98e10411 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -733,3 +733,37 @@ Proof.
- auto using (per_env_sym _ _ _ _ _ H).
- eauto using (per_env_trans _ _ _ _ _ _ H).
Qed.
+
+Lemma per_ctx_env_cons_clear_inversion : forall {Γ Γ' env_relΓ A A' env_relΓA},
+ {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ env_relΓ }} ->
+ {{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ env_relΓA }} ->
+ exists i (head_rel : forall {p p'} (equiv_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' (head_rel equiv_p_p')) /\
+ (env_relΓA <~> fun p p' =>
+ exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ env_relΓ }}),
+ {{ Dom ~(p 0) ≈ ~(p' 0) ∈ head_rel equiv_p_drop_p'_drop }}).
+Proof with intuition.
+ intros * HΓ HΓA.
+ inversion HΓA; subst.
+ handle_per_ctx_env_irrel.
+ eexists.
+ eexists.
+ split; intros.
+ - instantiate (1 := fun p p' (equiv_p_p' : env_relΓ p p') m m' =>
+ forall a a' R,
+ {{ ⟦ A ⟧ p ↘ a }} ->
+ {{ ⟦ A' ⟧ p' ↘ a' }} ->
+ {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
+ {{ Dom m ≈ m' ∈ R }}).
+ assert (tail_rel p p') by intuition.
+ (on_all_hyp: destruct_rel_by_assumption tail_rel).
+ econstructor; eauto.
+ apply -> per_univ_elem_morphism_iff; eauto.
+ split; intros; handle_per_univ_elem_irrel...
+ - intros o o'.
+ split; intros; destruct_conjs;
+ assert {{ Dom o ↯ ≈ o' ↯ ∈ tail_rel }} by intuition;
+ (on_all_hyp: destruct_rel_by_assumption tail_rel);
+ eexists; intros; handle_per_univ_elem_irrel; intuition.
+Qed.
From eba9e90b3a33de119435da293e776f3d232f18f7 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Wed, 22 May 2024 14:52:32 -0400
Subject: [PATCH 7/8] Update PER tactic
---
theories/Core/Completeness/ContextCases.v | 12 +-
theories/Core/Completeness/FunctionCases.v | 72 ++++-----
.../Completeness/LogicalRelation/Tactics.v | 1 +
.../Core/Completeness/SubstitutionCases.v | 6 +-
theories/Core/Semantic/PER/CoreTactics.v | 4 +-
theories/Core/Semantic/PER/Lemmas.v | 147 +++++++++++++-----
6 files changed, 150 insertions(+), 92 deletions(-)
diff --git a/theories/Core/Completeness/ContextCases.v b/theories/Core/Completeness/ContextCases.v
index 4221c87c..0855e47b 100644
--- a/theories/Core/Completeness/ContextCases.v
+++ b/theories/Core/Completeness/ContextCases.v
@@ -22,12 +22,10 @@ Proof with intuition.
destruct_conjs.
handle_per_ctx_env_irrel.
eexists.
- econstructor; eauto with typeclass_instances.
+ per_ctx_env_econstructor; eauto.
- instantiate (1 := fun p p' (equiv_p_p' : env_relΓ p p') m m' =>
- forall i a a' R,
- {{ ⟦ A ⟧ p ↘ a }} ->
- {{ ⟦ A' ⟧ p' ↘ a' }} ->
- per_univ_elem i R a a' ->
+ forall i R,
+ rel_typ i A p A' p' R ->
R m m').
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -37,6 +35,8 @@ Proof with intuition.
destruct_conjs.
econstructor; eauto.
apply -> per_univ_elem_morphism_iff; eauto.
- split; intros; handle_per_univ_elem_irrel...
+ split; intros; destruct_by_head rel_typ; handle_per_univ_elem_irrel...
+ eapply H12.
+ econstructor...
- apply Equivalence_Reflexive.
Qed.
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
index 5fefea0d..8fe562cf 100644
--- a/theories/Core/Completeness/FunctionCases.v
+++ b/theories/Core/Completeness/FunctionCases.v
@@ -12,31 +12,28 @@ Ltac extract_output_info_with p c p' c' env_rel :=
destruct_by_head rel_typ;
destruct_by_head rel_exp).
-Lemma rel_exp_pi_core : forall {i p o B p' o' B'} {tail_rel : relation env}
- (head_rel : forall p p', {{ Dom p ≈ p' ∈ tail_rel }} -> relation domain)
- (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }})
- {out_rel},
+Lemma rel_exp_pi_core : forall {i o B o' B' R out_rel},
(forall c c',
- head_rel p p' equiv_p_p' c c' ->
+ R c c' ->
rel_exp B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (per_univ i)) ->
(* We use this equality to make unification on `out_rel` works *)
- (out_rel = fun c c' (equiv_c_c' : head_rel p p' equiv_p_p' c c') m m' =>
- forall b b' R,
- {{ ⟦ B ⟧ o ↦ c ↘ b }} ->
- {{ ⟦ B' ⟧ o' ↦ c' ↘ b' }} ->
- per_univ_elem i R b b' -> R m m') ->
- (forall c c' (equiv_c_c' : head_rel p p' equiv_p_p' c c'), rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (out_rel c c' equiv_c_c')).
+ (out_rel = fun c c' (equiv_c_c' : R c c') m m' =>
+ forall R',
+ rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} R' ->
+ R' m m') ->
+ (forall c c' (equiv_c_c' : R c c'), rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (out_rel c c' equiv_c_c')).
Proof with intuition.
pose proof (@relation_equivalence_pointwise domain).
pose proof (@relation_equivalence_pointwise env).
intros.
subst.
- (on_all_hyp: destruct_rel_by_assumption (head_rel p p' equiv_p_p')).
- destruct_by_head rel_exp.
+ (on_all_hyp: destruct_rel_by_assumption R).
econstructor; mauto.
destruct_by_head per_univ.
apply -> per_univ_elem_morphism_iff; eauto.
- split; intros; handle_per_univ_elem_irrel...
+ split; intros; destruct_by_head rel_typ; handle_per_univ_elem_irrel...
+ eapply H5.
+ econstructor...
Qed.
Lemma rel_exp_pi_cong : forall {i Γ A A' B B'},
@@ -49,9 +46,7 @@ Proof with intuition.
intros * [env_relΓ] [env_relΓA].
destruct_conjs.
pose (env_relΓA0 := env_relΓA).
- match_by_head (per_ctx_env env_relΓA)
- ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
- destruct_conjs.
+ match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
eexists_rel_exp.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -63,7 +58,7 @@ Proof with intuition.
eexists (per_univ _).
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
eexists.
- per_univ_elem_econstructor; eauto with typeclass_instances.
+ per_univ_elem_econstructor; eauto.
- intros.
eapply rel_exp_pi_core; eauto.
+ clear dependent c.
@@ -87,10 +82,9 @@ Proof with intuition.
pose proof (@relation_equivalence_pointwise env).
intros * [env_relΓ] [env_relΔ] [env_relΔA].
destruct_conjs.
+ pose (env_relΔ0 := env_relΔ).
pose (env_relΔA0 := env_relΔA).
- match_by_head (per_ctx_env env_relΔA)
- ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
- destruct_conjs.
+ match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
@@ -105,7 +99,7 @@ Proof with intuition.
eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
eexists.
- per_univ_elem_econstructor; eauto with typeclass_instances.
+ per_univ_elem_econstructor; eauto.
- intros.
eapply rel_exp_pi_core; eauto.
+ clear dependent c.
@@ -131,9 +125,7 @@ Proof with intuition.
intros * [env_relΓ] [env_relΓA].
destruct_conjs.
pose (env_relΓA0 := env_relΓA).
- match_by_head (per_ctx_env env_relΓA)
- ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
- destruct_conjs.
+ match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
@@ -144,8 +136,7 @@ Proof with intuition.
functional_eval_rewrite_clear.
eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
- - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |];
- eauto with typeclass_instances.
+ - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | |]; eauto.
+ intros.
eapply rel_exp_pi_core; eauto.
* clear dependent c.
@@ -162,6 +153,7 @@ Proof with intuition.
extract_output_info_with p c p' c' env_relΓA.
econstructor; only 1-2: repeat econstructor; eauto.
intros.
+ destruct_by_head rel_typ.
handle_per_univ_elem_irrel...
Qed.
@@ -175,9 +167,7 @@ Proof with intuition.
intros * [env_relΓ [? [env_relΔ]]] [env_relΔA].
destruct_conjs.
pose (env_relΔA0 := env_relΔA).
- match_by_head (per_ctx_env env_relΔA)
- ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
- destruct_conjs.
+ match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
@@ -185,8 +175,7 @@ Proof with intuition.
(on_all_hyp: destruct_rel_by_assumption env_relΔ).
eexists.
split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
- - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |];
- eauto with typeclass_instances.
+ - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | |]; eauto.
+ intros.
eapply rel_exp_pi_core; eauto.
* clear dependent c.
@@ -201,8 +190,9 @@ Proof with intuition.
apply Equivalence_Reflexive.
- intros ? **.
extract_output_info_with o c o' c' env_relΔA.
- econstructor; only 1-2: repeat econstructor; simpl; mauto.
+ econstructor; only 1-2: repeat econstructor; mauto.
intros.
+ destruct_by_head rel_typ.
handle_per_univ_elem_irrel...
Qed.
@@ -222,17 +212,14 @@ Proof with intuition.
assert (equiv_p'_p' : env_relΓ p' p') by (etransitivity; [symmetry |]; eauto).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
- functional_eval_rewrite_clear.
- invert_rel_typ_body.
handle_per_univ_elem_irrel.
+ invert_rel_typ_body.
destruct_by_head rel_exp.
functional_eval_rewrite_clear.
- assert (in_rel0 m1 m2) by (etransitivity; [| symmetry]; eauto).
+ rename x into in_rel.
+ assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eauto).
assert (in_rel m1 m'2) by intuition.
- assert (in_rel m1 m2) by intuition.
(on_all_hyp: destruct_rel_by_assumption in_rel).
- (on_all_hyp: destruct_rel_by_assumption in_rel0).
- (on_all_hyp_rev: destruct_rel_by_assumption in_rel0).
handle_per_univ_elem_irrel.
eexists.
split; [> econstructor; only 1-2: econstructor ..].
@@ -259,9 +246,8 @@ Proof with intuition.
(on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
invert_rel_typ_body.
- handle_per_univ_elem_irrel.
destruct_by_head rel_exp.
- functional_eval_rewrite_clear.
+ rename x into in_rel.
(on_all_hyp_rev: destruct_rel_by_assumption in_rel).
eexists.
split; [> econstructor; only 1-2: econstructor ..].
@@ -280,9 +266,7 @@ Proof with intuition.
intros * [env_relΓA] [env_relΓ].
destruct_conjs.
pose (env_relΓA0 := env_relΓA).
- match_by_head (per_ctx_env env_relΓA)
- ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
- destruct_conjs.
+ match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v
index 439d2aec..3c1e04c5 100644
--- a/theories/Core/Completeness/LogicalRelation/Tactics.v
+++ b/theories/Core/Completeness/LogicalRelation/Tactics.v
@@ -16,6 +16,7 @@ Ltac eexists_rel_subst :=
Ltac invert_rel_typ_body :=
dir_inversion_by_head eval_exp; subst;
+ functional_eval_rewrite_clear;
match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H); subst;
clear_refl_eqs;
handle_per_univ_elem_irrel;
diff --git a/theories/Core/Completeness/SubstitutionCases.v b/theories/Core/Completeness/SubstitutionCases.v
index 88a841bc..577cefd6 100644
--- a/theories/Core/Completeness/SubstitutionCases.v
+++ b/theories/Core/Completeness/SubstitutionCases.v
@@ -57,8 +57,7 @@ Proof with intuition.
pose (env_relΔA0 := env_relΔA).
handle_per_ctx_env_irrel.
eexists_rel_subst.
- match_by_head (per_ctx_env env_relΔA)
- ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
destruct_conjs.
handle_per_ctx_env_irrel.
intros.
@@ -134,8 +133,7 @@ Proof with intuition.
pose (env_relΓ''A0 := env_relΓ''A).
handle_per_ctx_env_irrel.
eexists_rel_subst.
- match_by_head (per_ctx_env env_relΓ''A)
- ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+ match_by_head (per_ctx_env env_relΓ''A) invert_per_ctx_env.
destruct_conjs.
handle_per_ctx_env_irrel.
intros.
diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
index 4bf94b82..fb82b100 100644
--- a/theories/Core/Semantic/PER/CoreTactics.v
+++ b/theories/Core/Semantic/PER/CoreTactics.v
@@ -37,13 +37,13 @@ Ltac destruct_rel_typ :=
(** Universe/Element PER Helper Tactics *)
-Ltac invert_per_univ_elem H :=
+Ltac basic_invert_per_univ_elem H :=
simp per_univ_elem in H;
inversion H;
subst;
try rewrite <- per_univ_elem_equation_1 in *.
-Ltac per_univ_elem_econstructor :=
+Ltac basic_per_univ_elem_econstructor :=
simp per_univ_elem;
econstructor;
try rewrite <- per_univ_elem_equation_1 in *.
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 98e10411..61642ae7 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -1,4 +1,4 @@
-From Coq Require Import Lia Morphisms Morphisms_Prop Morphisms_Relations PeanoNat Relation_Definitions RelationClasses.
+From Coq Require Import Equivalence Lia Morphisms Morphisms_Prop Morphisms_Relations PeanoNat Relation_Definitions RelationClasses.
From Equations Require Import Equations.
From Mcltt Require Import Axioms Base LibTactics.
From Mcltt.Core Require Import Evaluation PER.Definitions PER.CoreTactics Readback.
@@ -184,7 +184,7 @@ Proof with mautosolve.
simpl.
intros R R' HRR'.
split; intros Horig; [gen R' | gen R];
- induction Horig using per_univ_elem_ind; per_univ_elem_econstructor; eauto;
+ induction Horig using per_univ_elem_ind; basic_per_univ_elem_econstructor; eauto;
try (etransitivity; [symmetry + idtac|]; eassumption);
intros;
destruct_rel_mod_eval;
@@ -244,7 +244,7 @@ Proof with (destruct_rel_mod_eval; destruct_rel_mod_app; functional_eval_rewrite
remember a as a' in |- *.
gen a' b' R'.
induction Horig using per_univ_elem_ind; intros * Heq Hright;
- subst; invert_per_univ_elem Hright; unfold per_univ;
+ subst; basic_invert_per_univ_elem Hright; unfold per_univ;
intros;
apply_relation_equivalence;
try reflexivity.
@@ -288,16 +288,16 @@ Proof with mautosolve.
destruct_by_head per_univ.
eexists.
eapply proj1...
- - split; [per_univ_elem_econstructor | intros; apply_relation_equivalence]...
+ - split; [basic_per_univ_elem_econstructor | intros; apply_relation_equivalence]...
- destruct_conjs.
split.
- + per_univ_elem_econstructor; eauto.
+ + basic_per_univ_elem_econstructor; eauto.
intros.
assert (in_rel c' c) by eauto.
assert (in_rel c c) by (etransitivity; eassumption).
destruct_rel_mod_eval.
functional_eval_rewrite_clear.
- econstructor; mauto.
+ econstructor; eauto.
per_univ_elem_right_irrel_assert.
apply_relation_equivalence.
eassumption.
@@ -308,7 +308,7 @@ Proof with mautosolve.
destruct_rel_mod_eval.
destruct_rel_mod_app.
functional_eval_rewrite_clear.
- econstructor; mauto.
+ econstructor; eauto.
per_univ_elem_right_irrel_assert.
intuition.
- split; [econstructor | intros; apply_relation_equivalence]...
@@ -397,11 +397,11 @@ Lemma per_univ_elem_trans : forall i R A1 A2,
R a1 a2 ->
R a2 a3 ->
R a1 a3).
-Proof with (per_univ_elem_econstructor; mautosolve).
+Proof with (basic_per_univ_elem_econstructor; mautosolve).
pose proof (@relation_equivalence_pointwise domain).
induction 1 using per_univ_elem_ind;
[> split;
- [ intros * HT2; invert_per_univ_elem HT2; clear HT2
+ [ intros * HT2; basic_invert_per_univ_elem HT2; clear HT2
| intros * HTR1 HTR2; apply_relation_equivalence ] ..]; mauto.
- (* univ case *)
subst.
@@ -415,7 +415,7 @@ Proof with (per_univ_elem_econstructor; mautosolve).
idtac...
- (* pi case *)
destruct_conjs.
- per_univ_elem_econstructor; eauto.
+ basic_per_univ_elem_econstructor; eauto.
+ handle_per_univ_elem_irrel.
intuition.
+ intros.
@@ -474,48 +474,97 @@ Proof.
Qed.
(* This lemma gets rid of the unnecessary PER premise. *)
-Lemma per_univ_elem_core_pi' :
- forall i A p B A' p' B' elem_rel
+Lemma per_univ_elem_pi' :
+ forall i a a' p B p' B'
(in_rel : relation domain)
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
- (equiv_a_a' : {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel}}),
+ elem_rel,
+ {{ DF a ≈ a' ∈ per_univ_elem i ↘ in_rel}} ->
(forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
rel_mod_eval (per_univ_elem i) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
(elem_rel <~> fun f f' => forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app f c f' c' (out_rel equiv_c_c')) ->
- {{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }}.
+ {{ DF Π a p B ≈ Π a' p' B' ∈ per_univ_elem i ↘ elem_rel }}.
Proof.
intros.
- per_univ_elem_econstructor; eauto.
+ basic_per_univ_elem_econstructor; eauto.
typeclasses eauto.
Qed.
+Ltac per_univ_elem_econstructor :=
+ (repeat intro; hnf; eapply per_univ_elem_pi') + basic_per_univ_elem_econstructor.
+
+#[export]
+Hint Resolve per_univ_elem_pi' : mcltt.
+
+Lemma per_univ_elem_pi_clean_inversion : forall {i j a a' in_rel p p' B B' elem_rel},
+ {{ DF a ≈ a' ∈ per_univ_elem i ↘ in_rel }} ->
+ {{ DF Π a p B ≈ Π a' p' B' ∈ per_univ_elem j ↘ elem_rel }} ->
+ exists (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
+ (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
+ rel_mod_eval (per_univ_elem j) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) /\
+ (elem_rel <~> fun f f' => forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app f c f' c' (out_rel equiv_c_c')).
+Proof.
+ intros * Ha HΠ.
+ basic_invert_per_univ_elem HΠ.
+ handle_per_univ_elem_irrel.
+ eexists.
+ split.
+ - instantiate (1 := fun c c' (equiv_c_c' : in_rel c c') m m' =>
+ forall R,
+ rel_typ j B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} R ->
+ R m m').
+ intros.
+ assert (in_rel0 c c') by intuition.
+ (on_all_hyp: destruct_rel_by_assumption in_rel0).
+ econstructor; eauto.
+ apply -> per_univ_elem_morphism_iff; eauto.
+ split; intuition.
+ destruct_by_head rel_typ.
+ handle_per_univ_elem_irrel.
+ intuition.
+ - split; intros;
+ [assert (in_rel0 c c') by intuition; (on_all_hyp: destruct_rel_by_assumption in_rel0)
+ | assert (in_rel c c') by intuition; (on_all_hyp: destruct_rel_by_assumption in_rel)];
+ econstructor; intuition.
+ destruct_by_head rel_typ.
+ handle_per_univ_elem_irrel.
+ intuition.
+Qed.
+
+Ltac invert_per_univ_elem H :=
+ (unshelve eapply (per_univ_elem_pi_clean_inversion _) in H; [| eassumption | |]; destruct H as [? []])
+ + basic_invert_per_univ_elem H.
+
Lemma per_univ_elem_cumu : forall i a0 a1 R,
{{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} ->
{{ DF a0 ≈ a1 ∈ per_univ_elem (S i) ↘ R }}.
Proof with solve [eauto].
simpl.
- induction 1 using per_univ_elem_ind; subst.
- - eapply per_univ_elem_core_univ'...
- - per_univ_elem_econstructor...
- - per_univ_elem_econstructor; mauto.
- intros.
- destruct_rel_mod_eval.
- econstructor...
- - per_univ_elem_econstructor...
+ induction 1 using per_univ_elem_ind; subst;
+ per_univ_elem_econstructor; eauto.
+ intros.
+ destruct_rel_mod_eval.
+ econstructor...
Qed.
+#[export]
+Hint Resolve per_univ_elem_cumu : mcltt.
+
Lemma per_univ_elem_cumu_ge : forall i i' a0 a1 R,
i <= i' ->
{{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} ->
{{ DF a0 ≈ a1 ∈ per_univ_elem i' ↘ R }}.
-Proof with solve [eauto using per_univ_elem_cumu].
+Proof with mautosolve.
induction 1...
Qed.
+#[export]
+Hint Resolve per_univ_elem_cumu_ge : mcltt.
+
Lemma per_univ_elem_cumu_max_left : forall i j a0 a1 R,
{{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} ->
{{ DF a0 ≈ a1 ∈ per_univ_elem (max i j) ↘ R }}.
-Proof with solve [eauto using per_univ_elem_cumu_ge].
+Proof with mautosolve.
intros.
assert (i <= max i j) by lia...
Qed.
@@ -523,7 +572,7 @@ Qed.
Lemma per_univ_elem_cumu_max_right : forall i j a0 a1 R,
{{ DF a0 ≈ a1 ∈ per_univ_elem j ↘ R }} ->
{{ DF a0 ≈ a1 ∈ per_univ_elem (max i j) ↘ R }}.
-Proof with solve [eauto using per_univ_elem_cumu_ge].
+Proof with mautosolve.
intros.
assert (j <= max i j) by lia...
Qed.
@@ -539,7 +588,7 @@ Qed.
Add Parametric Morphism : per_ctx_env
with signature (@relation_equivalence env) ==> (@relation_equivalence ctx) as per_ctx_env_morphism_relation_equivalence.
-Proof with mautosolve.
+Proof.
intros * HRR' Γ Γ'.
simpl.
rewrite HRR'.
@@ -624,7 +673,7 @@ Proof.
Qed.
Ltac do_per_ctx_env_irrel_assert1 :=
- let tactic_error o1 o2 := fail 3 "per_ctx_env_irrel equality between" o1 "and" o2 "cannot be solved by mauto" in
+ let tactic_error o1 o2 := fail 3 "per_ctx_env_irrel equality between" o1 "and" o2 "cannot be solved" in
match goal with
| H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
H2 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
@@ -734,11 +783,31 @@ Proof.
- eauto using (per_env_trans _ _ _ _ _ _ H).
Qed.
-Lemma per_ctx_env_cons_clear_inversion : forall {Γ Γ' env_relΓ A A' env_relΓA},
+(* This lemma removes the PER argument *)
+Lemma per_ctx_env_cons' : forall {Γ Γ' i A A' tail_rel}
+ (head_rel : forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), relation domain)
+ env_rel,
+ {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ tail_rel }} ->
+ (forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}),
+ rel_typ i A p A' p' (head_rel equiv_p_p')) ->
+ (env_rel <~> fun p p' =>
+ exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel }}),
+ {{ Dom ~(p 0) ≈ ~(p' 0) ∈ head_rel equiv_p_drop_p'_drop }}) ->
+ {{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ env_rel }}.
+Proof.
+ intros.
+ econstructor; eauto.
+ typeclasses eauto.
+Qed.
+
+Ltac per_ctx_env_econstructor :=
+ (repeat intro; hnf; eapply per_ctx_env_cons') + econstructor.
+
+Lemma per_ctx_env_cons_clean_inversion : forall {Γ Γ' env_relΓ A A' env_relΓA},
{{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ env_relΓ }} ->
{{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ env_relΓA }} ->
exists i (head_rel : forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}), relation domain),
- (forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
+ (forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
rel_typ i A p A' p' (head_rel equiv_p_p')) /\
(env_relΓA <~> fun p p' =>
exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ env_relΓ }}),
@@ -751,19 +820,25 @@ Proof with intuition.
eexists.
split; intros.
- instantiate (1 := fun p p' (equiv_p_p' : env_relΓ p p') m m' =>
- forall a a' R,
- {{ ⟦ A ⟧ p ↘ a }} ->
- {{ ⟦ A' ⟧ p' ↘ a' }} ->
- {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
+ forall R,
+ rel_typ i A p A' p' R ->
{{ Dom m ≈ m' ∈ R }}).
assert (tail_rel p p') by intuition.
(on_all_hyp: destruct_rel_by_assumption tail_rel).
econstructor; eauto.
apply -> per_univ_elem_morphism_iff; eauto.
- split; intros; handle_per_univ_elem_irrel...
+ split; intros...
+ destruct_by_head rel_typ.
+ handle_per_univ_elem_irrel...
- intros o o'.
split; intros; destruct_conjs;
assert {{ Dom o ↯ ≈ o' ↯ ∈ tail_rel }} by intuition;
(on_all_hyp: destruct_rel_by_assumption tail_rel);
- eexists; intros; handle_per_univ_elem_irrel; intuition.
+ unshelve eexists; intros...
+ destruct_by_head rel_typ.
+ handle_per_univ_elem_irrel...
Qed.
+
+Ltac invert_per_ctx_env H :=
+ (unshelve eapply (per_ctx_env_cons_clean_inversion _) in H; [eassumption | |]; destruct H as [? [? []]])
+ + (inversion H; subst).
From b6e06184e7e3d1e4ca14af1ad3f4ab4a6639947f Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Tue, 21 May 2024 04:23:11 -0400
Subject: [PATCH 8/8] Defer some nat cases
---
theories/Core/Completeness/NatCases.v | 118 +++++++++++++++++++++++++-
1 file changed, 116 insertions(+), 2 deletions(-)
diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v
index 46b015b9..9d3448a8 100644
--- a/theories/Core/Completeness/NatCases.v
+++ b/theories/Core/Completeness/NatCases.v
@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations RelationClasses.
+From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases System.
Import Domain_Notations.
Lemma valid_exp_nat : forall {Γ i},
@@ -96,3 +96,117 @@ Proof.
- per_univ_elem_econstructor; reflexivity.
- econstructor; eassumption.
Qed.
+
+Lemma eval_natrec_rel : forall {Γ env_relΓ MZ MZ' MS MS' A A' i m m'},
+ {{ DF Γ ≈ Γ ∈ per_ctx_env ↘ env_relΓ }} ->
+ {{ Γ, ℕ ⊨ A ≈ A' : Type@i }} ->
+ {{ Γ ⊨ MZ ≈ MZ' : A[Id,,zero] }} ->
+ {{ Γ, ℕ, A ⊨ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
+ {{ Dom m ≈ m' ∈ per_nat }} ->
+ (forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
+ forall (elem_rel : relation domain),
+ rel_typ i A d{{{ p ↦ m }}} A d{{{ p' ↦ m' }}} elem_rel ->
+ exists r r',
+ {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} /\
+ {{ rec m' ⟦return A' | zero -> MZ' | succ -> MS' end⟧ p' ↘ r' }} /\
+ {{ Dom r ≈ r' ∈ elem_rel }}).
+Proof.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * equiv_Γ_Γ HAA' [] [env_relΓℕA] equiv_m_m'.
+ assert {{ Γ, ℕ ⊨ A : Type@i }} as [env_relΓℕ] by (unfold valid_exp_under_ctx; etransitivity; [| symmetry]; eassumption).
+ destruct_conjs.
+ pose (env_relΓℕA0 := env_relΓℕA).
+ pose (env_relΓℕ0 := env_relΓℕ).
+ match_by_head (per_ctx_env env_relΓℕA) invert_per_ctx_env.
+ handle_per_ctx_env_irrel.
+ match_by_head (per_ctx_env env_relΓℕ) invert_per_ctx_env.
+ handle_per_ctx_env_irrel.
+ induction equiv_m_m'; intros;
+ destruct_by_head rel_typ;
+ (on_all_hyp: destruct_rel_by_assumption env_relΓ);
+ invert_rel_typ_body;
+ destruct_by_head rel_typ;
+ dir_inversion_by_head eval_exp; subst;
+ dir_inversion_by_head eval_sub; subst;
+ dir_inversion_by_head eval_exp; subst;
+ functional_eval_rewrite_clear;
+ destruct_by_head rel_exp;
+ handle_per_univ_elem_irrel.
+ - do 2 eexists.
+ repeat split; only 1-2: econstructor; eauto.
+ - assert {{ Dom p'2 ↦ m ≈ p'3 ↦ n ∈ env_relΓℕ }} by (apply_relation_equivalence; eexists; eauto).
+ (on_all_hyp: destruct_rel_by_assumption env_relΓℕ).
+ assert {{ Dom p'2 ↦ m ≈ p'3 ↦ n ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; eexists; eauto).
+ apply_relation_equivalence.
+ (on_all_hyp: fun H => directed destruct (H _ _ HinΓℕ) as [? []]).
+ destruct_by_head rel_typ.
+ invert_rel_typ_body.
+ destruct_by_head rel_exp.
+ destruct_conjs.
+ unshelve epose proof (IHequiv_m_m' _ _ equiv_p_p' _ _) as [? [? [? []]]]; [| econstructor; solve [eauto] |].
+ handle_per_univ_elem_irrel.
+ rename x4 into r0.
+ rename x5 into r'0.
+ assert {{ Dom p'2 ↦ m ↦ r0 ≈ p'3 ↦ n ↦ r'0 ∈ env_relΓℕA }} as HinΓℕA by (apply_relation_equivalence; eexists; eauto).
+ apply_relation_equivalence.
+ (on_all_hyp: fun H => directed destruct (H _ _ HinΓℕA) as [? []]).
+ destruct_by_head rel_typ.
+ invert_rel_typ_body.
+ destruct_by_head rel_exp.
+ dir_inversion_by_head eval_sub; subst.
+ dir_inversion_by_head (eval_exp {{{ zero }}}); subst.
+ dir_inversion_by_head (eval_exp {{{ succ #1 }}}); subst.
+ dir_inversion_by_head (eval_exp {{{ #1 }}}); subst.
+ match_by_head eval_exp ltac:(fun H => simpl in H).
+ clear_refl_eqs.
+Abort.
+
+Lemma rel_exp_natrec_cong : forall {Γ MZ MZ' MS MS' A A' i M M'},
+ {{ Γ, ℕ ⊨ A ≈ A' : Type@i }} ->
+ {{ Γ ⊨ MZ ≈ MZ' : A[Id,,zero] }} ->
+ {{ Γ, ℕ, A ⊨ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
+ {{ Γ ⊨ M ≈ M' : ℕ }} ->
+ {{ Γ ⊨ rec M return A | zero -> MZ | succ -> MS end ≈ rec M' return A' | zero -> MZ' | succ -> MS' end : A[Id,,M] }}.
+Proof.
+ pose proof (@relation_equivalence_pointwise domain).
+ pose proof (@relation_equivalence_pointwise env).
+ intros * [env_relΓℕ] [env_relΓ] [env_relΓℕA] [].
+ destruct_conjs.
+ pose (env_relΓ0 := env_relΓ).
+ pose (env_relΓℕ0 := env_relΓℕ).
+ pose (env_relΓℕA0 := env_relΓℕA).
+ inversion_by_head (per_ctx_env env_relΓℕA); subst.
+ inversion_by_head (per_ctx_env env_relΓℕ); subst.
+ handle_per_ctx_env_irrel.
+ unshelve eexists_rel_exp; [constructor |].
+ intros.
+ (on_all_hyp: destruct_rel_by_assumption tail_rel0).
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ ℕ }}}); subst.
+ match goal with
+ | H : per_univ_elem _ _ d{{{ ℕ }}} d{{{ ℕ }}} |- _ =>
+ invert_per_univ_elem H;
+ apply_relation_equivalence
+ end.
+ inversion_by_head (eval_exp {{{ A[Id ,, zero] }}}); subst.
+ inversion_by_head (eval_sub {{{ Id ,, zero }}}); subst.
+ destruct_by_head rel_exp.
+ handle_per_univ_elem_irrel.
+ match goal with
+ | HM : {{ ⟦ M ⟧ p ↘ ~?m }}, HM' : {{ ⟦ M' ⟧ p' ↘ ~?m' }} |- _ =>
+ assert {{ Dom p ↦ m ≈ p' ↦ m' ∈ env_relΓℕ }} as Hequiv by (apply_relation_equivalence; eexists; eauto)
+ end.
+ apply_relation_equivalence.
+ (on_all_hyp: fun H => destruct (H _ _ Hequiv) as [? []]).
+ destruct_by_head rel_typ.
+ inversion_by_head (eval_exp {{{ Type@i }}}); subst.
+ match goal with
+ | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
+ invert_per_univ_elem H;
+ apply_relation_equivalence;
+ clear_refl_eqs
+ end.
+ destruct_by_head rel_exp.
+ destruct_conjs.
+ Abort.