diff --git a/Mcltt.Algorithmic.Subtyping.Lemmas.html b/Mcltt.Algorithmic.Subtyping.Lemmas.html
index 2e09f31..6867d8c 100644
--- a/Mcltt.Algorithmic.Subtyping.Lemmas.html
+++ b/Mcltt.Algorithmic.Subtyping.Lemmas.html
@@ -39,8 +39,8 @@ Mcltt.Algorithmic.Subtyping.Lemmas
#[local]
Ltac apply_subtyping :=
repeat match goal with
- | H : {{ ~?Γ ⊢ ~?M : ~?A }},
- H1 : {{ ~?Γ ⊢ ~?A ⊆ ~?B }} |- _ =>
+ | H : {{ ^?Γ ⊢ ^?M : ^?A }},
+ H1 : {{ ^?Γ ⊢ ^?A ⊆ ^?B }} |- _ =>
assert {{ Γ ⊢ M : B }} by mauto; clear H
end.
@@ -59,13 +59,13 @@ Mcltt.Algorithmic.Subtyping.Lemmas
destruct_all.
gen_presups.
repeat match goal with
- | H : {{ ~?Γ ⊢ ~?A ⊆ ~?B }}, H1: {{ ⊢ ~?Γ , ~_ }} |- _ =>
+ | H : {{ ^?Γ ⊢ ^?A ⊆ ^?B }}, H1: {{ ⊢ ^?Γ , ^_ }} |- _ =>
pose proof (wf_subtyp_univ_weaken _ _ _ _ H H1);
fail_if_dup
end.
apply_subtyping.
- assert {{ Γ, ~(nf_to_exp A') ⊢ B : Type@(max x x0) }} by mauto using lift_exp_max_right.
- assert {{ Γ, ~(nf_to_exp A') ⊢ B' : Type@(max x x0) }} by mauto using lift_exp_max_left.
+ assert {{ Γ, ^(nf_to_exp A') ⊢ B : Type@(max x x0) }} by mauto using lift_exp_max_right.
+ assert {{ Γ, ^(nf_to_exp A') ⊢ B' : Type@(max x x0) }} by mauto using lift_exp_max_left.
deepexec IHalg_subtyping_nf ltac:(fun H => pose proof H).
mauto 3.
Qed.
diff --git a/Mcltt.Algorithmic.Typing.Lemmas.html b/Mcltt.Algorithmic.Typing.Lemmas.html
index d7a98b1..c6b1de4 100644
--- a/Mcltt.Algorithmic.Typing.Lemmas.html
+++ b/Mcltt.Algorithmic.Typing.Lemmas.html
@@ -69,7 +69,7 @@ Mcltt.Algorithmic.Typing.Lemmas
Ltac functional_alg_type_infer_rewrite_clear1 :=
let tactic_error o1 o2 := fail 3 "functional_alg_type_infer equality between" o1 "and" o2 "cannot be solved by mauto" in
match goal with
- | H1 : {{ ~?Γ ⊢a ~?M ⟹ ~?A1 }}, H2 : {{ ~?Γ ⊢a ~?M ⟹ ~?A2 }} |- _ =>
+ | H1 : {{ ^?Γ ⊢a ^?M ⟹ ^?A1 }}, H2 : {{ ^?Γ ⊢a ^?M ⟹ ^?A2 }} |- _ =>
clean replace A2 with A1 by first [solve [mauto 2 using functional_alg_type_infer] | tactic_error A2 A1]; clear H2
end.
Ltac functional_alg_type_infer_rewrite_clear := repeat functional_alg_type_infer_rewrite_clear1.
@@ -107,7 +107,7 @@ Mcltt.Algorithmic.Typing.Lemmas
mauto 3.
- assert {{ Γ ⊢ M : Π A B }} by mauto 2.
assert (exists i, {{ Γ ⊢ Π A B : Type@i }}) as [i] by (gen_presups; eauto 2).
- assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, ~(A : exp) ⊢ B : Type@i }}) as [] by mauto 3.
+ assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, ^(A : exp) ⊢ B : Type@i }}) as [] by mauto 3.
assert {{ Γ ⊢ N : A }} by mauto 2.
assert {{ Γ ⊢ B[Id,,N] ≈ C : Type@i }} as <- by mauto 4 using soundness_ty'.
mauto 3.
@@ -151,25 +151,25 @@ Mcltt.Algorithmic.Typing.Lemmas
- assert {{ Γ ⊢ ℕ : Type@0 }} by mauto 3.
assert {{ Γ ⊢ M : ℕ }} by mauto 3 using alg_type_check_sound.
assert {{ ⊢ Γ, ℕ }} by mauto 3.
- assert {{ Γ, ℕ ⊢ A : ~n{{{ Type@i }}} }} by mauto 3 using alg_type_infer_sound...
- - assert {{ Γ ⊢ A : ~n{{{ Type@i }}} }} by mauto 3 using alg_type_infer_sound.
+ assert {{ Γ, ℕ ⊢ A : ^n{{{ Type@i }}} }} by mauto 3 using alg_type_infer_sound...
+ - assert {{ Γ ⊢ A : ^n{{{ Type@i }}} }} by mauto 3 using alg_type_infer_sound.
assert {{ Γ ⊢ A ≈ C : Type@i }} by mauto 3 using soundness_ty'.
assert {{ Γ, A ⊢ M : B }} by mauto 3 using alg_type_infer_sound.
assert (exists j, {{ Γ, A ⊢ B : Type@j }}) as [j] by (gen_presups; eauto 2).
- assert {{ ⊢ Γ, A ≈ Γ, ~(C : exp) }} by mauto 3.
+ assert {{ ⊢ Γ, A ≈ Γ, ^(C : exp) }} by mauto 3.
dir_inversion_clear_by_head nbe_ty.
simplify_evals.
dir_inversion_by_head read_typ; subst.
functional_initial_env_rewrite_clear.
- assert (initial_env {{{ Γ, ~(C : exp) }}} d{{{ ρ ↦ ⇑! a (length Γ) }}}) by mauto 3.
+ assert (initial_env {{{ Γ, ^(C : exp) }}} d{{{ ρ ↦ ⇑! a (length Γ) }}}) by mauto 3.
assert (nbe_ty Γ A C) by mauto 3.
assert (nbe_ty Γ C A0) by mauto 3.
replace A0 with C by mauto 3.
- assert (nbe_ty {{{ Γ, ~(C : exp) }}} B B') by mauto 3.
+ assert (nbe_ty {{{ Γ, ^(C : exp) }}} B B') by mauto 3.
assert (nbe_ty {{{ Γ, A }}} B B') by mauto 4 using ctxeq_nbe_ty_eq'...
- - assert {{ Γ ⊢ M : ~n{{{ Π A B }}} }} by mauto 3 using alg_type_infer_sound.
+ - assert {{ Γ ⊢ M : ^n{{{ Π A B }}} }} by mauto 3 using alg_type_infer_sound.
assert (exists i, {{ Γ ⊢ Π A B : Type@i }}) as [i] by (gen_presups; eauto 2).
- assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, ~(A : exp) ⊢ B : Type@i }}) as [] by mauto 3.
+ assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, ^(A : exp) ⊢ B : Type@i }}) as [] by mauto 3.
assert {{ Γ ⊢ N : A }} by mauto 3 using alg_type_check_sound.
assert {{ Γ ⊢ B[Id,,N] : Type@i }} by mauto 3...
- assert (exists i, {{ Γ ⊢ A : Type@i }}) as [i] by mauto 2...
@@ -221,18 +221,18 @@ Mcltt.Algorithmic.Typing.Lemmas
dir_inversion_by_head eval_exp; subst.
dir_inversion_by_head read_typ; subst.
simpl in *.
- assert {{ Γ ⊢ M : ~n{{{ Π A0 B0 }}} }} by mauto 3 using alg_type_infer_sound.
+ assert {{ Γ ⊢ M : ^n{{{ Π A0 B0 }}} }} by mauto 3 using alg_type_infer_sound.
assert (exists j, {{ Γ ⊢ Π A0 B0 : Type@j }}) as [j] by (gen_presups; eauto 2).
- assert ({{ Γ ⊢ A0 : Type@j }} /\ {{ Γ, ~(A0 : exp) ⊢ B0 : Type@j }}) as [] by mauto 3.
+ assert ({{ Γ ⊢ A0 : Type@j }} /\ {{ Γ, ^(A0 : exp) ⊢ B0 : Type@j }}) as [] by mauto 3.
do 2 eexists.
assert (nbe_ty Γ A A0) by mauto 3.
assert {{ Γ ⊢ A ≈ A0 : Type@i }} by mauto 3 using soundness_ty'.
repeat split; mauto 3.
assert (initial_env {{{ Γ, A }}} d{{{ ρ ↦ ⇑! a (length Γ) }}}) by mauto 3.
assert (nbe_ty {{{ Γ, A }}} B B') by mauto 3.
- assert (initial_env {{{ Γ, ~(A0 : exp) }}} d{{{ ρ ↦ ⇑! a0 (length Γ) }}}) by mauto 3.
- assert (nbe_ty {{{ Γ, ~(A0 : exp) }}} B0 B0) by mauto 3.
- assert {{ ⊢ Γ, A ≈ Γ, ~(A0 : exp) }} by mauto 3.
+ assert (initial_env {{{ Γ, ^(A0 : exp) }}} d{{{ ρ ↦ ⇑! a0 (length Γ) }}}) by mauto 3.
+ assert (nbe_ty {{{ Γ, ^(A0 : exp) }}} B0 B0) by mauto 3.
+ assert {{ ⊢ Γ, A ≈ Γ, ^(A0 : exp) }} by mauto 3.
assert (nbe_ty {{{ Γ, A }}} B0 B0) by mauto 4 using ctxeq_nbe_ty_eq'.
mauto 3.
Qed.
@@ -304,9 +304,9 @@ Mcltt.Algorithmic.Typing.Lemmas
- assert {{ Γ ⊢a M ⟸ Π A B }} by mauto 2.
assert {{ Γ ⊢a N ⟸ A }} by mauto 2.
assert (exists A' B', {{ Γ ⊢a M ⟹ Π A' B' }} /\ {{ Γ ⊢ A' ≈ A : Type@i }} /\ {{ Γ, A ⊢a B' ⊆ B }}) as [A' [B' [? []]]] by mauto 3.
- assert {{ Γ ⊢ M : ~n{{{ Π A' B' }}} }} by mauto 3 using alg_type_infer_sound.
+ assert {{ Γ ⊢ M : ^n{{{ Π A' B' }}} }} by mauto 3 using alg_type_infer_sound.
assert (exists j, {{ Γ ⊢ Π A' B' : Type@j }}) as [j] by (gen_presups; eauto 2).
- assert ({{ Γ ⊢ A' : Type@j }} /\ {{ Γ, ~(A' : exp) ⊢ B' : Type@j }}) as [] by mauto 3.
+ assert ({{ Γ ⊢ A' : Type@j }} /\ {{ Γ, ^(A' : exp) ⊢ B' : Type@j }}) as [] by mauto 3.
assert {{ Γ ⊢ N : A' }} by mauto 3.
assert {{ Γ ⊢ B'[Id,,N] : Type@j }} by mauto 3.
assert (exists W, nbe_ty Γ {{{ B'[Id,,N] }}} W /\ {{ Γ ⊢ B'[Id,,N] ≈ W : Type@j }}) as [W []] by (eapply soundness_ty; mauto 3).
diff --git a/Mcltt.Core.Completeness.NatCases.html b/Mcltt.Core.Completeness.NatCases.html
index 6d624fb..d5f31c7 100644
--- a/Mcltt.Core.Completeness.NatCases.html
+++ b/Mcltt.Core.Completeness.NatCases.html
@@ -235,7 +235,7 @@ Mcltt.Core.Completeness.NatCases
{{ Γ, ℕ, A ⊨ M ≈ M' : A[Wk∘Wk,,succ(#1)] }} ->
exists env_rel (_ : {{ EF Γ, ℕ, A ≈ Γ, ℕ, A ∈ per_ctx_env ↘ env_rel }}) i,
forall ρ ρ' (equiv_ρ_ρ' : {{ Dom ρ ≈ ρ' ∈ env_rel }}),
- exists elem_rel, rel_typ i A d{{{ ρ ↯ ↯ ↦ succ ~(ρ 1) }}} A d{{{ ρ' ↯ ↯ ↦ succ ~(ρ' 1) }}} elem_rel /\ rel_exp M ρ M' ρ' elem_rel.
+ exists elem_rel, rel_typ i A d{{{ ρ ↯ ↯ ↦ succ ^(ρ 1) }}} A d{{{ ρ' ↯ ↯ ↦ succ ^(ρ' 1) }}} elem_rel /\ rel_exp M ρ M' ρ' elem_rel.
Proof.
intros * [env_relΓℕA].
destruct_conjs.
@@ -314,8 +314,8 @@ Mcltt.Core.Completeness.NatCases
destruct_conjs.
functional_eval_rewrite_clear.
match goal with
- | _: {{ ⟦ σ ⟧s ρ ↘ ~?ρ1 }},
- _: {{ ⟦ σ ⟧s ρ' ↘ ~?ρ2 }} |- _ =>
+ | _: {{ ⟦ σ ⟧s ρ ↘ ^?ρ1 }},
+ _: {{ ⟦ σ ⟧s ρ' ↘ ^?ρ2 }} |- _ =>
rename ρ1 into ρσ;
rename ρ2 into ρ'σ
end.
@@ -345,8 +345,8 @@ Mcltt.Core.Completeness.NatCases
{
apply_relation_equivalence; eexists; eauto.
unfold drop_env.
- repeat change (fun n => d{{{ ~?ρσ ↦ ~?x ↦ ~?y }}} (S n)) with (fun n => d{{{ ρ ↦ x }}} n).
- repeat change (d{{{ ~?ρσ ↦ ~?x ↦ ~?y }}} 0) with y.
+ repeat change (fun n => d{{{ ^?ρσ ↦ ^?x ↦ ^?y }}} (S n)) with (fun n => d{{{ ρ ↦ x }}} n).
+ repeat change (d{{{ ^?ρσ ↦ ^?x ↦ ^?y }}} 0) with y.
eapply per_bot_then_per_elem; mauto.
}
apply_relation_equivalence.
@@ -443,8 +443,8 @@ Mcltt.Core.Completeness.NatCases
unshelve epose proof (IHequiv_m_m' _ _ equiv_ρ_ρ' _ _) as [? [? [? []]]]; shelve_unifiable; [solve [mauto] |].
handle_per_univ_elem_irrel.
match goal with
- | _: {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ~?r0 }},
- _: {{ rec m' ⟦return A' | zero -> MZ' | succ -> MS' end⟧ ρ' ↘ ~?r0' }} |- _ =>
+ | _: {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ^?r0 }},
+ _: {{ rec m' ⟦return A' | zero -> MZ' | succ -> MS' end⟧ ρ' ↘ ^?r0' }} |- _ =>
rename r0 into rm;
rename r0' into rm'
end.
@@ -611,8 +611,8 @@ Mcltt.Core.Completeness.NatCases
destruct_by_head rel_typ.
invert_rel_typ_body.
match goal with
- | _: {{ ⟦ σ ⟧s ρ ↘ ~?ρ1 }},
- _: {{ ⟦ σ ⟧s ρ' ↘ ~?ρ2 }} |- _ =>
+ | _: {{ ⟦ σ ⟧s ρ ↘ ^?ρ1 }},
+ _: {{ ⟦ σ ⟧s ρ' ↘ ^?ρ2 }} |- _ =>
rename ρ1 into ρσ;
rename ρ2 into ρ'σ
end.
@@ -625,8 +625,8 @@ Mcltt.Core.Completeness.NatCases
unshelve epose proof (IHequiv_m_m' _ _ equiv_ρ_ρ' _ _ _ _ _ _ _) as [? [? [? []]]]; shelve_unifiable; only 4: solve [mauto]; eauto.
handle_per_univ_elem_irrel.
match goal with
- | _: {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ ~_ ↘ ~?r0 }},
- _: {{ rec m' ⟦return A'[q σ] | zero -> MZ'[σ] | succ -> MS'[q (q σ)] end⟧ ~_ ↘ ~?r0' }} |- _ =>
+ | _: {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ ^_ ↘ ^?r0 }},
+ _: {{ rec m' ⟦return A'[q σ] | zero -> MZ'[σ] | succ -> MS'[q (q σ)] end⟧ ^_ ↘ ^?r0' }} |- _ =>
rename r0 into rm;
rename r0' into rm'
end.
@@ -649,8 +649,8 @@ Mcltt.Core.Completeness.NatCases
(on_all_hyp_rev: destruct_rel_by_assumption env_relΔ).
invert_rel_typ_body.
match goal with
- | _: {{ ⟦ σ ⟧s ρ ↘ ~?ρ1 }},
- _: {{ ⟦ σ ⟧s ρ' ↘ ~?ρ2 }} |- _ =>
+ | _: {{ ⟦ σ ⟧s ρ ↘ ^?ρ1 }},
+ _: {{ ⟦ σ ⟧s ρ' ↘ ^?ρ2 }} |- _ =>
rename ρ1 into ρσ;
rename ρ2 into ρ'σ
end.
@@ -720,9 +720,9 @@ Mcltt.Core.Completeness.NatCases
destruct_by_head rel_typ.
invert_rel_typ_body.
match goal with
- | _: {{ ⟦ σ ⟧s ~?ρ0 ↘ ~?ρσ0 }},
- _: {{ ⟦ A ⟧ ρσ ↦ ~?m0 ↘ ~?a0 }},
- _: {{ ⟦ A ⟧ ~?ρσ0 ↦ ~?m0' ↘ ~?a0' }} |- _ =>
+ | _: {{ ⟦ σ ⟧s ^?ρ0 ↘ ^?ρσ0 }},
+ _: {{ ⟦ A ⟧ ρσ ↦ ^?m0 ↘ ^?a0 }},
+ _: {{ ⟦ A ⟧ ^?ρσ0 ↦ ^?m0' ↘ ^?a0' }} |- _ =>
rename ρ0 into ρ';
rename ρσ0 into ρ'σ;
rename a0 into a;
diff --git a/Mcltt.Core.Completeness.TermStructureCases.html b/Mcltt.Core.Completeness.TermStructureCases.html
index f7c47bf..92b7ec4 100644
--- a/Mcltt.Core.Completeness.TermStructureCases.html
+++ b/Mcltt.Core.Completeness.TermStructureCases.html
@@ -53,8 +53,8 @@ Mcltt.Core.Completeness.TermStructureCases
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
handle_per_univ_elem_irrel.
match goal with
- | _: {{ ⟦ σ ⟧s ρ ↘ ~?ρ0 }},
- _: {{ ⟦ σ ⟧s ρ' ↘ ~?ρ'0 }} |- _ =>
+ | _: {{ ⟦ σ ⟧s ρ ↘ ^?ρ0 }},
+ _: {{ ⟦ σ ⟧s ρ' ↘ ^?ρ'0 }} |- _ =>
rename ρ0 into ρσ;
rename ρ'0 into ρ'σ
end.
diff --git a/Mcltt.Core.Semantic.Consequences.html b/Mcltt.Core.Semantic.Consequences.html
index 86a7f1e..da4dd9a 100644
--- a/Mcltt.Core.Semantic.Consequences.html
+++ b/Mcltt.Core.Semantic.Consequences.html
@@ -163,15 +163,15 @@ Mcltt.Core.Semantic.Consequences
assert (j = i) as -> by mauto 3
end.
do 2 eexists; repeat split; mauto 3; lia.
- + assert {{ Γ ⊢ Π ~_ ~_ ≈ Type@_ : Type@_ }} by mauto 3.
- assert ({{{ Π ~_ ~_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
+ + assert {{ Γ ⊢ Π ^_ ^_ ≈ Type@_ : Type@_ }} by mauto 3.
+ assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
+ right; left.
- assert {{ Γ ⊢ Π ~_ ~_ ≈ Type@_ : Type@_ }} by mauto 3.
- assert ({{{ Π ~_ ~_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
+ assert {{ Γ ⊢ Π ^_ ^_ ≈ Type@_ : Type@_ }} by mauto 3.
+ assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
+ right; right.
match goal with
- | _: {{ Γ ⊢ M' ≈ Π ~?A1 ~?A2 : Type@_ }},
- _: {{ Γ ⊢ Π ~?B1 ~?B2 ≈ M' : Type@_ }} |- _ =>
+ | _: {{ Γ ⊢ M' ≈ Π ^?A1 ^?A2 : Type@_ }},
+ _: {{ Γ ⊢ Π ^?B1 ^?B2 ≈ M' : Type@_ }} |- _ =>
assert {{ Γ ⊢ Π A1 A2 ≈ Π B1 B2 : Type@_ }} by mauto 3;
assert ({{ Γ ⊢ A1 ≈ B1 : Type@_ }} /\ {{ Γ, A1 ⊢ A2 ≈ B2 : Type@_ }}) as [] by mauto 3 using exp_eq_pi_inversion
end.
@@ -208,8 +208,8 @@ Mcltt.Core.Semantic.Consequences
assert {{ ⋅, Type@i ⊢ Type@i[Wk] ≈ Type@i : Type@(S i) }} by mauto 3.
eapply subtyp_spec in Heq as [| []]; destruct_conjs;
try (eapply HT'eq; mautosolve 4).
- assert {{ ⋅, Type@i ⊢ Type@i ≈ Π ~_ ~_ : Type@_ }} by mauto 3.
- assert ({{{ Π ~_ ~_ }}} = {{{ Type@i }}}) by mauto 3.
+ assert {{ ⋅, Type@i ⊢ Type@i ≈ Π ^_ ^_ : Type@_ }} by mauto 3.
+ assert ({{{ Π ^_ ^_ }}} = {{{ Type@i }}}) by mauto 3.
congruence.
Qed.
@@ -231,13 +231,13 @@ Mcltt.Core.Semantic.Consequences
simpl in *.
assert (exists B, {{ ⋅, Type@i ⊢ M0 : B }} /\ {{ ⋅ ⊢ Π Type@i B ⊆ Π Type@i #0 }}) as [? [? [| []]%subtyp_spec]] by mauto 3;
destruct_conjs;
- try assert ({{{ Π ~_ ~_ }}} = {{{ Type@_ }}}) by mauto 3;
+ try assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3;
try congruence.
- - assert (_ /\ {{ ⋅, Type@i ⊢ ~_ ≈ #0 : ~_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
+ - assert (_ /\ {{ ⋅, Type@i ⊢ ^_ ≈ #0 : ^_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
eapply consistency_ne_helper; mauto 3.
congruence.
- - assert (_ /\ {{ ~_ ⊢ x ≈ ~_ : ~_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
- assert (_ /\ {{ ~_ ⊢ ~_ ≈ #0 : ~_ }}) as [? ?] by mauto 3 using exp_eq_pi_inversion.
+ - assert (_ /\ {{ ^_ ⊢ x ≈ ^_ : ^_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
+ assert (_ /\ {{ ^_ ⊢ ^_ ≈ #0 : ^_ }}) as [? ?] by mauto 3 using exp_eq_pi_inversion.
assert {{ ⋅, Type@i ⊢ x ⊆ #0 }} by (etransitivity; [| eapply ctxeq_subtyp]; mauto 4).
eapply consistency_ne_helper; mauto 3.
congruence.
diff --git a/Mcltt.Core.Semantic.Domain.html b/Mcltt.Core.Semantic.Domain.html
index de92128..017128d 100644
--- a/Mcltt.Core.Semantic.Domain.html
+++ b/Mcltt.Core.Semantic.Domain.html
@@ -95,7 +95,7 @@ Mcltt.Core.Semantic.Domain
Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{' x '}}}'") : mcltt_scope.
Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : mcltt_scope.
- Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : mcltt_scope.
+ Notation "'^' x" := x (in custom domain at level 0, x constr at level 0) : mcltt_scope.
Notation "x" := x (in custom domain at level 0, x ident) : mcltt_scope.
Notation "'λ' ρ M" := (d_fn ρ M) (in custom domain at level 0, ρ custom domain at level 30, M custom exp at level 30) : mcltt_scope.
Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : mcltt_scope.
diff --git a/Mcltt.Core.Semantic.Evaluation.Definitions.html b/Mcltt.Core.Semantic.Evaluation.Definitions.html
index 712622a..e12b9ff 100644
--- a/Mcltt.Core.Semantic.Evaluation.Definitions.html
+++ b/Mcltt.Core.Semantic.Evaluation.Definitions.html
@@ -46,7 +46,7 @@ Mcltt.Core.Semantic.Evaluation.Definitions
| eval_exp_typ :
`( {{ ⟦ Type@i ⟧ ρ ↘ 𝕌@i }} )
| eval_exp_var :
- `( {{ ⟦ # x ⟧ ρ ↘ ~(ρ x) }} )
+ `( {{ ⟦ # x ⟧ ρ ↘ ^(ρ x) }} )
| eval_exp_nat :
`( {{ ⟦ ℕ ⟧ ρ ↘ ℕ }} )
| eval_exp_zero :
diff --git a/Mcltt.Core.Semantic.Evaluation.Lemmas.html b/Mcltt.Core.Semantic.Evaluation.Lemmas.html
index 007dcd6..64be5c3 100644
--- a/Mcltt.Core.Semantic.Evaluation.Lemmas.html
+++ b/Mcltt.Core.Semantic.Evaluation.Lemmas.html
@@ -109,13 +109,13 @@ Mcltt.Core.Semantic.Evaluation.Lemmas
Ltac functional_eval_rewrite_clear1 :=
let tactic_error o1 o2 := fail 3 "functional_eval equality between" o1 "and" o2 "cannot be solved by mauto" in
match goal with
- | H1 : {{ ⟦ ~?M ⟧ ~?ρ ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?ρ ↘ ~?m2 }} |- _ =>
+ | H1 : {{ ⟦ ^?M ⟧ ^?ρ ↘ ^?m1 }}, H2 : {{ ⟦ ^?M ⟧ ^?ρ ↘ ^?m2 }} |- _ =>
clean replace m2 with m1 by first [solve [mauto 2] | tactic_error m2 m1]; clear H2
- | H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
+ | H1 : {{ $| ^?m & ^?n |↘ ^?r1 }}, H2 : {{ $| ^?m & ^?n |↘ ^?r2 }} |- _ =>
clean replace r2 with r1 by first [solve [mauto 2] | tactic_error r2 r1]; clear H2
- | H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?ρ ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?ρ ↘ ~?r2 }} |- _ =>
+ | H1 : {{ rec ^?m ⟦return ^?A | zero -> ^?MZ | succ -> ^?MS end⟧ ^?ρ ↘ ^?r1 }}, H2 : {{ rec ^?m ⟦return ^?A | zero -> ^?MZ | succ -> ^?MS end⟧ ^?ρ ↘ ^?r2 }} |- _ =>
clean replace r2 with r1 by first [solve [mauto 2] | tactic_error r2 r1]; clear H2
- | H1 : {{ ⟦ ~?σ ⟧s ~?ρ ↘ ~?ρσ1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?ρ ↘ ~?ρσ2 }} |- _ =>
+ | H1 : {{ ⟦ ^?σ ⟧s ^?ρ ↘ ^?ρσ1 }}, H2 : {{ ⟦ ^?σ ⟧s ^?ρ ↘ ^?ρσ2 }} |- _ =>
clean replace ρσ2 with ρσ1 by first [solve [mauto 2] | tactic_error ρσ2 ρσ1]; clear H2
end.
Ltac functional_eval_rewrite_clear := repeat functional_eval_rewrite_clear1.
diff --git a/Mcltt.Core.Semantic.PER.CoreTactics.html b/Mcltt.Core.Semantic.PER.CoreTactics.html
index 2c9a369..2be77ef 100644
--- a/Mcltt.Core.Semantic.PER.CoreTactics.html
+++ b/Mcltt.Core.Semantic.PER.CoreTactics.html
@@ -41,7 +41,7 @@ Mcltt.Core.Semantic.PER.CoreTactics
Ltac destruct_rel_by_assumption in_rel H :=
repeat
match goal with
- | H' : {{ Dom ~?c ≈ ~?c' ∈ ?in_rel0 }} |- _ =>
+ | H' : {{ Dom ^?c ≈ ^?c' ∈ ?in_rel0 }} |- _ =>
unify in_rel0 in_rel;
destruct (H _ _ H') as [];
destruct_all;
diff --git a/Mcltt.Core.Semantic.PER.Definitions.html b/Mcltt.Core.Semantic.PER.Definitions.html
index 4caebef..f7f19cf 100644
--- a/Mcltt.Core.Semantic.PER.Definitions.html
+++ b/Mcltt.Core.Semantic.PER.Definitions.html
@@ -393,7 +393,7 @@ Mcltt.Core.Semantic.PER.Definitions
rel_typ i A ρ A' ρ' (head_rel equiv_ρ_ρ')) ->
(env_rel <~> fun ρ ρ' =>
exists (equiv_ρ_drop_ρ'_drop : {{ Dom ρ ↯ ≈ ρ' ↯ ∈ tail_rel }}),
- {{ Dom ~(ρ 0) ≈ ~(ρ' 0) ∈ head_rel equiv_ρ_drop_ρ'_drop }}) ->
+ {{ Dom ^(ρ 0) ≈ ^(ρ' 0) ∈ head_rel equiv_ρ_drop_ρ'_drop }}) ->
{{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ env_rel }} }
.
#[export]
diff --git a/Mcltt.Core.Semantic.PER.Lemmas.html b/Mcltt.Core.Semantic.PER.Lemmas.html
index 4cd13ca..7fe3537 100644
--- a/Mcltt.Core.Semantic.PER.Lemmas.html
+++ b/Mcltt.Core.Semantic.PER.Lemmas.html
@@ -375,8 +375,8 @@ Mcltt.Core.Semantic.PER.Lemmas
#[local]
Ltac per_univ_elem_right_irrel_assert1 :=
match goal with
- | H1 : {{ DF ~?a ≈ ~?b ∈ per_univ_elem ?i ↘ ?R1 }},
- H2 : {{ DF ~?a ≈ ~?b' ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+ | H1 : {{ DF ^?a ≈ ^?b ∈ per_univ_elem ?i ↘ ?R1 }},
+ H2 : {{ DF ^?a ≈ ^?b' ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
assert_fails (unify R1 R2);
match goal with
| H : R1 <~> R2 |- _ => fail 1
@@ -482,24 +482,24 @@ Mcltt.Core.Semantic.PER.Lemmas
Ltac do_per_univ_elem_irrel_assert1 :=
let tactic_error o1 o2 := fail 2 "per_univ_elem_irrel biconditional between" o1 "and" o2 "cannot be solved" in
match goal with
- | H1 : {{ DF ~?a ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
- H2 : {{ DF ~?a ≈ ~_ ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+ | H1 : {{ DF ^?a ≈ ^_ ∈ per_univ_elem ?i ↘ ?R1 }},
+ H2 : {{ DF ^?a ≈ ^_ ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
assert_fails (unify R1 R2);
match goal with
| H : R1 <~> R2 |- _ => fail 1
| H : R2 <~> R1 |- _ => fail 1
| _ => assert (R1 <~> R2) by (eapply per_univ_elem_right_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
end
- | H1 : {{ DF ~_ ≈ ~?b ∈ per_univ_elem ?i ↘ ?R1 }},
- H2 : {{ DF ~_ ≈ ~?b ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+ | H1 : {{ DF ^_ ≈ ^?b ∈ per_univ_elem ?i ↘ ?R1 }},
+ H2 : {{ DF ^_ ≈ ^?b ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
assert_fails (unify R1 R2);
match goal with
| H : R1 <~> R2 |- _ => fail 1
| H : R2 <~> R1 |- _ => fail 1
| _ => assert (R1 <~> R2) by (eapply per_univ_elem_left_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
end
- | H1 : {{ DF ~?a ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
- H2 : {{ DF ~_ ≈ ~?a ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+ | H1 : {{ DF ^?a ≈ ^_ ∈ per_univ_elem ?i ↘ ?R1 }},
+ H2 : {{ DF ^_ ≈ ^?a ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
@@ -1190,7 +1190,7 @@
Mcltt.Core.Semantic.PER.Lemmas
rel_typ i A ρ A' ρ' (
head_rel equiv_ρ_ρ')
) ->
(env_rel <~> fun ρ ρ' =>
exists (equiv_ρ_drop_ρ'_drop :
{{ Dom ρ ↯ ≈ ρ' ↯ ∈ tail_rel }}),
-
{{ Dom ~(ρ 0
) ≈ ~(ρ' 0
) ∈ head_rel equiv_ρ_drop_ρ'_drop }}) ->
+
{{ Dom ^(ρ 0
) ≈ ^(ρ' 0
) ∈ head_rel equiv_ρ_drop_ρ'_drop }}) ->
{{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ env_rel }}.
Proof.
intros.
@@ -1215,7 +1215,7 @@
Mcltt.Core.Semantic.PER.Lemmas
rel_typ i A ρ A' ρ' (
head_rel equiv_ρ_ρ')
) /\
(env_relΓA <~> fun ρ ρ' =>
exists (equiv_ρ_drop_ρ'_drop :
{{ Dom ρ ↯ ≈ ρ' ↯ ∈ env_relΓ }}),
-
{{ Dom ~(ρ 0
) ≈ ~(ρ' 0
) ∈ head_rel equiv_ρ_drop_ρ'_drop }}).
+
{{ Dom ^(ρ 0
) ≈ ^(ρ' 0
) ∈ head_rel equiv_ρ_drop_ρ'_drop }}).
Proof with intuition.
intros *
HΓ HΓA.
inversion HΓA;
subst.
diff --git a/Mcltt.Core.Semantic.Readback.Lemmas.html b/Mcltt.Core.Semantic.Readback.Lemmas.html
index efb5299..eafabc9 100644
--- a/Mcltt.Core.Semantic.Readback.Lemmas.html
+++ b/Mcltt.Core.Semantic.Readback.Lemmas.html
@@ -95,11 +95,11 @@
Mcltt.Core.Semantic.Readback.Lemmas
Ltac functional_read_rewrite_clear1 :=
let tactic_error o1 o2 :=
fail 3 "functional_read equality between"
o1 "and"
o2 "cannot be solved by mauto"
in
match goal with
- |
H1 :
{{ Rnf ~?
m in ?
s ↘ ~?
M1 }},
H2 :
{{ Rnf ~?
m in ?
s ↘ ~?
M2 }} |-
_ =>
+ |
H1 :
{{ Rnf ^?
m in ?
s ↘ ^?
M1 }},
H2 :
{{ Rnf ^?
m in ?
s ↘ ^?
M2 }} |-
_ =>
clean replace M2 with M1 by first [
solve [
mauto 2] |
tactic_error M2 M1];
clear H2
- |
H1 :
{{ Rne ~?
m in ?
s ↘ ~?
M1 }},
H2 :
{{ Rne ~?
m in ?
s ↘ ~?
M2 }} |-
_ =>
+ |
H1 :
{{ Rne ^?
m in ?
s ↘ ^?
M1 }},
H2 :
{{ Rne ^?
m in ?
s ↘ ^?
M2 }} |-
_ =>
clean replace M2 with M1 by first [
solve [
mauto 2] |
tactic_error M2 M1];
clear H2
- |
H1 :
{{ Rtyp ~?
m in ?
s ↘ ~?
M1 }},
H2 :
{{ Rtyp ~?
m in ?
s ↘ ~?
M2 }} |-
_ =>
+ |
H1 :
{{ Rtyp ^?
m in ?
s ↘ ^?
M1 }},
H2 :
{{ Rtyp ^?
m in ?
s ↘ ^?
M2 }} |-
_ =>
clean replace M2 with M1 by first [
solve [
mauto 2] |
tactic_error M2 M1];
clear H2
end.
Ltac functional_read_rewrite_clear :=
repeat functional_read_rewrite_clear1.
diff --git a/Mcltt.Core.Semantic.Realizability.html b/Mcltt.Core.Semantic.Realizability.html
index 951b355..f2bb107 100644
--- a/Mcltt.Core.Semantic.Realizability.html
+++ b/Mcltt.Core.Semantic.Realizability.html
@@ -91,10 +91,10 @@
Mcltt.Core.Semantic.Realizability
destruct_rel_mod_eval.
destruct_rel_mod_app.
match goal with
- |
_:
{{ $| ~?
f0 & ⇑! a s |↘ ~_ }},
-
_:
{{ $| ~?
f0' & ⇑! a' s |↘ ~_ }},
-
_:
{{ ⟦ B ⟧ ρ ↦ ⇑! a s ↘ ~?
b0 }},
-
_:
{{ ⟦ B' ⟧ ρ' ↦ ⇑! a' s ↘ ~?
b0' }} |-
_ =>
+ |
_:
{{ $| ^?
f0 & ⇑! a s |↘ ^_ }},
+
_:
{{ $| ^?
f0' & ⇑! a' s |↘ ^_ }},
+
_:
{{ ⟦ B ⟧ ρ ↦ ⇑! a s ↘ ^?
b0 }},
+
_:
{{ ⟦ B' ⟧ ρ' ↦ ⇑! a' s ↘ ^?
b0' }} |-
_ =>
rename f0 into f;
rename f0' into f';
rename b0 into b;
diff --git a/Mcltt.Core.Soundness.FunctionCases.html b/Mcltt.Core.Soundness.FunctionCases.html
index ce8a527..379ff16 100644
--- a/Mcltt.Core.Soundness.FunctionCases.html
+++ b/Mcltt.Core.Soundness.FunctionCases.html
@@ -119,7 +119,7 @@
Mcltt.Core.Soundness.FunctionCases
destruct_by_head per_univ.
functional_eval_rewrite_clear.
match goal with
- |
_:
{{ ⟦ B ⟧ ρ ↦ m ↘ ~?
a }} |-
_ =>
+ |
_:
{{ ⟦ B ⟧ ρ ↦ m ↘ ^?
a }} |-
_ =>
rename a into b
end.
assert {{ Δ' ⊢ M : A[σ][τ] }} by mauto 3
using glu_univ_elem_trm_escape.
@@ -231,7 +231,7 @@
Mcltt.Core.Soundness.FunctionCases
handle_per_univ_elem_irrel.
eexists;
split;
mauto 3.
match goal with
- |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ~?
a }} |-
_ =>
+ |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ^?
a }} |-
_ =>
rename a into b
end.
assert {{ DG b ∈ glu_univ_elem i ↘ OP n equiv_n ↘ OEl n equiv_n }} by mauto 3.
@@ -323,8 +323,8 @@
Mcltt.Core.Soundness.FunctionCases
inversion_clear_by_head pi_glu_exp_pred.
match goal with
|
_:
glu_univ_elem i ?
P' ?
El' a,
-
_:
{{ ⟦ A ⟧ ρ ↘ ~?
a' }},
-
_:
{{ ⟦ N ⟧ ρ ↘ ~?
n' }} |-
_ =>
+
_:
{{ ⟦ A ⟧ ρ ↘ ^?
a' }},
+
_:
{{ ⟦ N ⟧ ρ ↘ ^?
n' }} |-
_ =>
rename a' into a;
rename n' into n;
rename P' into Pa;
@@ -336,8 +336,8 @@
Mcltt.Core.Soundness.FunctionCases
(
on_all_hyp:
destruct_rel_by_assumption in_rel).
simplify_evals.
match goal with
- |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ~?
b' }},
-
_:
{{ $| m & n |↘ ~?
mn' }} |-
_ =>
+ |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ^?
b' }},
+
_:
{{ $| m & n |↘ ^?
mn' }} |-
_ =>
rename b' into b;
rename mn' into mn
end.
diff --git a/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html b/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html
index 140e460..4a3643c 100644
--- a/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html
+++ b/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html
@@ -621,8 +621,8 @@
Mcltt.Core.Soundness.LogicalRelation.CoreLemmas
Ltac apply_functional_glu_univ_elem1 :=
let tactic_error o1 o2 :=
fail 2 "functional_glu_univ_elem biconditional between"
o1 "and"
o2 "cannot be solved"
in
match goal with
- |
H1 :
{{ DG ~?
a ∈ glu_univ_elem ?
i ↘ ?
P1 ↘ ?
El1 }},
-
H2 :
{{ DG ~?
a ∈ glu_univ_elem ?
i' ↘ ?
P2 ↘ ?
El2 }} |-
_ =>
+ |
H1 :
{{ DG ^?
a ∈ glu_univ_elem ?
i ↘ ?
P1 ↘ ?
El1 }},
+
H2 :
{{ DG ^?
a ∈ glu_univ_elem ?
i' ↘ ?
P2 ↘ ?
El2 }} |-
_ =>
unify i i';
assert_fails (
unify P1 P2;
unify El1 El2);
match goal with
diff --git a/Mcltt.Core.Soundness.LogicalRelation.Definitions.html b/Mcltt.Core.Soundness.LogicalRelation.Definitions.html
index f999275..5b6017d 100644
--- a/Mcltt.Core.Soundness.LogicalRelation.Definitions.html
+++ b/Mcltt.Core.Soundness.LogicalRelation.Definitions.html
@@ -387,7 +387,7 @@
Mcltt.Core.Soundness.LogicalRelation.Definitions
a more direct consequence of
{{ Γ, A ⊢ #0 : A[Wk] }}
-
{{ Δ ⊢ #0
[σ] : A[Wk][σ] ® ~(ρ 0
) ∈ El }} ->
+
{{ Δ ⊢ #0
[σ] : A[Wk][σ] ® ^(ρ 0
) ∈ El }} ->
{{ Δ ⊢s Wk ∘ σ ® ρ ↯ ∈ TSb }} ->
{{ Δ ⊢s σ ® ρ ∈ cons_glu_sub_pred i Γ A TSb }} }.
diff --git a/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html b/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html
index 2351c80..58fdabc 100644
--- a/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html
+++ b/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html
@@ -279,7 +279,7 @@
Mcltt.Core.Soundness.LogicalRelation.Lemmas
destruct_rel_mod_app.
handle_per_univ_elem_irrel.
match goal with
- |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ~?
a }} |-
_ =>
+ |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ^?
a }} |-
_ =>
rename a into b
end.
eexists;
split;
mauto 4.
@@ -496,8 +496,8 @@
Mcltt.Core.Soundness.LogicalRelation.Lemmas
destruct_rel_mod_eval.
handle_per_univ_elem_irrel.
match goal with
- |
_:
{{ ⟦ B ⟧ ρ ↦ ⇑! a (length Γ) ↘ ~?
a0 }},
-
_:
{{ ⟦ B' ⟧ ρ' ↦ ⇑! a' (length Γ) ↘ ~?
a0' }} |-
_ =>
+ |
_:
{{ ⟦ B ⟧ ρ ↦ ⇑! a (length Γ) ↘ ^?
a0 }},
+
_:
{{ ⟦ B' ⟧ ρ' ↦ ⇑! a' (length Γ) ↘ ^?
a0' }} |-
_ =>
rename a0 into b;
rename a0' into b'
end.
@@ -594,8 +594,8 @@
Mcltt.Core.Soundness.LogicalRelation.Lemmas
destruct_rel_mod_eval.
handle_per_univ_elem_irrel.
match goal with
- |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ~?
a }},
-
_:
{{ ⟦ B' ⟧ ρ' ↦ n ↘ ~?
a' }} |-
_ =>
+ |
_:
{{ ⟦ B ⟧ ρ ↦ n ↘ ^?
a }},
+
_:
{{ ⟦ B' ⟧ ρ' ↦ n ↘ ^?
a' }} |-
_ =>
rename a into b;
rename a' into b'
end.
@@ -956,7 +956,7 @@
Mcltt.Core.Soundness.LogicalRelation.Lemmas
assert (
exists Pmax Elmax, {{ DG a ∈ glu_univ_elem (
max i l)
↘ Pmax ↘ Elmax }})
as [
Pmax [
Elmax]]
by mauto using glu_univ_elem_cumu_max_left.
assert (
i <= max i l)
by lia.
-
assert {{ Δ0 ⊢ #0
[σ0] : A'[Wk][σ0] ® ~(ρ0 0
) ∈ Elmax }}.
+
assert {{ Δ0 ⊢ #0
[σ0] : A'[Wk][σ0] ® ^(ρ0 0
) ∈ Elmax }}.
{
assert {{ Γ, A ⊢s Wk : Γ }} by mauto 3.
assert {{ Δ0 ⊢ A[Wk][σ0] ≈ A'[Wk][σ0] : Type@l }} by mauto 3.
@@ -983,8 +983,8 @@
Mcltt.Core.Soundness.LogicalRelation.Lemmas
Ltac apply_functional_glu_ctx_env1 :=
let tactic_error o1 o2 :=
fail 2 "functional_glu_ctx_env biconditional between"
o1 "and"
o2 "cannot be solved"
in
match goal with
- |
H1 :
{{ EG ~?
Γ ∈ glu_ctx_env ↘ ?
Sb1 }},
-
H2 :
{{ EG ~?
Γ ∈ glu_ctx_env ↘ ?
Sb2 }} |-
_ =>
+ |
H1 :
{{ EG ^?
Γ ∈ glu_ctx_env ↘ ?
Sb1 }},
+
H2 :
{{ EG ^?
Γ ∈ glu_ctx_env ↘ ?
Sb2 }} |-
_ =>
assert_fails (
unify Sb1 Sb2);
match goal with
|
H :
Sb1 <∙> Sb2 |-
_ =>
fail 1
@@ -1090,7 +1090,7 @@
Mcltt.Core.Soundness.LogicalRelation.Lemmas
destruct_by_head cons_glu_sub_pred.
econstructor;
mauto 3.
- -
assert {{ Δ' ⊢ #0
[σ0][σ] : A[Wk][σ0][σ] ® ~(ρ 0
) ∈ El }} by (
eapply glu_univ_elem_exp_monotone;
mauto 3).
+ -
assert {{ Δ' ⊢ #0
[σ0][σ] : A[Wk][σ0][σ] ® ^(ρ 0
) ∈ El }} by (
eapply glu_univ_elem_exp_monotone;
mauto 3).
assert {{ Γ, A ⊢ #0
: A[Wk] }} by mauto 3.
assert {{ Γ, A ⊢s Wk : Γ }} by mauto 3.
assert {{ Δ' ⊢ #0
[σ0∘σ] ≈ #0
[σ0][σ] : A[Wk][σ0∘σ] }} as ->
by mauto 3.
@@ -1175,7 +1175,7 @@
Mcltt.Core.Soundness.LogicalRelation.Lemmas
Ltac destruct_glu_rel_by_assumption sub_glu_rel H :=
repeat
match goal with
- |
H' :
{{ ~?
Δ ⊢s ~?σ
® ~?ρ
∈ ?
sub_glu_rel0 }} |-
_ =>
+ |
H' :
{{ ^?
Δ ⊢s ^?σ
® ^?ρ
∈ ?
sub_glu_rel0 }} |-
_ =>
unify sub_glu_rel0 sub_glu_rel;
destruct (
H _ _ _ H')
as [];
destruct_conjs;
diff --git a/Mcltt.Core.Soundness.NatCases.html b/Mcltt.Core.Soundness.NatCases.html
index 67bd76d..3edd754 100644
--- a/Mcltt.Core.Soundness.NatCases.html
+++ b/Mcltt.Core.Soundness.NatCases.html
@@ -292,7 +292,7 @@
Mcltt.Core.Soundness.NatCases
unfold univ_glu_exp_pred' in *.
destruct_conjs.
match goal with
- |
_:
{{ ⟦ A ⟧ ρ ↦ m' ↘ ~?
m }},
_:
{{ DG ~?
m ∈ glu_univ_elem i ↘ ?
P ↘ ?
El }} |-
_ =>
+ |
_:
{{ ⟦ A ⟧ ρ ↦ m' ↘ ^?
m }},
_:
{{ DG ^?
m ∈ glu_univ_elem i ↘ ?
P ↘ ?
El }} |-
_ =>
rename m into am';
rename P into P';
rename El into El'
@@ -330,7 +330,7 @@
Mcltt.Core.Soundness.NatCases
destruct_conjs.
handle_functional_glu_univ_elem.
match goal with
- |
_:
{{ ⟦ MS ⟧ ρ ↦ m' ↦ r' ↘ ~?
m }} |-
_ =>
+ |
_:
{{ ⟦ MS ⟧ ρ ↦ m' ↦ r' ↘ ^?
m }} |-
_ =>
rename m into ms
end.
exists ms;
split;
mauto 3.
@@ -443,7 +443,7 @@
Mcltt.Core.Soundness.NatCases
destruct_conjs.
handle_functional_glu_univ_elem.
match goal with
- |
_:
{{ ⟦ MZ ⟧ ~?ρ0
↘ ~?
m }},
_:
{{ ⟦ A ⟧ ~?ρ0
↦ zero ↘ ~?
a }} |-
_ =>
+ |
_:
{{ ⟦ MZ ⟧ ^?ρ0
↘ ^?
m }},
_:
{{ ⟦ A ⟧ ^?ρ0
↦ zero ↘ ^?
a }} |-
_ =>
rename ρ0
into ρ;
rename m into mz;
rename a into az
@@ -492,7 +492,7 @@
Mcltt.Core.Soundness.NatCases
destruct_rel_typ.
invert_rel_typ_body.
match goal with
- |
_:
{{ ⟦ A ⟧ ρ ↦ ⇑! ℕ s ↘ ~?
a }},
_:
{{ ⟦ A ⟧ ρ ↦ (succ ⇑! ℕ s) ↘ ~?
a' }} |-
_ =>
+ |
_:
{{ ⟦ A ⟧ ρ ↦ ⇑! ℕ s ↘ ^?
a }},
_:
{{ ⟦ A ⟧ ρ ↦ (succ ⇑! ℕ s) ↘ ^?
a' }} |-
_ =>
rename a into as';
@@ -511,7 +511,7 @@
Mcltt.Core.Soundness.NatCases
destruct_by_head rel_exp.
functional_eval_rewrite_clear.
match goal with
- |
_:
{{ ⟦ MS ⟧ ρ ↦ ⇑! ℕ s ↦ ⇑! as' (S s) ↘ ~?
m }} |-
_ =>
+ |
_:
{{ ⟦ MS ⟧ ρ ↦ ⇑! ℕ s ↦ ⇑! as' (S s) ↘ ^?
m }} |-
_ =>
rename m into ms
end.
assert {{ Dom as' ≈ as' ∈ per_top_typ }} as [? []]%(
fun {
a} (
f :
per_top_typ a a) =>
f (
S s))
by mauto 3.
@@ -537,7 +537,7 @@
Mcltt.Core.Soundness.NatCases
match_by_head read_ne ltac:(
fun H =>
directed inversion_clear H).
handle_functional_glu_univ_elem.
match goal with
- |
_:
{{ ⟦ A ⟧ ~?ρ'
↦ ⇑! ℕ (length Δ') ↘ ~?
a }} |-
_ =>
+ |
_:
{{ ⟦ A ⟧ ^?ρ'
↦ ⇑! ℕ (length Δ') ↘ ^?
a }} |-
_ =>
rename ρ'
into ρ;
rename a into aΔ'
end.
@@ -552,10 +552,10 @@
Mcltt.Core.Soundness.NatCases
clear_dups.
handle_functional_glu_univ_elem.
match goal with
- |
_:
{{ ⟦ A ⟧ ~?ρ'
↦ succ (⇑! ℕ (length Δ')) ↘ ~?
a }},
-
_:
{{ Rtyp aΔ' in S (
length Δ')
↘ ~?
A }},
-
_:
{{ Rnf ⇓ az mz in length Δ' ↘ ~?
MZ }},
-
_:
{{ Rne m in length Δ' ↘ ~?
M }} |-
_ =>
+ |
_:
{{ ⟦ A ⟧ ^?ρ'
↦ succ (⇑! ℕ (length Δ')) ↘ ^?
a }},
+
_:
{{ Rtyp aΔ' in S (
length Δ')
↘ ^?
A }},
+
_:
{{ Rnf ⇓ az mz in length Δ' ↘ ^?
MZ }},
+
_:
{{ Rne m in length Δ' ↘ ^?
M }} |-
_ =>
rename A into A';
rename ρ'
into ρ;
rename a into asucc;
@@ -730,19 +730,19 @@
Mcltt.Core.Soundness.NatCases
clear_dups.
match_by_head nat_glu_typ_pred ltac:(
fun H =>
clear H).
match goal with
- |
_:
{{ ⟦ A ⟧ ρ ↦ m ↘ ~?
a' }},
-
_:
{{ DG ~?
a' ∈ glu_univ_elem i ↘ ?
P' ↘ ?
El' }} |-
_ =>
+ |
_:
{{ ⟦ A ⟧ ρ ↦ m ↘ ^?
a' }},
+
_:
{{ DG ^?
a' ∈ glu_univ_elem i ↘ ?
P' ↘ ?
El' }} |-
_ =>
rename a' into a;
rename P' into P;
rename El' into El
end.
-
assert (
exists r, {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ~ r }} /\ El Δ {{{ A[σ,, M[σ]] }}} {{{ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end }}} r)
as [? []]
by (
eapply glu_rel_exp_natrec_helper;
revgoals;
mauto 4).
+
assert (
exists r, {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\ El Δ {{{ A[σ,, M[σ]] }}} {{{ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end }}} r)
as [? []]
by (
eapply glu_rel_exp_natrec_helper;
revgoals;
mauto 4).
econstructor;
mauto 3.
-
assert {{ Δ ⊢s σ : Γ }} by mauto 2.
-
assert {{ Γ ⊢ M : ℕ }} by mauto 2.
-
assert {{ Γ, ℕ ⊢ A : Type@i }} by mauto 3.
-
assert {{ Δ ⊢ A[σ,,M[σ]] ≈ A[Id,,M][σ] : Type@i }} as <-
by (
symmetry;
mauto 2).
-
assert {{ Δ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] ≈ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }} as ->
by (
econstructor;
mauto 3).
+
assert {{ Δ ⊢s σ : Γ }} by mauto 2.
+
assert {{ Γ ⊢ M : ℕ }} by mauto 2.
+
assert {{ Γ, ℕ ⊢ A : Type@i }} by mauto 3.
+
assert {{ Δ ⊢ A[σ,,M[σ]] ≈ A[Id,,M][σ] : Type@i }} as <-
by (
symmetry;
mauto 2).
+
assert {{ Δ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] ≈ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }} as ->
by (
econstructor;
mauto 3).
eassumption.
Qed.
diff --git a/Mcltt.Core.Soundness.Realizability.html b/Mcltt.Core.Soundness.Realizability.html
index e4d2cd6..b25251b 100644
--- a/Mcltt.Core.Soundness.Realizability.html
+++ b/Mcltt.Core.Soundness.Realizability.html
@@ -74,7 +74,7 @@
Mcltt.Core.Soundness.Realizability
{{ Δ ⊢w σ : Γ }} ->
forall Γ1 Γ2 A0,
Γ = Γ1 ++ A0 :: Γ2 ->
-
{{ Δ ⊢ #(length Γ1)[σ] ≈ #(length Δ - length Γ2 - 1
) : ~(iter (
S (
length Γ1)) (
fun A =>
{{{ A[Wk] }}})
A0)[σ] }}.
+
{{ Δ ⊢ #(length Γ1)[σ] ≈ #(length Δ - length Γ2 - 1
) : ^(iter (
S (
length Γ1)) (
fun A =>
{{{ A[Wk] }}})
A0)[σ] }}.
Proof.
induction 1;
intros;
subst;
gen_presups.
-
pose proof (
app_ctx_vlookup _ _ _ _ HΔ eq_refl)
as Hvar.
@@ -91,7 +91,7 @@
Mcltt.Core.Soundness.Realizability
gen_presup Hvar.
clear_dups.
assert {{ ⊢ Δ', A }} by mauto 3.
-
assert {{ Δ', A ⊢s Wk : ~ (Γ1 ++ {{{ Γ2, A0 }}}) }} by mauto 3.
+
assert {{ Δ', A ⊢s Wk : ^(Γ1 ++ {{{ Γ2, A0 }}}) }} by mauto 3.
transitivity {{{ #(length Γ1)[Wk∘τ] }}}; [
mauto 3 |].
rewrite H1.
etransitivity; [
eapply wf_exp_eq_sub_compose;
mauto 3 |].
@@ -272,7 +272,7 @@
Mcltt.Core.Soundness.Realizability
bulky_rewrite_in H23.
unshelve (
econstructor;
eauto).
+
trivial.
- +
eassert {{ Δ ⊢ M[σ] N : ~_ }} by (
eapply wf_app';
eassumption).
+ +
eassert {{ Δ ⊢ M[σ] N : ^_ }} by (
eapply wf_app';
eassumption).
autorewrite with mcltt in H25.
trivial.
+
mauto using domain_app_per.
@@ -321,7 +321,7 @@
Mcltt.Core.Soundness.Realizability
specialize (
H29 _ _ _ H19 H9).
rewrite H5 in *.
autorewrite with mcltt.
-
eassert {{ Δ ⊢ M[σ] : ~_ }} by (
mauto 2).
+
eassert {{ Δ ⊢ M[σ] : ^_ }} by (
mauto 2).
autorewrite with mcltt in H30.
rewrite @
wf_exp_eq_pi_eta' with (
M :=
{{{ M[σ] }}}); [|
trivial].
cbn [
nf_to_exp].
diff --git a/Mcltt.Core.Soundness.Weakening.Lemmas.html b/Mcltt.Core.Soundness.Weakening.Lemmas.html
index 0b7aa41..6ced903 100644
--- a/Mcltt.Core.Soundness.Weakening.Lemmas.html
+++ b/Mcltt.Core.Soundness.Weakening.Lemmas.html
@@ -56,7 +56,7 @@
Mcltt.Core.Soundness.Weakening.Lemmas
Ltac saturate_weakening_escape1 :=
match goal with
- |
H :
{{ ~_ ⊢w ~_ : ~_ }} |-
_ =>
+ |
H :
{{ ^_ ⊢w ^_ : ^_ }} |-
_ =>
pose proof (
weakening_escape _ _ _ H);
fail_if_dup
end.
diff --git a/Mcltt.Core.Syntactic.Corollaries.html b/Mcltt.Core.Syntactic.Corollaries.html
index 1fbcc85..c68530c 100644
--- a/Mcltt.Core.Syntactic.Corollaries.html
+++ b/Mcltt.Core.Syntactic.Corollaries.html
@@ -115,7 +115,7 @@
Mcltt.Core.Syntactic.Corollaries
Lemma app_ctx_lookup :
forall Δ T Γ n,
length Δ = n ->
-
{{ #n : ~(iter (
S n) (
fun T =>
{{{T [ Wk ]}}})
T) ∈ ~(Δ ++ T :: Γ) }}.
+
{{ #n : ^(iter (
S n) (
fun T =>
{{{T [ Wk ]}}})
T) ∈ ^(Δ ++ T :: Γ) }}.
Proof.
induction Δ;
intros;
simpl in *;
subst;
mauto.
Qed.
@@ -133,9 +133,9 @@
Mcltt.Core.Syntactic.Corollaries
Lemma app_ctx_vlookup :
forall Δ T Γ n,
-
{{ ⊢ ~(Δ ++ T :: Γ) }} ->
+
{{ ⊢ ^(Δ ++ T :: Γ) }} ->
length Δ = n ->
-
{{ ~(Δ ++ T :: Γ) ⊢ #n : ~(iter (
S n) (
fun T =>
{{{T [ Wk ]}}})
T) }}.
+
{{ ^(Δ ++ T :: Γ) ⊢ #n : ^(iter (
S n) (
fun T =>
{{{T [ Wk ]}}})
T) }}.
Proof.
intros.
econstructor;
auto using app_ctx_lookup.
Qed.
diff --git a/Mcltt.Core.Syntactic.CtxSub.html b/Mcltt.Core.Syntactic.CtxSub.html
index 7296470..9a16a01 100644
--- a/Mcltt.Core.Syntactic.CtxSub.html
+++ b/Mcltt.Core.Syntactic.CtxSub.html
@@ -50,11 +50,11 @@
Mcltt.Core.Syntactic.CtxSub
#[
local]
Ltac gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyp_helper H :=
match type of H with
- |
{{ ~?
Γ ⊢ ~?
M : ~?
A }} =>
pose proof ctxsub_exp_helper _ _ _ H
- |
{{ ~?
Γ ⊢ ~?
M ≈ ~?
N : ~?
A }} =>
pose proof ctxsub_exp_eq_helper _ _ _ _ H
- |
{{ ~?
Γ ⊢s ~?σ
: ~?
Δ }} =>
pose proof ctxsub_sub_helper _ _ _ H
- |
{{ ~?
Γ ⊢s ~?σ
≈ ~?τ
: ~?
Δ }} =>
pose proof ctxsub_sub_eq_helper _ _ _ _ H
- |
{{ ~?
Γ ⊢ ~?
M ⊆ ~?
M' }} =>
pose proof ctxsub_subtyp_helper _ _ _ H
+ |
{{ ^?
Γ ⊢ ^?
M : ^?
A }} =>
pose proof ctxsub_exp_helper _ _ _ H
+ |
{{ ^?
Γ ⊢ ^?
M ≈ ^?
N : ^?
A }} =>
pose proof ctxsub_exp_eq_helper _ _ _ _ H
+ |
{{ ^?
Γ ⊢s ^?σ
: ^?
Δ }} =>
pose proof ctxsub_sub_helper _ _ _ H
+ |
{{ ^?
Γ ⊢s ^?σ
≈ ^?τ
: ^?
Δ }} =>
pose proof ctxsub_sub_eq_helper _ _ _ _ H
+ |
{{ ^?
Γ ⊢ ^?
M ⊆ ^?
M' }} =>
pose proof ctxsub_subtyp_helper _ _ _ H
end.
diff --git a/Mcltt.Core.Syntactic.Presup.html b/Mcltt.Core.Syntactic.Presup.html
index 642df23..7652650 100644
--- a/Mcltt.Core.Syntactic.Presup.html
+++ b/Mcltt.Core.Syntactic.Presup.html
@@ -37,11 +37,11 @@
Mcltt.Core.Syntactic.Presup
#[
local]
Ltac gen_presup_ctx H :=
match type of H with
- |
{{ ⊢ ~?
Γ ≈ ~?
Δ }} =>
+ |
{{ ⊢ ^?
Γ ≈ ^?
Δ }} =>
let HΓ :=
fresh "HΓ"
in
let HΔ :=
fresh "HΔ"
in
pose proof presup_ctx_eq H as [
HΓ HΔ]
- |
{{ ⊢ ~?
Γ ⊆ ~?
Δ }} =>
+ |
{{ ⊢ ^?
Γ ⊆ ^?
Δ }} =>
let HΓ :=
fresh "HΓ"
in
let HΔ :=
fresh "HΔ"
in
pose proof presup_ctx_sub H as [
HΓ HΔ]
@@ -51,31 +51,31 @@
Mcltt.Core.Syntactic.Presup
#[
local]
Ltac gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp H :=
match type of H with
- |
{{ ~?
Γ ⊢ ~?
M ≈ ~?
N : ~?
A }} =>
+ |
{{ ^?
Γ ⊢ ^?
M ≈ ^?
N : ^?
A }} =>
let HΓ :=
fresh "HΓ"
in
let i :=
fresh "i"
in
let HM :=
fresh "HM"
in
let HN :=
fresh "HN"
in
let HAi :=
fresh "HAi"
in
pose proof presup_exp_eq _ _ _ _ H as [
HΓ [
HM [
HN [
i HAi]]]]
- |
{{ ~?
Γ ⊢s ~?σ
≈ ~?τ
: ~?
Δ }} =>
+ |
{{ ^?
Γ ⊢s ^?σ
≈ ^?τ
: ^?
Δ }} =>
let HΓ :=
fresh "HΓ"
in
let Hσ :=
fresh "Hσ"
in
let Hτ :=
fresh "Hτ"
in
let HΔ :=
fresh "HΔ"
in
pose proof presup_sub_eq _ _ _ _ H as [
HΓ [
Hσ [
Hτ
HΔ]]]
- |
{{ ~?
Γ ⊢ ~?
M ⊆ ~?
N }} =>
+ |
{{ ^?
Γ ⊢ ^?
M ⊆ ^?
N }} =>
let HΓ :=
fresh "HΓ"
in
let i :=
fresh "i"
in
let HM :=
fresh "HM"
in
let HN :=
fresh "HN"
in
pose proof presup_subtyp _ _ _ H as [
HΓ [
i [
HM HN]]]
- |
{{ ~?
Γ ⊢ ~?
M : ~?
A }} =>
+ |
{{ ^?
Γ ⊢ ^?
M : ^?
A }} =>
let HΓ :=
fresh "HΓ"
in
let i :=
fresh "i"
in
let HAi :=
fresh "HAi"
in
pose proof presup_exp H as [
HΓ [
i HAi]]
- |
{{ ~?
Γ ⊢s ~?σ
: ~?
Δ }} =>
+ |
{{ ^?
Γ ⊢s ^?σ
: ^?
Δ }} =>
let HΓ :=
fresh "HΓ"
in
let HΔ :=
fresh "HΔ"
in
pose proof presup_sub H as [
HΓ HΔ]
diff --git a/Mcltt.Core.Syntactic.Syntax.html b/Mcltt.Core.Syntactic.Syntax.html
index d11e771..93982d7 100644
--- a/Mcltt.Core.Syntactic.Syntax.html
+++ b/Mcltt.Core.Syntactic.Syntax.html
@@ -226,7 +226,7 @@
Mcltt.Core.Syntactic.Syntax
Notation "e [ s ]" := (
a_sub e s) (
in custom exp at level 0,
e custom exp,
s custom exp at level 60,
left associativity,
format "e [ s ]") :
mcltt_scope.
Notation "( x )" :=
x (
in custom exp at level 0,
x custom exp at level 60) :
mcltt_scope.
-
Notation "~ x" :=
x (
in custom exp at level 0,
x constr at level 0) :
mcltt_scope.
+
Notation "'^' x" :=
x (
in custom exp at level 0,
x constr at level 0) :
mcltt_scope.
Notation "x" :=
x (
in custom exp at level 0,
x ident) :
mcltt_scope.
Notation "'λ' A e" := (
a_fn A e) (
in custom exp at level 1,
A custom exp at level 0,
e custom exp at level 60) :
mcltt_scope.
Notation "f x .. y" := (
a_app .. (
a_app f x) ..
y) (
in custom exp at level 40,
f custom exp,
x custom exp at next level,
y custom exp at next level) :
mcltt_scope.
@@ -252,7 +252,7 @@
Mcltt.Core.Syntactic.Syntax
Notation "n{{{ x }}}" :=
x (
at level 0,
x custom nf at level 99,
format "'n{{{' x '}}}'") :
mcltt_scope.
Notation "( x )" :=
x (
in custom nf at level 0,
x custom nf at level 60) :
mcltt_scope.
-
Notation "~ x" :=
x (
in custom nf at level 0,
x constr at level 0) :
mcltt_scope.
+
Notation "'^' x" :=
x (
in custom nf at level 0,
x constr at level 0) :
mcltt_scope.
Notation "x" :=
x (
in custom nf at level 0,
x ident) :
mcltt_scope.
Notation "'λ' A e" := (
nf_fn A e) (
in custom nf at level 2,
A custom nf at level 1,
e custom nf at level 60) :
mcltt_scope.
Notation "f x .. y" := (
ne_app .. (
ne_app f x) ..
y) (
in custom nf at level 40,
f custom nf,
x custom nf at next level,
y custom nf at next level) :
mcltt_scope.
diff --git a/Mcltt.Core.Syntactic.System.Tactics.html b/Mcltt.Core.Syntactic.System.Tactics.html
index 8c8bd88..8ee7b5a 100644
--- a/Mcltt.Core.Syntactic.System.Tactics.html
+++ b/Mcltt.Core.Syntactic.System.Tactics.html
@@ -37,10 +37,10 @@
Mcltt.Core.Syntactic.System.Tactics
#[
global]
Ltac pi_univ_level_tac :=
match goal with
- | |-
{{ ~_ ⊢s ~_ : ~_ }} =>
mauto 4
- |
H :
{{ ~?
Δ ⊢ ~?
A : Type@?
j }} |-
{{ ~?
Δ , ~?
A ⊢ ~?
B : Type@?
i }} =>
+ | |-
{{ ^_ ⊢s ^_ : ^_ }} =>
mauto 4
+ |
H :
{{ ^?
Δ ⊢ ^?
A : Type@?
j }} |-
{{ ^?
Δ , ^?
A ⊢ ^?
B : Type@?
i }} =>
eapply lift_exp_max_right;
mauto 4
- | |-
{{ ~?
Δ ⊢ ~?
A : Type@?
j }} =>
+ | |-
{{ ^?
Δ ⊢ ^?
A : Type@?
j }} =>
eapply lift_exp_max_left;
mauto 4
end.
@@ -52,7 +52,7 @@
Mcltt.Core.Syntactic.System.Tactics
#[
local]
Ltac invert_wf_ctx1 H :=
match type of H with
- |
{{ ⊢ ~_ , ~_ }} =>
+ |
{{ ⊢ ^_ , ^_ }} =>
let H' :=
fresh "H"
in
pose proof H as H';
progressive_invert H'
diff --git a/Mcltt.Extraction.Subtyping.html b/Mcltt.Extraction.Subtyping.html
index 17a3dbe..d4467dc 100644
--- a/Mcltt.Extraction.Subtyping.html
+++ b/Mcltt.Extraction.Subtyping.html
@@ -40,12 +40,12 @@
Mcltt.Extraction.Subtyping
Ltac subtyping_tac :=
intros;
lazymatch goal with
- | |-
{{ ⊢anf ~_ ⊆ ~_ }} =>
+ | |-
{{ ⊢anf ^_ ⊆ ^_ }} =>
subst;
mauto 4;
try congruence;
econstructor;
simpl;
trivial
- | |-
~ {{ ⊢anf ~_ ⊆ ~_ }} =>
+ | |-
~ {{ ⊢anf ^_ ⊆ ^_ }} =>
let H :=
fresh "H"
in
intro H;
dependent destruction H;
simpl in *;
try lia;
diff --git a/Mcltt.Extraction.TypeCheck.html b/Mcltt.Extraction.TypeCheck.html
index fa838e2..0d289f3 100644
--- a/Mcltt.Extraction.TypeCheck.html
+++ b/Mcltt.Extraction.TypeCheck.html
@@ -45,10 +45,10 @@
Mcltt.Extraction.TypeCheck
#[
local]
Ltac impl_obl_tac1 :=
match goal with
- | |-
~_ =>
intro
- |
H:
{{ ⊢ ~_, ~_ }} |-
_ =>
inversion_clear H
- |
H:
{{ # _ : ~_ ∈ ⋅ }} |-
_ =>
inversion_clear H
- |
H:
{{ # (S _) : ~_ ∈ ~_, ~_ }} |-
_ =>
inversion_clear H
+ | |-
~ _ =>
intro
+ |
H:
{{ ⊢ ^_, ^_ }} |-
_ =>
inversion_clear H
+ |
H:
{{ # _ : ^_ ∈ ⋅ }} |-
_ =>
inversion_clear H
+ |
H:
{{ # (S _) : ^_ ∈ ^_, ^_ }} |-
_ =>
inversion_clear H
end.
@@ -145,14 +145,14 @@
Mcltt.Extraction.TypeCheck
{{ ⊢ G }} ->
forall M :
typ,
type_infer_order M ->
-
({ B : nf | {{ G ⊢a M ⟹ B }} /\ (exists i :
nat, {{ G ⊢a ~(nf_to_exp B) ⟹ Type@i }}) } + { forall C :
nf,
~ {{ G ⊢a M ⟹ C }} }))
+
({ B : nf | {{ G ⊢a M ⟹ B }} /\ (exists i :
nat, {{ G ⊢a ^(nf_to_exp B) ⟹ Type@i }}) } + { forall C :
nf,
~ {{ G ⊢a M ⟹ C }} }))
|-
_ =>
clear H
|
H: (
forall G :
ctx,
{{ ⊢ G }} ->
forall M :
typ,
type_infer_order M ->
-
({ B : nf | {{ G ⊢a M ⟹ B }} /\ (exists i :
nat, {{ G ⊢a ~(nf_to_exp B) ⟹ Type@i }}) } + { forall C :
nf,
~ {{ G ⊢a M ⟹ C }} }))
+
({ B : nf | {{ G ⊢a M ⟹ B }} /\ (exists i :
nat, {{ G ⊢a ^(nf_to_exp B) ⟹ Type@i }}) } + { forall C :
nf,
~ {{ G ⊢a M ⟹ C }} }))
|-
_ =>
clear H
end.
@@ -176,17 +176,17 @@
Mcltt.Extraction.TypeCheck
end;
destruct_conjs;
match goal with
- | |-
{{ ⊢ ~_ }} =>
gen_presups;
mautosolve 4
- |
H:
{{ ~?
G ⊢ ~?
A : Type@?
i }} |-
{{ ~?
G ⊢ ~?
A : Type@(Nat.max ?
i ?
j) }} =>
apply lift_exp_max_left;
mautosolve 4
- |
H:
{{ ~?
G ⊢ ~?
A : Type@?
j }} |-
{{ ~?
G ⊢ ~?
A : Type@(Nat.max ?
i ?
j) }} =>
apply lift_exp_max_right;
mautosolve 4
- | |-
{{ ~_ ⊢ ~_ : ~_ }} =>
gen_presups;
mautosolve 4
- | |-
_ -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }} =>
+ | |-
{{ ⊢ ^_ }} =>
gen_presups;
mautosolve 4
+ |
H:
{{ ^?
G ⊢ ^?
A : Type@?
i }} |-
{{ ^?
G ⊢ ^?
A : Type@(Nat.max ?
i ?
j) }} =>
apply lift_exp_max_left;
mautosolve 4
+ |
H:
{{ ^?
G ⊢ ^?
A : Type@?
j }} |-
{{ ^?
G ⊢ ^?
A : Type@(Nat.max ?
i ?
j) }} =>
apply lift_exp_max_right;
mautosolve 4
+ | |-
{{ ^_ ⊢ ^_ : ^_ }} =>
gen_presups;
mautosolve 4
+ | |-
_ -> ~ {{ ^_ ⊢a ^_ ⟸ ^_ }} =>
let H :=
fresh "H"
in
intros ?
H;
directed dependent destruction H;
functional_alg_type_infer_rewrite_clear;
firstorder
- | |-
_ -> (forall A :
nf,
~ {{ ~_ ⊢a ~_ ⟹ ~_ }}) =>
+ | |-
_ -> (forall A :
nf,
~ {{ ^_ ⊢a ^_ ⟹ ^_ }}) =>
unfold not in *;
intros;
progressive_inversion;
@@ -195,8 +195,8 @@
Mcltt.Extraction.TypeCheck
| |-
type_infer_order _ =>
eassumption;
fail 1
| |-
type_check_order _ =>
eassumption;
fail 1
| |-
subtyping_order ?
G ?
A ?
B =>
-
enough (
exists i, {{ G ⊢ A : ~n{{{ Type@i }}} }})
as [? [? []]%
soundness_ty];
-
only 1:
enough (
exists j, {{ G ⊢ B : ~n{{{ Type@j }}} }})
as [? [? []]%
soundness_ty];
+
enough (
exists i, {{ G ⊢ A : ^n{{{ Type@i }}} }})
as [? [? []]%
soundness_ty];
+
only 1:
enough (
exists j, {{ G ⊢ B : ^n{{{ Type@j }}} }})
as [? [? []]%
soundness_ty];
only 1:
solve [
econstructor;
eauto 3
using nbe_ty_order_sound];
solve [
mauto 4
using alg_type_infer_sound]
|
_ =>
try mautosolve 3
@@ -244,7 +244,7 @@
Mcltt.Extraction.TypeCheck
let*o (exist _ C _) := type_infer G _ M' _ while _ in
let*o (existT _ A (exist _ B _)) := get_subterms_of_pi_nf C while _ in
let*b->o _ := type_check G (
A :
nf)
_ N' _ while _ in
-
let (
B',
_) :=
nbe_ty_impl G {{{ ~(B :
nf)[Id,,N'] }}} _ in
+
let (
B',
_) :=
nbe_ty_impl G {{{ ^(B :
nf)[Id,,N'] }}} _ in
pureo (exist _ B' _)
|
{{{ #x }}} =>
let*o (exist _ A _) := lookup G _ x while _ in
@@ -265,7 +265,7 @@
Mcltt.Extraction.TypeCheck
clear_defs.
functional_alg_type_infer_rewrite_clear.
eexists.
-
assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G, ℕ ⊢ A' : ^n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
mauto 3.
Qed.
@@ -274,17 +274,17 @@
Mcltt.Extraction.TypeCheck
clear_defs.
functional_alg_type_infer_rewrite_clear.
eexists.
-
assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G, ℕ ⊢ A' : ^n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
mauto 3.
Qed.
Next Obligation.
clear_defs.
-
enough (
exists i, {{ G ⊢ A'[Id,,M'] : ~n{{{ Type@i }}} }})
as [? [? []]%
exp_eq_refl%
completeness_ty]
+
enough (
exists i, {{ G ⊢ A'[Id,,M'] : ^n{{{ Type@i }}} }})
as [? [? []]%
exp_eq_refl%
completeness_ty]
by eauto 3
using nbe_ty_order_sound.
eexists.
-
assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G, ℕ ⊢ A' : ^n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
assert {{ G ⊢ ℕ : Type@0 }} by mauto 3.
mauto 4
using alg_type_check_sound.
Qed.
@@ -293,7 +293,7 @@
Mcltt.Extraction.TypeCheck
Next Obligation.
clear_defs.
split; [
mauto 3 |].
-
assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G, ℕ ⊢ A' : ^n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
assert {{ G ⊢ ℕ : Type@0 }} by mauto 3.
assert {{ G ⊢ A'[Id,,M'] ≈ A'' : Type@i }} by (
eapply soundness_ty';
mauto 4
using alg_type_check_sound).
assert (
user_exp A'')
by trivial using user_exp_nf.
@@ -334,13 +334,13 @@
Mcltt.Extraction.TypeCheck
assert {{ G ⊢ A' ≈ A'' : Type@i }} by (
eapply soundness_ty';
mauto 4
using alg_type_check_sound).
assert {{ ⊢ G, A' }} by mauto 2.
assert {{ G ⊢ A'' : Type@i }} by (
gen_presups;
mauto 2).
-
assert {{ ⊢ G, ~(A'' :
exp) }} by mauto 2.
+
assert {{ ⊢ G, ^(A'' :
exp) }} by mauto 2.
assert {{ G, A' ⊢ B' : Type@H1 }} by mauto 4
using alg_type_infer_sound.
-
assert {{ G, ~(A'' :
exp) ⊢ B' : Type@H1 }} by mauto 4.
+
assert {{ G, ^(A'' :
exp) ⊢ B' : Type@H1 }} by mauto 4.
assert (
user_exp A'')
by trivial using user_exp_nf.
assert (
exists j, {{ G ⊢a A'' ⟹ Type@j }} /\ j <= i)
as [? []]
by (
gen_presups;
mauto 3).
assert (
user_exp B')
by trivial using user_exp_nf.
-
assert (
exists k, {{ G, ~(A'' :
exp) ⊢a B' ⟹ Type@k }} /\ k <= H1)
as [? []]
by (
gen_presups;
mauto 3).
+
assert (
exists k, {{ G, ^(A'' :
exp) ⊢a B' ⟹ Type@k }} /\ k <= H1)
as [? []]
by (
gen_presups;
mauto 3).
firstorder mauto 3.
Qed.
@@ -357,10 +357,10 @@
Mcltt.Extraction.TypeCheck
clear_defs.
functional_alg_type_infer_rewrite_clear.
progressive_inversion.
-
assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
-
assert {{ G, ~(A :
exp) ⊢ s : ~n{{{ Type@j }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G ⊢ A : ^n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G, ^(A :
exp) ⊢ s : ^n{{{ Type@j }}} }} by mauto 4
using alg_type_infer_sound.
assert {{ G ⊢ N' : A }} by mauto 3
using alg_type_check_sound.
-
assert {{ G ⊢ s[Id,,N'] : ~n{{{ Type@j }}} }} as [? []]%
soundness_ty by mauto 3.
+
assert {{ G ⊢ s[Id,,N'] : ^n{{{ Type@j }}} }} as [? []]%
soundness_ty by mauto 3.
mauto 3
using nbe_ty_order_sound.
Qed.
@@ -370,8 +370,8 @@
Mcltt.Extraction.TypeCheck
functional_alg_type_infer_rewrite_clear.
progressive_inversion.
split; [
mauto 3 |].
-
assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
-
assert {{ G, ~(A :
exp) ⊢ s : ~n{{{ Type@j }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G ⊢ A : ^n{{{ Type@i }}} }} by mauto 4
using alg_type_infer_sound.
+
assert {{ G, ^(A :
exp) ⊢ s : ^n{{{ Type@j }}} }} by mauto 4
using alg_type_infer_sound.
assert {{ G ⊢ s[Id,,N'] ≈ B' : Type@j }} by (
eapply soundness_ty';
mauto 4
using alg_type_check_sound).
assert (
user_exp B')
by trivial using user_exp_nf.
assert (
exists k, {{ G ⊢a B' ⟹ Type@k }} /\ k <= j)
as [? []]
by (
gen_presups;
mauto 3).
@@ -473,13 +473,13 @@
Mcltt.Extraction.TypeCheck
Qed.
Next Obligation.
assert {{ ⊢ ⋅ }} by mauto 2.
-
assert {{ ⋅ ⊢ A : ~n{{{ Type@i }}} }} by mauto 2
using alg_type_infer_sound.
+
assert {{ ⋅ ⊢ A : ^n{{{ Type@i }}} }} by mauto 2
using alg_type_infer_sound.
simpl in *.
firstorder.
Qed.
Next Obligation.
assert {{ ⊢ ⋅ }} by mauto 2.
-
assert {{ ⋅ ⊢ A : ~n{{{ Type@i }}} }} by mauto 3
using alg_type_infer_sound.
+
assert {{ ⋅ ⊢ A : ^n{{{ Type@i }}} }} by mauto 3
using alg_type_infer_sound.
simpl in *.
mauto 3
using alg_type_check_sound.
Qed.
diff --git a/indexpage.html b/indexpage.html
index 8c97b65..a9921b6 100644
--- a/indexpage.html
+++ b/indexpage.html
@@ -894,7 +894,7 @@
Global Index
domain:_ _ .. _ (mcltt_scope) [notation, in
Mcltt.Core.Semantic.Domain]
domain:λ _ _ (mcltt_scope) [notation, in
Mcltt.Core.Semantic.Domain]
domain:_ (mcltt_scope) [notation, in
Mcltt.Core.Semantic.Domain]
-
domain:~ _ (mcltt_scope) [notation, in
Mcltt.Core.Semantic.Domain]
+
domain:^ _ (mcltt_scope) [notation, in
Mcltt.Core.Semantic.Domain]
domain:( _ ) (mcltt_scope) [notation, in
Mcltt.Core.Semantic.Domain]
d{{{ _ }}} (mcltt_scope) [notation, in
Mcltt.Core.Semantic.Domain]
Domain_Notations [module, in
Mcltt.Core.Semantic.Domain]
@@ -1891,7 +1891,7 @@
Global Index
nf:_ _ .. _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
nf:λ _ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
nf:_ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
-
nf:~ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
+
nf:^ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
nf:( _ ) (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
n{{{ _ }}} (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:_ , _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
@@ -1911,7 +1911,7 @@
Global Index
exp:_ _ .. _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:λ _ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:_ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
-
exp:~ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
+
exp:^ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:( _ ) (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
{{{ _ }}} (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
@@ -2273,7 +2273,7 @@
Notation Index
domain:_ _ .. _ (mcltt_scope) [in
Mcltt.Core.Semantic.Domain]
domain:λ _ _ (mcltt_scope) [in
Mcltt.Core.Semantic.Domain]
domain:_ (mcltt_scope) [in
Mcltt.Core.Semantic.Domain]
-
domain:~ _ (mcltt_scope) [in
Mcltt.Core.Semantic.Domain]
+
domain:^ _ (mcltt_scope) [in
Mcltt.Core.Semantic.Domain]
domain:( _ ) (mcltt_scope) [in
Mcltt.Core.Semantic.Domain]
d{{{ _ }}} (mcltt_scope) [in
Mcltt.Core.Semantic.Domain]
S
@@ -2288,7 +2288,7 @@
Notation Index
nf:_ _ .. _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
nf:λ _ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
nf:_ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
-
nf:~ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
+
nf:^ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
nf:( _ ) (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
n{{{ _ }}} (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:_ , _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
@@ -2308,7 +2308,7 @@
Notation Index
exp:_ _ .. _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:λ _ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:_ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
-
exp:~ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
+
exp:^ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:( _ ) (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
{{{ _ }}} (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]