From ec807c02aa90979ca753ca08697c759977cf1327 Mon Sep 17 00:00:00 2001 From: Ailrun Date: Fri, 4 Oct 2024 00:52:48 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20Beluga-l?= =?UTF-8?q?ang/McLTT@8a8bde5f5568aba1ee71d8a697a5535f927fbc0e=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mcltt.Algorithmic.Subtyping.Lemmas.html | 10 ++-- Mcltt.Algorithmic.Typing.Lemmas.html | 32 +++++----- Mcltt.Core.Completeness.NatCases.html | 32 +++++----- ....Core.Completeness.TermStructureCases.html | 4 +- Mcltt.Core.Semantic.Consequences.html | 24 ++++---- Mcltt.Core.Semantic.Domain.html | 2 +- ....Core.Semantic.Evaluation.Definitions.html | 2 +- Mcltt.Core.Semantic.Evaluation.Lemmas.html | 8 +-- Mcltt.Core.Semantic.PER.CoreTactics.html | 2 +- Mcltt.Core.Semantic.PER.Definitions.html | 2 +- Mcltt.Core.Semantic.PER.Lemmas.html | 32 +++++----- Mcltt.Core.Semantic.Readback.Lemmas.html | 6 +- Mcltt.Core.Semantic.Realizability.html | 8 +-- Mcltt.Core.Soundness.FunctionCases.html | 12 ++-- ....Soundness.LogicalRelation.CoreLemmas.html | 4 +- ...Soundness.LogicalRelation.Definitions.html | 2 +- ...Core.Soundness.LogicalRelation.Lemmas.html | 20 +++---- Mcltt.Core.Soundness.NatCases.html | 36 +++++------ Mcltt.Core.Soundness.Realizability.html | 8 +-- Mcltt.Core.Soundness.Weakening.Lemmas.html | 2 +- Mcltt.Core.Syntactic.Corollaries.html | 6 +- Mcltt.Core.Syntactic.CtxSub.html | 10 ++-- Mcltt.Core.Syntactic.Presup.html | 14 ++--- Mcltt.Core.Syntactic.Syntax.html | 4 +- Mcltt.Core.Syntactic.System.Tactics.html | 8 +-- Mcltt.Extraction.Subtyping.html | 4 +- Mcltt.Extraction.TypeCheck.html | 60 +++++++++---------- indexpage.html | 12 ++-- 28 files changed, 183 insertions(+), 183 deletions(-) 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 }} |- _ =>
      
@@ -1050,24 +1050,24 @@

Mcltt.Core.Semantic.PER.Lemmas

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" in
  match goal with
-    | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
-        H2 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
+    | H1 : {{ DF ^?Γ ≈ ^_ ∈ per_ctx_env ↘ ?R1 }},
+        H2 : {{ DF ^?Γ ≈ ^_ ∈ per_ctx_env ↘ ?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_ctx_env_right_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
        end
-    | H1 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R1 }},
-        H2 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
+    | H1 : {{ DF ^_ ≈ ^?Δ ∈ per_ctx_env ↘ ?R1 }},
+        H2 : {{ DF ^_ ≈ ^?Δ ∈ per_ctx_env ↘ ?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_ctx_env_left_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
        end
-    | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
-        H2 : {{ DF ~_ ≈ ~?Γ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
+    | H1 : {{ DF ^?Γ ≈ ^_ ∈ per_ctx_env ↘ ?R1 }},
+        H2 : {{ DF ^_ ≈ ^?Γ ∈ per_ctx_env ↘ ?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. (* nbe_ty_order G {{{ A'Id,,M' }}} *)
    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. (* {{ G ⊢a rec M' return A' | zero -> MZ | succ -> MS end ⟹ A'' }} /\ (exists j, {{ G ⊢a A'' ⟹ Type@j }}) *)
    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. (* exists i, {{ ⋅ ⊢ A : Type@i }} *)
    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. (* {{ ⋅ ⊢ M : A }} *)
    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]