diff --git a/Mcltt.Core.Completeness.Consequences.Types.html b/Mcltt.Core.Completeness.Consequences.Types.html index 9d3d03b..66c96ce 100644 --- a/Mcltt.Core.Completeness.Consequences.Types.html +++ b/Mcltt.Core.Completeness.Consequences.Types.html @@ -122,176 +122,6 @@

Mcltt.Core.Completeness.Consequences.Types


#[export]
Hint Resolve is_typ_constr_and_exp_eq_nat_implies_eq_nat : mcltt.
- -
-(* We cannot use this spec as the definition of typ_subsumption as
-   then its transitivity requires exp_eq_typ_implies_eq_level or a similar semantic lemma *)
- -
-(* Lemma typ_subsumption_spec : forall {Γ A A'}, *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     {{ ⊢ Γ }} /\ exists j, {{ Γ ⊢ A ≈ A' : Type@j }} \/ exists i i', i < i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }} /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H. *)
-(*   dependent induction H; split; mauto 3. *)
-(*   - (* typ_subsumption_typ *) *)
-(*     eexists. *)
-(*     right. *)
-(*     do 2 eexists. *)
-(*     repeat split; revgoals; mauto. *)
-(*   - (* typ_subsumption_trans *) *)
-(*     destruct IHtyp_subsumption1 as ? [? [| [i1 [i1']]]]; destruct IHtyp_subsumption2 as ? [? [| [i2 [i2']]]]; *)
-(*       destruct_conjs; *)
-(*       only 1: mautosolve 4; *)
-(*       eexists; right; do 2 eexists. *)
-(*     + (* left & right *) *)
-(*       split; eassumption |. *)
-(*       solve mauto using lift_exp_eq_max_left. *)
-(*     + (* right & left *) *)
-(*       split; eassumption |. *)
-(*       solve mauto using lift_exp_eq_max_right. *)
-(*     + exvar nat ltac:(fun j => assert {{ Γ ⊢ Type@i2 ≈ Type@i1' : Type@j }} by mauto). *)
-(*       replace i2 with i1' in * by mauto. *)
-(*       split; etransitivity; revgoals; eassumption |. *)
-(*       mauto 4 using lift_exp_eq_max_left, lift_exp_eq_max_right. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_spec : mcltt. *)
- -
-(* Lemma not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
-(*     is_typ_constr A -> *)
-(*     (forall i, A <> {{{ Type@i }}}) -> *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * ? ? H*)
-(*   destruct_all; mauto. *)
-(*   exfalso. *)
-(*   intuition. *)
-(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : mcltt. *)
- -
-(* Lemma not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
-(*     is_typ_constr A' -> *)
-(*     (forall i, A' <> {{{ Type@i }}}) -> *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * ? ? H*)
-(*   destruct_all; mauto. *)
-(*   exfalso. *)
-(*   intuition. *)
-(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : mcltt. *)
- -
-(* Corollary typ_subsumption_left_nat : forall {Γ A'}, *)
-(*     {{ Γ ⊢ ℕ ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ ℕ ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H*)
-(*   congruence. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_left_nat : mcltt. *)
- -
-(* Corollary typ_subsumption_left_pi : forall {Γ A B C'}, *)
-(*     {{ Γ ⊢ Π A B ⊆ C' }} -> *)
-(*     exists j, {{ Γ ⊢ Π A B ≈ C' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H*)
-(*   congruence. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_left_pi : mcltt. *)
- -
-(* Corollary typ_subsumption_left_typ : forall {Γ i A'}, *)
-(*     {{ Γ ⊢ Type@i ⊆ A' }} -> *)
-(*     exists j i', i <= i' /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H*)
-(*   destruct_all; mauto. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
-(*   mauto using PeanoNat.Nat.lt_le_incl. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_left_typ : mcltt. *)
- -
-(* Corollary typ_subsumption_right_nat : forall {Γ A}, *)
-(*     {{ Γ ⊢ A ⊆ ℕ }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ ℕ : Type@j }}. *)
-(* Proof. *)
-(*   intros * H*)
-(*   congruence. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_right_nat : mcltt. *)
- -
-(* Corollary typ_subsumption_right_pi : forall {Γ C A' B'}, *)
-(*     {{ Γ ⊢ C ⊆ Π A' B' }} -> *)
-(*     exists j, {{ Γ ⊢ C ≈ Π A' B' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H*)
-(*   congruence. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_right_pi : mcltt. *)
- -
-(* Corollary typ_subsumption_right_typ : forall {Γ A i'}, *)
-(*     {{ Γ ⊢ A ⊆ Type@i' }} -> *)
-(*     exists j i, i <= i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }}. *)
-(* Proof. *)
-(*   intros * H*)
-(*   destruct_all; mauto. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
-(*   mauto using PeanoNat.Nat.lt_le_incl. *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_right_typ : mcltt. *)
- -
-(* Corollary typ_subsumption_typ_spec : forall {Γ i i'}, *)
-(*     {{ Γ ⊢ Type@i ⊆ Type@i' }} -> *)
-(*     {{ ⊢ Γ }} /\ i <= i'. *)
-(* Proof with mautosolve. *)
-(*   intros * H. *)
-(*   pose proof (typ_subsumption_left_typ H). *)
-(*   destruct_conjs. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst... *)
-(* Qed. *)
- -
-(* [export] *)
-(* Hint Resolve typ_subsumption_typ_spec : mcltt. *)
+ +
+We use the next equality to make unification on `out_rel` works +
+
    (out_rel = fun c c' (equiv_c_c' : R c c') m m' =>
                 forall R',
                   rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} R' ->
@@ -145,8 +150,7 @@

Mcltt.Core.Completeness.FunctionCases

  - intros.
    eapply rel_exp_pi_core; eauto.
    reflexivity.
-  - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
-    apply Equivalence_Reflexive.
+  - solve_refl.
Qed.

@@ -179,8 +183,7 @@

Mcltt.Core.Completeness.FunctionCases

  - eapply rel_exp_pi_core; eauto; try reflexivity.
    intros.
    extract_output_info_with ρσ c ρ'σ' c' env_relΔA...
-  - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
-    apply Equivalence_Reflexive.
+  - solve_refl.
Qed.

diff --git a/Mcltt.Core.Completeness.SubtypingCases.html b/Mcltt.Core.Completeness.SubtypingCases.html index dd7965c..b7460e6 100644 --- a/Mcltt.Core.Completeness.SubtypingCases.html +++ b/Mcltt.Core.Completeness.SubtypingCases.html @@ -137,7 +137,12 @@

Mcltt.Core.Completeness.SubtypingCases

      by (intros; apply_relation_equivalence; unshelve eexists; eassumption).

-  (* The proofs for the next two assertions are basically the same *)
+
+ +
+The proofs for the next two assertions are basically the same +
+
  exvar (relation domain)
    ltac:(fun R => assert ({{ DF Π m0 ρ B ≈ Π m1 ρ' B ∈ per_univ_elem (Nat.max i k) ↘ R }})).
  {
diff --git a/Mcltt.Core.Semantic.PER.Definitions.html b/Mcltt.Core.Semantic.PER.Definitions.html index dc36e43..af6a698 100644 --- a/Mcltt.Core.Semantic.PER.Definitions.html +++ b/Mcltt.Core.Semantic.PER.Definitions.html @@ -39,9 +39,14 @@

Mcltt.Core.Semantic.PER.Definitions

Notation "'DF' a ≈ b ∈ R ↘ R'" := ((R R' a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr, R' constr).
Notation "'Exp' a ≈ b ∈ R" := (R a b : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr).
Notation "'EF' a ≈ b ∈ R ↘ R'" := (R R' a b : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr, R' constr).
-(* Precedences of the next notations follow the ones in the standard library.
-   However, we do not use the ones in the standard library so that we can change
-   the relation if necessary in the future. *)
+
+ +
+Precedences of the next notations follow the ones in the standard library. + However, we do not use the ones in the standard library so that we can change + the relation if necessary in the future. +
+
Notation "R ~> R'" := (subrelation R R') (at level 70, right associativity).
Notation "R <~> R'" := (relation_equivalence R R') (at level 95, no associativity).
@@ -52,10 +57,10 @@

Mcltt.Core.Semantic.PER.Definitions

-Helper Bundles +

Helper Bundles

+ Related modulo evaluation
-(* Related modulo evaluation *)
Inductive rel_mod_eval (R : relation domain -> domain -> domain -> Prop) A ρ A' ρ' R' : Prop := mk_rel_mod_eval : forall a a', {{ ⟦ A ⟧ ρ ↘ a }} -> {{ ⟦ A' ⟧ ρ' ↘ a' }} -> {{ DF a ≈ a' ∈ R ↘ R' }} -> rel_mod_eval R A ρ A' ρ' R'.
#[global]
Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
@@ -63,7 +68,12 @@

Mcltt.Core.Semantic.PER.Definitions

Hint Constructors rel_mod_eval : mcltt.

-(* Related modulo application *)
+
+ +
+Related modulo application +
+
Inductive rel_mod_app f a f' a' (R : relation domain) : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app f a f' a' R.
#[global]
Arguments mk_rel_mod_app {_ _ _ _ _}.
@@ -74,7 +84,8 @@

Mcltt.Core.Semantic.PER.Definitions

-(Some Elements of) PER Lattice +

(Some Elements of) PER Lattice

+
@@ -131,7 +142,8 @@

Mcltt.Core.Semantic.PER.Definitions

-Universe/Element PER Definition +

Universe/Element PER Definition

+
@@ -249,7 +261,8 @@

Mcltt.Core.Semantic.PER.Definitions

-Universe/Element PER Induction Principle +

Universe/Element PER Induction Principle

+
@@ -338,7 +351,8 @@

Mcltt.Core.Semantic.PER.Definitions

-Context/Environment PER +

Context/Environment PER

+
diff --git a/Mcltt.Core.Semantic.PER.Lemmas.html b/Mcltt.Core.Semantic.PER.Lemmas.html index db68aaa..85023e1 100644 --- a/Mcltt.Core.Semantic.PER.Lemmas.html +++ b/Mcltt.Core.Semantic.PER.Lemmas.html @@ -497,7 +497,12 @@

Mcltt.Core.Semantic.PER.Lemmas

      end
  | H1 : {{ DF ~?a ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
      H2 : {{ DF ~_ ≈ ~?a ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
-      (* Order matters less here as H1 and H2 cannot be exchanged *)
+      
+ +
+Order matters less here as H1 and H2 cannot be exchanged +
+
      assert_fails (unify R1 R2);
      match goal with
      | H : R1 <~> R2 |- _ => fail 1
@@ -532,7 +537,12 @@

Mcltt.Core.Semantic.PER.Lemmas

    [> split;
     [ intros * HT2; basic_invert_per_univ_elem HT2
     | intros * HTR1 HTR2; apply_relation_equivalence ] ..]; mauto.
-  - (* univ case *)
+  -
+ +
+univ case +
+
    subst.
    destruct HTR1, HTR2.
    functional_eval_rewrite_clear.
@@ -540,9 +550,19 @@

Mcltt.Core.Semantic.PER.Lemmas

    eexists.
    specialize (H2 _ _ _ H0) as [].
    intuition.
-  - (* nat case *)
+  -
+ +
+nat case +
+
    idtac...
-  - (* pi case *)
+  -
+ +
+pi case +
+
    destruct_conjs.
    basic_per_univ_elem_econstructor; eauto.
    + handle_per_univ_elem_irrel.
@@ -555,7 +575,12 @@

Mcltt.Core.Semantic.PER.Lemmas

      destruct_rel_mod_eval.
      functional_eval_rewrite_clear.
      handle_per_univ_elem_irrel...
-  - (* fun case *)
+  -
+ +
+fun case +
+
    intros.
    assert (in_rel c c) by intuition.
    destruct_rel_mod_eval.
@@ -563,7 +588,12 @@

Mcltt.Core.Semantic.PER.Lemmas

    handle_per_univ_elem_irrel.
    econstructor; eauto.
    intuition.
-  - (* neut case *)
+  -
+ +
+neut case +
+
    idtac...
Qed.
@@ -627,7 +657,12 @@

Mcltt.Core.Semantic.PER.Lemmas

Qed.

-(* This lemma gets rid of the unnecessary PER premise. *)
+
+ +
+This lemma gets rid of the unnecessary PER premise. +
+
Lemma per_univ_elem_pi' :
  forall i a a' ρ B ρ' B'
    (in_rel : relation domain)
@@ -1030,7 +1065,12 @@

Mcltt.Core.Semantic.PER.Lemmas

        end
    | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
        H2 : {{ DF ~_ ≈ ~?Γ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
-        (* Order matters less here as H1 and H2 cannot be exchanged *)
+        
+ +
+Order matters less here as H1 and H2 cannot be exchanged +
+
        assert_fails (unify R1 R2);
        match goal with
        | H : R1 <~> R2 |- _ => fail 1
@@ -1077,7 +1117,12 @@

Mcltt.Core.Semantic.PER.Lemmas

      destruct_rel_typ.
      handle_per_univ_elem_irrel.
      econstructor; intuition.
-      (* This one cannot be replaced with `etransitivity` as we need different `i`s. *)
+
+ +
+This one cannot be replaced with `etransitivity` as we need different `i`s. +
+
      eapply per_univ_trans; [| eassumption]; eassumption.
  - destruct_conjs.
    assert (tail_rel d{{{ ρ1 ↯ }}} d{{{ ρ3 ↯ }}}) by eauto.
@@ -1128,7 +1173,12 @@

Mcltt.Core.Semantic.PER.Lemmas

Qed.

-(* This lemma removes the PER argument *)
+
+ +
+This lemma removes the PER argument +
+
Lemma per_ctx_env_cons' : forall {Γ Γ' i A A' tail_rel}
                             (head_rel : forall {ρ ρ'} (equiv_ρ_ρ' : {{ Dom ρ ≈ ρ' ∈ tail_rel }}), relation domain)
                             env_rel,
diff --git a/Mcltt.Core.Semantic.Readback.Definitions.html b/Mcltt.Core.Semantic.Readback.Definitions.html index 20bdfae..3be20b5 100644 --- a/Mcltt.Core.Semantic.Readback.Definitions.html +++ b/Mcltt.Core.Semantic.Readback.Definitions.html @@ -54,10 +54,19 @@

Mcltt.Core.Semantic.Readback.Definitions

  `( {{ Rne m in s ↘ M }} ->
     {{ Rnf ⇓ ℕ (⇑ ℕ m) in s ↘ ⇑ M }} )
| read_nf_fn :
-  (* Nf of arg type *)
-  `( {{ Rtyp a in s ↘ A }} ->
-
-     (* Nf of eta-expanded body *)
+  `(
+ +
+Normal form of arg type +
+
+     {{ Rtyp a in s ↘ A }} ->
+     
+ +
+Normal form of eta-expanded body +
+
     {{ $| m & ⇑! a s |↘ m' }} ->
     {{ ⟦ B ⟧ ρ ↦ ⇑! a s ↘ b }} ->
     {{ Rnf ⇓ b m' in S s ↘ M }} ->
@@ -75,20 +84,40 @@

Mcltt.Core.Semantic.Readback.Definitions

     {{ Rnf n in s ↘ N }} ->
     {{ Rne m n in s ↘ M N }} )
| read_ne_natrec :
-  (* Nf of motive *)
-  `( {{ ⟦ B ⟧ ρ ↦ ⇑! ℕ s ↘ b }} ->
+  `(
+ +
+Normal form of motive +
+
+     {{ ⟦ B ⟧ ρ ↦ ⇑! ℕ s ↘ b }} ->
     {{ Rtyp b in S s ↘ B' }} ->

-     (* Nf of mz *)
+     
+ +
+Normal form of mz +
+
     {{ ⟦ B ⟧ ρ ↦ zero ↘ bz }} ->
     {{ Rnf ⇓ bz mz in s ↘ MZ }} ->

-     (* Nf of MS *)
+     
+ +
+Normal form of MS +
+
     {{ ⟦ B ⟧ ρ ↦ succ (⇑! ℕ s) ↘ bs }} ->
     {{ ⟦ MS ⟧ ρ ↦ ⇑! ℕ s ↦ ⇑! b (S s) ↘ ms }} ->
     {{ Rnf ⇓ bs ms in S (S s) ↘ MS' }} ->

-     (* Ne of m *)
+     
+ +
+Neutral form of m +
+
     {{ Rne m in s ↘ M }} ->

     {{ Rne rec m under ρ return B | zero -> mz | succ -> MS end in s ↘ rec M return B' | zero -> MZ | succ -> MS' end }} )
@@ -99,10 +128,20 @@

Mcltt.Core.Semantic.Readback.Definitions

| read_typ_nat :
  `( {{ Rtyp ℕ in s ↘ ℕ }} )
| read_typ_pi :
-  (* Nf of arg type *)
-  `( {{ Rtyp a in s ↘ A }} ->
+  `(
+ +
+Normal form of arg type +
+
+     {{ Rtyp a in s ↘ A }} ->

-     (* Nf of ret type *)
+     
+ +
+Normal form of ret type +
+
     {{ ⟦ B ⟧ ρ ↦ ⇑! a s ↘ b }} ->
     {{ Rtyp b in S s ↘ B' }} ->

diff --git a/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html b/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html index a8d3d58..6b8df42 100644 --- a/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html +++ b/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html @@ -492,7 +492,13 @@

Mcltt.Core.Soundness.LogicalRelation.CoreLemmas

  clear_predicate_equivalence.

-(* Simple Morphism instance for "glu_univ_elem" *)
+
+ +
+

Simple Morphism instance for glu_univ_elem

+ +
+
Add Parametric Morphism i : (glu_univ_elem i)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> iff as simple_glu_univ_elem_morphism_iff.
Proof with mautosolve.
@@ -503,7 +509,13 @@

Mcltt.Core.Soundness.LogicalRelation.CoreLemmas

Qed.

-(* Morphism instances for "neut_glu_*_pred"s *)
+
+ +
+

Morphism instances for neut_glu_*_preds

+ +
+
Add Parametric Morphism i : (neut_glu_typ_pred i)
    with signature per_bot ==> eq ==> eq ==> iff as neut_glu_typ_pred_morphism_iff.
Proof with mautosolve.
@@ -537,7 +549,13 @@

Mcltt.Core.Soundness.LogicalRelation.CoreLemmas

Qed.

-(* Morphism instances for "pi_glu_*_pred"s *)
+
+ +
+

Morphism instances for pi_glu_*_preds

+ +
+
Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> eq ==> iff as pi_glu_typ_pred_morphism_iff.
Proof with mautosolve.
@@ -761,7 +779,13 @@

Mcltt.Core.Soundness.LogicalRelation.CoreLemmas

Qed.

-(* Morphism instances for "glu_univ_elem" *)
+
+ +
+

Morphism instances for glu_univ_elem

+ +
+
Add Parametric Morphism i : (glu_univ_elem i)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> per_univ i ==> iff as glu_univ_elem_morphism_iff.
Proof with mautosolve.
@@ -1067,7 +1091,13 @@

Mcltt.Core.Soundness.LogicalRelation.CoreLemmas

Qed.

-(* Simple Morphism instance for "glu_ctx_env" *)
+
+ +
+

Simple Morphism instance for glu_ctx_env

+ +
+
Add Parametric Morphism : glu_ctx_env
    with signature glu_sub_pred_equivalence ==> eq ==> iff as simple_glu_ctx_env_morphism_iff.
Proof.
diff --git a/Mcltt.Core.Soundness.LogicalRelation.Definitions.html b/Mcltt.Core.Soundness.LogicalRelation.Definitions.html index 912e86d..449af69 100644 --- a/Mcltt.Core.Soundness.LogicalRelation.Definitions.html +++ b/Mcltt.Core.Soundness.LogicalRelation.Definitions.html @@ -47,7 +47,12 @@

Mcltt.Core.Soundness.LogicalRelation.Definitions

Notation "'glu_typ_pred_args'" := (Tcons ctx (Tcons typ Tnil)).
Notation "'glu_typ_pred'" := (predicate glu_typ_pred_args).
Notation "'glu_typ_pred_equivalence'" := (@predicate_equivalence glu_typ_pred_args) (only parsing).
-(* This type annotation is to distinguish this notation from others *)
+
+ +
+This type annotation is to distinguish this notation from others +
+
Notation "Γ ⊢ A ® R" := ((R Γ A : (Prop : Type)) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, A custom exp, R constr).

@@ -104,10 +109,9 @@

Mcltt.Core.Soundness.LogicalRelation.Definitions

  `{ {{ Γ ⊢ A ® neut_glu_typ_pred i a }} ->
     {{ Γ ⊢ M : A }} ->
     {{ Dom m ≈ m ∈ per_bot }} ->
-     (forall Δ σ (* A' *) M', {{ Δ ⊢w σ : Γ }} ->
-                    (* {{ Rne a in length Δ ↘ A' }} -> *)
-                    {{ Rne m in length Δ ↘ M' }} ->
-                    {{ Δ ⊢ M[σ] ≈ M' : A[σ] }}) ->
+     (forall Δ σ M', {{ Δ ⊢w σ : Γ }} ->
+                   {{ Rne m in length Δ ↘ M' }} ->
+                   {{ Δ ⊢ M[σ] ≈ M' : A[σ] }}) ->
     {{ Γ ⊢ M : A ® ⇑ b m ∈ neut_glu_exp_pred i a }} }.

@@ -361,17 +365,27 @@

Mcltt.Core.Soundness.LogicalRelation.Definitions

Arguments nil_glu_sub_pred Δ σ ρ/.

-(* The parameters are ordered differently from the Agda version
-   so that we can return "glu_sub_pred". *)
+
+ +
+The parameters are ordered differently from the Agda version + so that we can return glu_sub_pred. +
+
Variant cons_glu_sub_pred i Γ A (TSb : glu_sub_pred) : glu_sub_pred :=
| mk_cons_glu_sub_pred :
  `{ forall P El,
        {{ Δ ⊢s σ : Γ, A }} ->
        {{ ⟦ A ⟧ ρ ↯ ↘ a }} ->
        {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-        (* Here we use A[Wk][σ] instead of A[Wk∘σ]
-           as syntactic judgement derived from that is
-           a more direct consequence of {{ Γ, A ⊢ #0 : A[Wk] }} *)
+        
+ +
+Here we use {{{ A[Wk][σ] }}} instead of {{{ A[Wk∘σ] }}} + as syntactic judgement derived from that is + a more direct consequence of {{ Γ, A ⊢ #0 : A[Wk] }} +
+
        {{ Δ ⊢ #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 549f833..937ff56 100644 --- a/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html +++ b/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html @@ -633,7 +633,8 @@

Mcltt.Core.Soundness.LogicalRelation.Lemmas

-Lemmas for glu_rel_typ_with_sub and glu_rel_exp_with_sub +

Lemmas for glu_rel_typ_with_sub and glu_rel_exp_with_sub

+
@@ -760,7 +761,8 @@

Mcltt.Core.Soundness.LogicalRelation.Lemmas

-Lemmas for glu_ctx_env +

Lemmas for glu_ctx_env

+
@@ -1165,7 +1167,8 @@

Mcltt.Core.Soundness.LogicalRelation.Lemmas

-Tactics for glu_rel_* +

Tactics for glu_rel_*

+
@@ -1212,7 +1215,8 @@

Mcltt.Core.Soundness.LogicalRelation.Lemmas

-Lemmas about glu_rel_exp +

Lemmas about glu_rel_exp

+
@@ -1293,7 +1297,8 @@

Mcltt.Core.Soundness.LogicalRelation.Lemmas

-Lemmas about glu_rel_sub +

Lemmas about glu_rel_sub

+
diff --git a/Mcltt.Core.Soundness.NatCases.html b/Mcltt.Core.Soundness.NatCases.html index c08c9d3..6108a8a 100644 --- a/Mcltt.Core.Soundness.NatCases.html +++ b/Mcltt.Core.Soundness.NatCases.html @@ -490,7 +490,12 @@

Mcltt.Core.Soundness.NatCases

    invert_rel_typ_body.
    match goal with
    | _: {{ ⟦ A ⟧ ρ ↦ ⇑! ℕ s ↘ ~?a }}, _: {{ ⟦ A ⟧ ρ ↦ (succ ⇑! ℕ s) ↘ ~?a' }} |- _ =>
-        rename a into as'; (* We cannot use as as a name *)
+        rename a into as';
+ +
+We cannot use as as a name +
+
        rename a' into asucc
    end.
    assert {{ Dom ρ ↦ ⇑! ℕ s ↦ ⇑! as' (S s) ≈ ρ ↦ ⇑! ℕ s ↦ ⇑! as' (S s) ∈ env_relΓℕA }} as HΓℕA
@@ -661,11 +666,26 @@

Mcltt.Core.Soundness.NatCases

    mauto.
  }
  induction 1; intros; rename Γ0 into Δ.
-  - (* glu_nat_zero *)
+  -
+ +
+glu_nat_zero +
+
    mauto 4 using glu_rel_exp_natrec_zero_helper.
-  - (* glu_nat_succ *)
+  -
+ +
+glu_nat_succ +
+
    mauto 3 using glu_rel_exp_natrec_succ_helper.
-  - (* glu_nat_neut *)
+  -
+ +
+glu_nat_neut +
+
    mauto 3 using glu_rel_exp_natrec_neut_helper.
Qed.
diff --git a/Mcltt.Core.Soundness.Realizability.html b/Mcltt.Core.Soundness.Realizability.html index e10f006..c5a5ee1 100644 --- a/Mcltt.Core.Soundness.Realizability.html +++ b/Mcltt.Core.Soundness.Realizability.html @@ -144,14 +144,24 @@

Mcltt.Core.Soundness.Realizability

        {{ Γ ⊢ A ® P }} ->
        {{ Γ ⊢ A ® glu_typ_top i a }}) /\
      (forall Γ M A m,
-          (* We repeat this to get the relation between a and P
-             more easily after applying induction 1. *)
+          
+ +
+We repeat this to get the relation between a and P + more easily after applying induction 1. +
+
          {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
          {{ Γ ⊢ M : A ® m ∈ glu_elem_bot i a }} ->
          {{ Γ ⊢ M : A ® ⇑ a m ∈ El }}) /\
      (forall Γ M A m R,
-          (* We repeat this to get the relation between a and P
-             more easily after applying induction 1. *)
+          
+ +
+We repeat this to get the relation between a and P + more easily after applying induction 1. +
+
          {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
          {{ Γ ⊢ M : A ® m ∈ El }} ->
          {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
diff --git a/Mcltt.Core.Soundness.html b/Mcltt.Core.Soundness.html index f3b3bc6..e3fa49d 100644 --- a/Mcltt.Core.Soundness.html +++ b/Mcltt.Core.Soundness.html @@ -50,7 +50,6 @@

Mcltt.Core.Soundness

  destruct_conjs.
  functional_initial_env_rewrite_clear.
  assert {{ Γ ⊢s Id ® p ∈ Sb }} by (eapply initial_env_glu_rel_exp; mauto).
-  (* TODO: extract a tactic from this *)
  destruct_glu_rel_exp_with_sub.
  assert {{ Γ ⊢ M[Id] : A[Id] ® m ∈ glu_elem_top i a }} as [] by (eapply realize_glu_elem_top; mauto).
  match_by_head per_top ltac:(fun H => destruct (H (length Γ)) as [W []]).
diff --git a/Mcltt.Core.Syntactic.CoreInversions.html b/Mcltt.Core.Syntactic.CoreInversions.html index ab5076a..7bde6ab 100644 --- a/Mcltt.Core.Syntactic.CoreInversions.html +++ b/Mcltt.Core.Syntactic.CoreInversions.html @@ -148,7 +148,12 @@

Mcltt.Core.Syntactic.CoreInversions

Hint Resolve wf_exp_sub_inversion : mcltt.

-(* wf_conv and wf_cumu do not give useful inversions *)
+
+ +
+We omit wf_conv and wf_cumu as they do not give useful inversions +
+

Lemma wf_sub_id_inversion : forall Γ Δ,
diff --git a/Mcltt.Core.Syntactic.Corollaries.html b/Mcltt.Core.Syntactic.Corollaries.html index 8b5ad09..9d66046 100644 --- a/Mcltt.Core.Syntactic.Corollaries.html +++ b/Mcltt.Core.Syntactic.Corollaries.html @@ -314,7 +314,12 @@

Mcltt.Core.Syntactic.Corollaries

Hint Resolve exp_eq_natrec_cong_rhs_typ : mcltt.

-(* This works for both natrec_sub and app_sub *)
+
+ +
+This works for both natrec_sub and app_sub cases +
+
Lemma exp_eq_elim_sub_lhs_typ_gen : forall {Γ σ Δ M A B i},
    {{ Γ ⊢s σ : Δ }} ->
    {{ Δ, A ⊢ B : Type@i }} ->
@@ -334,7 +339,12 @@

Mcltt.Core.Syntactic.Corollaries

Hint Resolve exp_eq_elim_sub_lhs_typ_gen : mcltt.

-(* This works for both natrec_sub and app_sub *)
+
+ +
+This works for both natrec_sub and app_sub cases +
+
Lemma exp_eq_elim_sub_rhs_typ : forall {Γ σ Δ M A B i},
    {{ Γ ⊢s σ : Δ }} ->
    {{ Δ, A ⊢ B : Type@i }} ->
@@ -453,7 +463,12 @@

Mcltt.Core.Syntactic.Corollaries

Hint Resolve exp_pi_eta_rhs_body : mcltt.

-(* This works for both var_0 and var_S *)
+
+ +
+This works for both var_0 and var_S cases +
+
Lemma exp_eq_var_sub_rhs_typ_gen : forall {Γ σ Δ i A M},
    {{ Γ ⊢s σ : Δ }} ->
    {{ Δ ⊢ A : Type@i }} ->
diff --git a/Mcltt.Core.Syntactic.CtxSub.html b/Mcltt.Core.Syntactic.CtxSub.html index aaad9ac..935064e 100644 --- a/Mcltt.Core.Syntactic.CtxSub.html +++ b/Mcltt.Core.Syntactic.CtxSub.html @@ -73,19 +73,44 @@

Mcltt.Core.Syntactic.CtxSub

      clear ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyp_helper;
      intros * HΓΔ; destruct (presup_ctx_sub HΓΔ); mauto 4;
      try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
-    (* ctxsub_exp_helper & ctxsub_exp_eq_helper recursion cases *)
+
+ +
+ctxsub_exp_helper & ctxsub_exp_eq_helper recursion cases +
+
    1,6-8: assert {{ ⊢ Δ, ℕ ⊆ Γ, ℕ }} by (econstructor; mautosolve);
    assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
-    (* ctxsub_exp_helper & ctxsub_exp_eq_helper function cases *)
+
+ +
+ctxsub_exp_helper & ctxsub_exp_eq_helper function cases +
+
    1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Δ, B ⊆ Γ, B }} by mauto;
    try econstructor...
-    (* ctxsub_exp_helper & ctxsub_exp_eq_helper variable cases *)
+
+ +
+ctxsub_exp_helper & ctxsub_exp_eq_helper variable cases +
+
    1-2: assert (exists B, {{ #x : B ∈ Δ }} /\ {{ Δ ⊢ B ⊆ A }}); destruct_conjs; mautosolve 4.
-    (* ctxsub_sub_helper & ctxsub_sub_eq_helper weakening cases *)
+
+ +
+ctxsub_sub_helper & ctxsub_sub_eq_helper weakening cases +
+
    2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.

-    - (* ctxsub_exp_eq_helper variable case *)
+    -
+ +
+ctxsub_exp_eq_helper variable case +
+
      inversion_clear HΓΔ as [|Δ0 ? ? C'].
      assert (exists D, {{ #x : D ∈ Δ0 }} /\ {{ Δ0 ⊢ D ⊆ B }}) as [D [i0 ?]] by mauto.
      destruct_conjs.
diff --git a/Mcltt.Core.Syntactic.ExpNoConfusion.html b/Mcltt.Core.Syntactic.ExpNoConfusion.html index 15acd2e..976b98c 100644 --- a/Mcltt.Core.Syntactic.ExpNoConfusion.html +++ b/Mcltt.Core.Syntactic.ExpNoConfusion.html @@ -28,7 +28,12 @@

Mcltt.Core.Syntactic.ExpNoConfusion

-(* For some reason, fitting this file in Syntax.v breaks menhir... Who knows? *)
+
+ +
+For some reason, fitting this file in Syntax.v breaks menhir... Who knows? +
+

From Equations Require Import Equations.
diff --git a/Mcltt.Core.Syntactic.Presup.html b/Mcltt.Core.Syntactic.Presup.html index 75f525e..71bde0d 100644 --- a/Mcltt.Core.Syntactic.Presup.html +++ b/Mcltt.Core.Syntactic.Presup.html @@ -96,13 +96,23 @@

Mcltt.Core.Syntactic.Presup

    try (rename M0 into N); try (rename MZ into NZ); try (rename MS into NS);
    try (rename M'0 into N'); try (rename MZ' into NZ'); try (rename MS' into NS');
    try (rename M' into N').
-  (* presup_exp cases *)
+
+ +
+presup_exp cases +
+
  - eexists.
    assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
    assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...

-  (* presup_exp_eq cases *)
+
+ +
+presup_exp_eq cases +
+
  - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto 4.
    assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
    assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto 4.
@@ -308,7 +318,12 @@

Mcltt.Core.Syntactic.Presup

  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...

-  (* presup_sub_eq cases *)
+
+ +
+presup_sub_eq cases +
+
  - econstructor...

@@ -339,7 +354,12 @@

Mcltt.Core.Syntactic.Presup

    eapply wf_conv...

-    (* presup_subtyp cases *)
+
+ +
+presup_subtyp cases +
+
  - exists (max i i0); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
  - exists (max (S i) (S j)); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
  - mauto.
diff --git a/Mcltt.Core.Syntactic.Syntax.html b/Mcltt.Core.Syntactic.Syntax.html index 9ec0223..bc28a03 100644 --- a/Mcltt.Core.Syntactic.Syntax.html +++ b/Mcltt.Core.Syntactic.Syntax.html @@ -34,7 +34,13 @@

Mcltt.Core.Syntactic.Syntax

From Mcltt Require Import Base.

-(* CST term *)
+
+ +
+

Concrete Syntax Tree

+ +
+
Module Cst.
Inductive obj : Set :=
| typ : nat -> obj
@@ -42,28 +48,60 @@

Mcltt.Core.Syntactic.Syntax

| zero : obj
| succ : obj -> obj
| natrec : obj -> string -> obj -> obj -> string -> string -> obj -> obj
-| app : obj -> obj -> obj
-| fn : string -> obj -> obj -> obj
| pi : string -> obj -> obj -> obj
+| fn : string -> obj -> obj -> obj
+| app : obj -> obj -> obj
| var : string -> obj.
End Cst.

-(* AST term *)
+
+ +
+

Abstract Syntac Tree

+ +
+
Inductive exp : Set :=
-(* Natural numbers *)
+
+ +
+Universe +
+
+| a_typ : nat -> exp
+
+ +
+Natural numbers +
+
+| a_nat : exp
| a_zero : exp
| a_succ : exp -> exp
| a_natrec : exp -> exp -> exp -> exp -> exp
-(* Type constructors *)
-| a_nat : exp
-| a_typ : nat -> exp
-| a_var : nat -> exp
-(* Functions *)
+
+ +
+Functions +
+
+| a_pi : exp -> exp -> exp
| a_fn : exp -> exp -> exp
| a_app : exp -> exp -> exp
-| a_pi : exp -> exp -> exp
-(* Substitutions *)
+
+ +
+Variable +
+
+| a_var : nat -> exp
+
+ +
+Substitution Application +
+
| a_sub : exp -> sub -> exp
with sub : Set :=
| a_id : sub
@@ -101,6 +139,13 @@

Mcltt.Core.Syntactic.Syntax

  end.

+
+ +
+

Syntactic Normal/Neutral Form

+ +
+
Inductive nf : Set :=
| nf_typ : nat -> nf
| nf_nat : nf
diff --git a/Mcltt.Core.Syntactic.System.Lemmas.html b/Mcltt.Core.Syntactic.System.Lemmas.html index a2d59b9..83da288 100644 --- a/Mcltt.Core.Syntactic.System.Lemmas.html +++ b/Mcltt.Core.Syntactic.System.Lemmas.html @@ -32,7 +32,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Import Syntax_Notations.

-(* Core Presuppositions *)
+
+ +
+

Core Presuppositions

+ +
+
Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
Proof with now eauto.
  inversion 1...
@@ -145,8 +151,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve presup_exp_eq_ctx : mcltt.

-(* Recover some previous rules without subtyping.
-   Rest are recovered after presupposition lemmas (in SystemOpt). *)
+
+ +
+Recover some rules we had before adding subtyping. + Rest are recovered after presupposition lemmas (in SystemOpt). +
+

Lemma wf_ctx_sub_refl : forall Γ Δ,
@@ -161,7 +172,12 @@

Mcltt.Core.Syntactic.System.Lemmas


Lemma wf_conv : forall Γ M A i A',
    {{ Γ ⊢ M : A }} ->
-    (* this will be removed in SystemOpt *)
+    
+ +
+The next argument will be removed in SystemOpt +
+
    {{ Γ ⊢ A' : Type@i }} ->
    {{ Γ ⊢ A ≈ A' : Type@i }} ->
    {{ Γ ⊢ M : A' }}.
@@ -194,7 +210,12 @@

Mcltt.Core.Syntactic.System.Lemmas


Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
   {{ Γ ⊢ M ≈ M' : A }} ->
-    (* this will be removed in SystemOpt *)
+   
+ +
+The next argument will be removed in SystemOpt +
+
   {{ Γ ⊢ A' : Type@i }} ->
   {{ Γ ⊢ A ≈ A' : Type@i }} ->
   {{ Γ ⊢ M ≈ M' : A' }}.
@@ -294,7 +315,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-(* PER extension *)
+
+ +
+

Additional Lemmas for Syntactic PERs

+ +
+

Lemma exp_eq_refl : forall {Γ M A},
@@ -332,7 +359,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_eq_refl : mcltt.

-(* Lemmas for exp of "Type@i" *)
+
+ +
+

Lemmas for exp of {{{ Type@i }}}

+ +
+

Lemma exp_sub_typ : forall {Δ Γ A σ i},
@@ -585,7 +618,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_sub_sub_compose_cong_typ : mcltt.

-(* Lemmas for exp of "ℕ" *)
+
+ +
+

Lemmas for exp of {{{ ℕ }}}

+ +
+

Lemma exp_sub_nat : forall {Δ Γ M σ},
@@ -812,7 +851,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_sub_sub_compose_cong_nat : mcltt.

-(* Other lemmas *)
+
+ +
+

Other Tedious Lemmas

+ +
+

Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i},
@@ -1191,6 +1236,15 @@

Mcltt.Core.Syntactic.System.Lemmas

#[export]
Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
+
+
+ +
+

Lemmas for wf_subtyp

+ +
+
+
Fact wf_subtyp_refl : forall {Γ A i},
    {{ Γ ⊢ A : Type@i }} ->
diff --git a/Mcltt.Extraction.Evaluation.html b/Mcltt.Extraction.Evaluation.html index 80a7209..b24277e 100644 --- a/Mcltt.Extraction.Evaluation.html +++ b/Mcltt.Extraction.Evaluation.html @@ -164,14 +164,14 @@

Mcltt.Extraction.Evaluation

    let (r, Hr) := eval_natrec_impl A MZ MS m p _ in
    exist _ r _
| {{{ Π A B }}} , p, H =>
-    let (r , Hr) := eval_exp_impl A p _ in
-    exist _ d{{{ Π r p B }}} _
-| {{{ λ A M }}} , p, H => exist _ d{{{ λ p M }}} _
+    let (r , Hr) := eval_exp_impl A p _ in
+    exist _ d{{{ Π r p B }}} _
+| {{{ λ A M }}} , p, H => exist _ d{{{ λ p M }}} _
| {{{ M N }}} , p, H =>
-    let (m , Hm) := eval_exp_impl M p _ in
-    let (n , Hn) := eval_exp_impl N p _ in
-    let (a, Ha) := eval_app_impl m n _ in
-    exist _ a _
+    let (m , Hm) := eval_exp_impl M p _ in
+    let (n , Hn) := eval_exp_impl N p _ in
+    let (a, Ha) := eval_app_impl m n _ in
+    exist _ a _
| {{{ M[σ] }}} , p, H =>
    let (p', Hp') := eval_sub_impl σ p _ in
    let (m, Hm) := eval_exp_impl M p' _ in
@@ -220,7 +220,7 @@

Mcltt.Extraction.Evaluation

-The definitions of eval_*_impl already come with soundness proofs, +The definitions of eval_*_impl already come with soundness proofs, so we only need to prove completeness. However, the completeness is also obvious from the soundness of eval orders and functional nature of eval. diff --git a/Mcltt.Extraction.Readback.html b/Mcltt.Extraction.Readback.html index e295b97..dfabd5d 100644 --- a/Mcltt.Extraction.Readback.html +++ b/Mcltt.Extraction.Readback.html @@ -209,7 +209,7 @@

Mcltt.Extraction.Readback

-The definitions of read_*_impl already come with soundness proofs, +The definitions of read_*_impl already come with soundness proofs, so we only need to prove completeness. However, the completeness is also obvious from the soundness of eval orders and functional nature of readback. diff --git a/Mcltt.Extraction.Subtyping.html b/Mcltt.Extraction.Subtyping.html index 6e55223..7b8041a 100644 --- a/Mcltt.Extraction.Subtyping.html +++ b/Mcltt.Extraction.Subtyping.html @@ -62,8 +62,14 @@

Mcltt.Extraction.Subtyping

    let*b _ := nf_eq_dec A A' while _ in
    let*b _ := subtyping_nf_impl B B' while _ in
    pureb _
-(* Pseudo-monadic syntax for the next catch-all branch
-   generates some unsolved obligations *)
+
+ +
+Pseudo-monadic syntax for the next catch-all branch + generates some unsolved obligations, so we directly match on + nf_eq_dec A B here. +
+
| A, B with nf_eq_dec A B => {
  | left _ => left _
  | right _ => right _
diff --git a/Mcltt.Extraction.TypeCheck.html b/Mcltt.Extraction.TypeCheck.html index 9759e4f..003cc60 100644 --- a/Mcltt.Extraction.TypeCheck.html +++ b/Mcltt.Extraction.TypeCheck.html @@ -236,39 +236,39 @@

Mcltt.Extraction.TypeCheck

        let (A'', _) := nbe_ty_impl G {{{ A'[Id,,M'] }}} _ in
        pureo (exist _ A'' _)
    | {{{ Π B C }}} =>
-        let*o (exist _ UB _) := type_infer G _ B _ while _ in
-        let*o (exist _ i _) := get_level_of_type_nf UB while _ in
-        let*o (exist _ UC _) := type_infer {{{ G, B }}} _ C _ while _ in
-        let*o (exist _ j _) := get_level_of_type_nf UC while _ in
-        pureo (exist _ n{{{ Type@(max i j) }}} _)
+        let*o (exist _ UB _) := type_infer G _ B _ while _ in
+        let*o (exist _ i _) := get_level_of_type_nf UB while _ in
+        let*o (exist _ UC _) := type_infer {{{ G, B }}} _ C _ while _ in
+        let*o (exist _ j _) := get_level_of_type_nf UC while _ in
+        pureo (exist _ n{{{ Type@(max i j) }}} _)
    | {{{ λ A' M' }}} =>
-        let*o (exist _ UA' _) := type_infer G _ A' _ while _ in
-        let*o (exist _ i _) := get_level_of_type_nf UA' while _ in
-        let*o (exist _ B' _) := type_infer {{{ G, A' }}} _ M' _ while _ in
-        let (A'', _) := nbe_ty_impl G A' _ in
-        pureo (exist _ n{{{ Π A'' B' }}} _)
+        let*o (exist _ UA' _) := type_infer G _ A' _ while _ in
+        let*o (exist _ i _) := get_level_of_type_nf UA' while _ in
+        let*o (exist _ B' _) := type_infer {{{ G, A' }}} _ M' _ while _ in
+        let (A'', _) := nbe_ty_impl G A' _ in
+        pureo (exist _ n{{{ Π A'' B' }}} _)
    | {{{ M' N' }}} =>
-        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
-        pureo (exist _ B' _)
+        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
+        pureo (exist _ B' _)
    | {{{ #x }}} =>
-        let*o (exist _ A _) := lookup G _ x while _ in
-        let (A', _) := nbe_ty_impl G A _ in
-        pureo (exist _ A' _)
+        let*o (exist _ A _) := lookup G _ x while _ in
+        let (A', _) := nbe_ty_impl G A _ in
+        pureo (exist _ A' _)
    | _ => inright _
    }
  .

-  Next Obligation (* {{ G ⊢a succ M' ⟹ ℕ }} /\ (exists i, {{ G ⊢a ℕ ⟹ Type@i }}) *).
+  Next Obligation. (* {{ G ⊢a succ M' ⟹ ℕ }} /\ (exists i, {{ G ⊢a ℕ ⟹ Type@i }}) *)
    clear_defs.
    mautosolve 4.
  Qed.

-  Next Obligation (* exists j, {{ G ⊢ A'Id,,zero : Type@j }} *).
+  Next Obligation. (* exists j, {{ G ⊢ A'Id,,zero : Type@j }} *)
    clear_defs.
    functional_alg_type_infer_rewrite_clear.
    eexists.
@@ -277,7 +277,7 @@

Mcltt.Extraction.TypeCheck

  Qed.

-  Next Obligation (* exists j, {{ G, ℕ, A' ⊢ A'Wk∘Wk,,succ #1 : Type@i }} *).
+  Next Obligation. (* exists j, {{ G, ℕ, A' ⊢ A'Wk∘Wk,,succ #1 : Type@i }} *)
    clear_defs.
    functional_alg_type_infer_rewrite_clear.
    eexists.
@@ -286,7 +286,7 @@

Mcltt.Extraction.TypeCheck

  Qed.

-  Next Obligation (* nbe_ty_order G {{{ A'Id,,M' }}} *).
+  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]
        by eauto 3 using nbe_ty_order_sound.
@@ -297,7 +297,7 @@

Mcltt.Extraction.TypeCheck

  Qed.

-  Next Obligation (* {{ G ⊢a rec M' return A' | zero -> MZ | succ -> MS end ⟹ A'' }} /\ (exists j, {{ G ⊢a A'' ⟹ Type@j }}) *).
+  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.
@@ -308,49 +308,46 @@

Mcltt.Extraction.TypeCheck

  Qed.

-  Next Obligation (* nbe_ty_order G A *).
+  Next Obligation. (* {{ ⊢ G, B }} *)
    clear_defs.
-    assert (exists i, {{ G ⊢ A : Type@i }}) as [? [? []]%soundness_ty] by mauto 3.
-    mauto 3 using nbe_ty_order_sound.
+    assert {{ G ⊢ B : Type@i }} by mauto 4 using alg_type_infer_sound.
+    mauto 3.
  Qed.

-  Next Obligation. (* {{ G ⊢a x ⟹ A' }} /\ (exists i, {{ G ⊢a A' ⟹ Type@i }}) *)
+  Next Obligation. (* {{ G ⊢a Π B C ⟹ Type@(max i j) }} /\ (exists k, {{ G ⊢a Type@(max i j) ⟹ Type@k }}) *)
    clear_defs.
-    assert (exists i, {{ G ⊢ A : Type@i }}) as [i] by mauto 3.
-    assert {{ G ⊢ A ≈ A' : Type@i }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
-    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 4); firstorder mauto 3.
+    mautosolve 4.
  Qed.

  Next Obligation. (* {{ ⊢ G, A' }} *)
    clear_defs.
-    assert {{ G ⊢ A' : Type@i }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ A' : Type@i }} by mauto 4 using alg_type_infer_sound.
    mauto 3.
  Qed.

  Next Obligation. (* nbe_ty_order G A' *)
    clear_defs.
-    assert {{ G ⊢ A' : Type@i }} as [? []]%soundness_ty by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ A' : Type@i }} as [? []]%soundness_ty by mauto 4 using alg_type_infer_sound.
    mauto 3 using nbe_ty_order_sound.
  Qed.

  Next Obligation. (* {{ G ⊢a λ A' M' ⟹ Π A'' B' }} /\ (exists j, {{ G ⊢a Π A'' B' ⟹ Type@j }}) *)
    clear_defs.
-    assert {{ G ⊢ A' : Type@i }} by mauto 4 using alg_type_infer_sound.
-    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' ⊢ B' : Type@H1 }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G, ~(A'' : exp) ⊢ B' : Type@H1 }} by mauto 4.
+    assert {{ G ⊢ A' : Type@i }} by mauto 4 using alg_type_infer_sound.
+    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' ⊢ B' : Type@H1 }} by mauto 4 using alg_type_infer_sound.
+    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 (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.
@@ -367,10 +364,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 ⊢ 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 ⊢ 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.
    mauto 3 using nbe_ty_order_sound.
  Qed.
@@ -380,25 +377,28 @@

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 ⊢ s[Id,,N'] ≈ B' : Type@j }} by (eapply soundness_ty'; mauto 4 using alg_type_check_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).
+    assert (exists k, {{ G ⊢a B' ⟹ Type@k }} /\ k <= j) as [? []] by (gen_presups; mauto 3).
    firstorder.
  Qed.

-  Next Obligation. (* {{ ⊢ G, B }} *)
+  Next Obligation. (* nbe_ty_order G A *)
    clear_defs.
-    assert {{ G ⊢ B : Type@i }} by mauto 4 using alg_type_infer_sound.
-    mauto 3.
+    assert (exists i, {{ G ⊢ A : Type@i }}) as [? [? []]%soundness_ty] by mauto 3.
+    mauto 3 using nbe_ty_order_sound.
  Qed.

-  Next Obligation. (* {{ G ⊢a Π B C ⟹ Type@(max i j) }} /\ (exists k, {{ G ⊢a Type@(max i j) ⟹ Type@k }}) *)
+  Next Obligation. (* {{ G ⊢a x ⟹ A' }} /\ (exists i, {{ G ⊢a A' ⟹ Type@i }}) *)
    clear_defs.
-    mautosolve 4.
+    assert (exists i, {{ G ⊢ A : Type@i }}) as [i] by mauto 3.
+    assert {{ G ⊢ A ≈ A' : Type@i }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    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 4); firstorder mauto 3.
  Qed.

diff --git a/Mcltt.Frontend.Elaborator.html b/Mcltt.Frontend.Elaborator.html index a24953d..8ecf2c4 100644 --- a/Mcltt.Frontend.Elaborator.html +++ b/Mcltt.Frontend.Elaborator.html @@ -42,13 +42,23 @@

Mcltt.Frontend.Elaborator

Module StrSProp := MSetProperties.Properties StrSet.

-(* One cannot import notation from module type without
-   restricting a module to that exact type.
-   Thus here we repeat the notation from WSetsOn. *)
+
+ +
+One cannot import notation from module type without + restricting a module to that exact type. + Thus, here we repeat the notation from WSetsOn. +
+
Notation "s [<=] t" := (StrSet.Subset s t) (at level 70, no associativity).

-(* De-monadify with pattern matching for now *)
+
+ +
+De-monadify with pattern matching for now +
+
Fixpoint lookup (s : string) (ctx : list string) : option nat :=
  match ctx with
  | nil => None
@@ -56,7 +66,7 @@

Mcltt.Frontend.Elaborator

      if string_dec c s
      then Some 0
      else
-        match lookup s cs with
+        match lookup s cs with
        | Some n => Some (n + 1)%nat
        | None => None
        end
@@ -198,7 +208,12 @@

Mcltt.Frontend.Elaborator

Hint Constructors closed_at: mcltt.

-(*Lemma for the well_scoped proof, lookup succeeds if var is in context*)
+
+ +
+Lemma for the well_scoped proof, lookup succeeds if var is in context +
+
Lemma lookup_known (s : string) (ctx : list string) (H_in : List.In s ctx) : exists n : nat, (lookup s ctx = Some n /\ n < List.length ctx).
Proof.
  induction ctx as [| c ctx' IHctx]; simpl in *.
@@ -212,7 +227,12 @@

Mcltt.Frontend.Elaborator

Qed.

-(*Lemma for the well_scoped proof, lookup result always less than context length*)
+
+ +
+Lemma for the well_scoped proof, lookup result always less than context length +
+
Lemma lookup_bound s : forall ctx m, lookup s ctx = Some m -> m < (List.length ctx).
  induction ctx.
  - intros. discriminate H.
@@ -259,14 +279,25 @@

Mcltt.Frontend.Elaborator

Qed.

-(*Well scopedness lemma: If the set of free variables in a cst are contained in a context
-  then elaboration succeeds with that context, and the result is a closed term*)
+
+ +
+

Well scopedness lemma

+ +
+ + If the set of free variables in a cst are contained in a context + then elaboration succeeds with that context, and the result is a closed term +
+
Lemma well_scoped (cst : Cst.obj) : forall ctx, cst_variables cst [<=] StrSProp.of_list ctx ->
exists a : exp, (elaborate cst ctx = Some a) /\ (closed_at a (List.length ctx)).
Proof.
  induction cst; intros; simpl in *; mauto.
-  - destruct (IHcst _ H) as [ast [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+  - (* succ *)
+    destruct (IHcst _ H) as [ast [-> ?]]; mauto.
+  - (* natrec *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
    assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
    assert (cst_variables cst3 [<=] StrSProp.of_list ctx) by fsetdec.
    assert (cst_variables cst4 [<=] StrSProp.of_list (s1 :: s0 :: ctx)) by (simpl; fsetdec).
@@ -274,16 +305,19 @@

Mcltt.Frontend.Elaborator

      destruct (IHcst2 _ H1) as [ast' [-> ?]];
      destruct (IHcst3 _ H2) as [ast'' [-> ?]];
      destruct (IHcst4 _ H3) as [ast''' [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
-    assert (cst_variables cst2 [<=] StrSProp.of_list ctx) by fsetdec.
+  - (* pi *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+    assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
    destruct (IHcst1 _ H0) as [ast [-> ?]];
      destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+  - (* fn *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
    assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
    destruct (IHcst1 _ H0) as [ast [-> ?]];
      destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
-    assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
+  - (* app *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+    assert (cst_variables cst2 [<=] StrSProp.of_list ctx) by fsetdec.
    destruct (IHcst1 _ H0) as [ast [-> ?]];
      destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
  - apply Subset_to_In in H.
@@ -293,16 +327,6 @@

Mcltt.Frontend.Elaborator

    mauto.
Qed.
-
-(* Check elaborate Cst.nat nil : option exp. *)
-(* Fail Check elaborate (Cst.succ a_nat) : option exp. *)
- -
-(* Compute (elaborate (Cst.fn "s" (Cst.typ 5) (Cst.var "s")) nil). *)
-(* Compute (elaborate (Cst.fn "s" (Cst.typ 0) (Cst.fn "x" Cst.nat (Cst.app (Cst.var "x") (Cst.var "s")))) nil). *)
-(* Compute (elaborate (Cst.fn "s" Cst.nat (Cst.fn "x" Cst.nat (Cst.fn "s" Cst.nat (Cst.var "s")))) nil). *)
-(* Compute (elaborate (Cst.fn "s" (Cst.typ 10) (Cst.fn "x" (Cst.typ 0) (Cst.fn "s" (Cst.typ 5) (Cst.var "q")))) nil). *)
-
Example test_elab : elaborate Cst.nat nil = Some a_nat.
Proof. reflexivity. Qed.
diff --git a/Mcltt.LibTactics.html b/Mcltt.LibTactics.html index 584253e..80fa086 100644 --- a/Mcltt.LibTactics.html +++ b/Mcltt.LibTactics.html @@ -38,7 +38,12 @@

Mcltt.LibTactics

Create HintDb mcltt discriminated.

-(* Transparency setting for generalized rewriting *)
+
+ +
+Transparency setting for generalized rewriting +
+
#[export]
Typeclasses Transparent arrows.
@@ -46,7 +51,8 @@

Mcltt.LibTactics

-Generalization of Variables +

Generalization of Variables

+
@@ -60,7 +66,8 @@

Mcltt.LibTactics

-Marking-based Tactics +

Marking-based Tactics

+
@@ -114,7 +121,8 @@

Mcltt.LibTactics

-Simple helper +

Simple helper

+
@@ -180,12 +188,17 @@

Mcltt.LibTactics


Ltac progressive_invert H :=
-  (* dependent destruction is more general than inversion *)
+  
+ +
+We use dependent destruction as it is more general than inversion +
+
  directed dependent destruction H.

#[local]
-  Ltac progressive_invert_once H n :=
+Ltac progressive_invert_once H n :=
  let T := type of H in
  lazymatch T with
  | __mark__ _ _ => fail
@@ -204,7 +217,7 @@

Mcltt.LibTactics


#[global]
-  Ltac progressive_inversion :=
+Ltac progressive_inversion :=
  clear_dups;
  repeat match goal with
    | H : _ |- _ =>
@@ -227,7 +240,7 @@

Mcltt.LibTactics


#[global]
-  Ltac find_head t :=
+Ltac find_head t :=
  lazymatch t with
  | ?t' _ => find_head t'
  | _ => t
@@ -268,7 +281,8 @@

Mcltt.LibTactics

-McLTT automation +

McLTT automation

+
@@ -320,7 +334,12 @@

Mcltt.LibTactics

Tactic Notation "mautosolve" int_or_var(pow) := mautosolve_impl pow.

-(* Improve type class resolution *)
+
+ +
+Improve type class resolution for Equivalence and PER +
+

#[export]
@@ -337,7 +356,12 @@

Mcltt.LibTactics

Hint Extern 1 (@Transitive _ (@predicate_implication _)) => simple apply @PreOrder_Transitive : typeclass_instances.

-(* intuition tactic default setting *)
+
+ +
+Default setting for intuition tactic +
+
Ltac Tauto.intuition_solver ::= auto with mcltt core solve_subterm.

@@ -357,7 +381,12 @@

Mcltt.LibTactics

  end.

-(* this tactic traverses to the bottom of a lemma following universals and conjunctions to the bottom and apply a tactic *)
+
+ +
+this tactic traverses to the bottom of a lemma following universals and conjunctions to the bottom and apply a tactic +
+
Ltac deepexec lem tac :=
  let T := type of lem in
  let T' := eval simpl in T in
@@ -378,7 +407,12 @@

Mcltt.LibTactics

  end.

-(* this tactic is similar to above, but the traversal cuts off when it sees an assumption applicable to a cut-off argument C *)
+
+ +
+this tactic is similar to above, but the traversal cuts off when it sees an assumption applicable to a cut-off argument C +
+
Ltac cutexec lem C tac :=
  let CT := type of C in
  let T := type of lem in
@@ -415,7 +449,7 @@

Mcltt.LibTactics


#[global]
-  Ltac strong_apply H X :=
+Ltac strong_apply H X :=
  let H' := fresh "H" in
  let T := type of X in
  let R := unify_args H T in
@@ -423,7 +457,7 @@

Mcltt.LibTactics


#[global]
-  Ltac apply_equiv_left1 :=
+Ltac apply_equiv_left1 :=
  let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in
  let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in
  match goal with
@@ -435,11 +469,11 @@

Mcltt.LibTactics


#[global]
-  Ltac apply_equiv_left := repeat apply_equiv_left1.
+Ltac apply_equiv_left := repeat apply_equiv_left1.

#[global]
-  Ltac apply_equiv_right1 :=
+Ltac apply_equiv_right1 :=
  let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in
  let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in
  match goal with
@@ -451,11 +485,11 @@

Mcltt.LibTactics


#[global]
-  Ltac apply_equiv_right := repeat apply_equiv_right1.
+Ltac apply_equiv_right := repeat apply_equiv_right1.

#[global]
-  Ltac clear_PER :=
+Ltac clear_PER :=
  repeat match goal with
    | H : PER _ |- _ => clear H
    | H : Symmetric _ |- _ => clear H
@@ -480,7 +514,7 @@

Mcltt.LibTactics


#[global]
-  Ltac saturate_refl :=
+Ltac saturate_refl :=
  repeat match goal with
    | H : ?R ?a ?b |- _ =>
        tryif unify a b
@@ -493,7 +527,7 @@

Mcltt.LibTactics


#[global]
-  Ltac saturate_refl_for hd :=
+Ltac saturate_refl_for hd :=
  repeat match goal with
    | H : ?R ?a ?b |- _ =>
        unify_by_head_of R hd;
@@ -507,11 +541,24 @@

Mcltt.LibTactics


#[global]
-  Ltac solve_refl :=
+Ltac solve_refl :=
+  
+ +
+Sometimes `reflexivity` does not work as (simple) unification fails for some unknown reason. + Thus, we try Equivalence_Reflexive as well. +
+
  solve [reflexivity || apply Equivalence_Reflexive].

-(* Helper Instances for Generalized Rewriting *)
+
+ +
+

Helper Instances for Generalized Rewriting

+ +
+
#[export]
Hint Extern 1 (subrelation (@predicate_equivalence ?Ts) _) => (let H := fresh "H" in intros ? ? H; exact H) : typeclass_instances.
@@ -563,7 +610,12 @@

Mcltt.LibTactics

Qed.

-(* The following facility converts search of Proper from type class instances to the local context *)
+
+ +
+The following facility converts search of Proper from type class instances to the local context +
+

Class PERElem (A : Type) (P : A -> Prop) (R : A -> A -> Prop) :=
@@ -571,7 +623,7 @@

Mcltt.LibTactics


#[export]
-  Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) :
+Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) :
  Proper R a.
Proof.
  cbv. pose proof per_elem; auto.
diff --git a/indexpage.html b/indexpage.html index 3958547..22a851e 100644 --- a/indexpage.html +++ b/indexpage.html @@ -744,15 +744,15 @@

Global Index

a_weaken [constructor, in Mcltt.Core.Syntactic.Syntax]
a_id [constructor, in Mcltt.Core.Syntactic.Syntax]
a_sub [constructor, in Mcltt.Core.Syntactic.Syntax]
-a_pi [constructor, in Mcltt.Core.Syntactic.Syntax]
+a_var [constructor, in Mcltt.Core.Syntactic.Syntax]
a_app [constructor, in Mcltt.Core.Syntactic.Syntax]
a_fn [constructor, in Mcltt.Core.Syntactic.Syntax]
-a_var [constructor, in Mcltt.Core.Syntactic.Syntax]
-a_typ [constructor, in Mcltt.Core.Syntactic.Syntax]
-a_nat [constructor, in Mcltt.Core.Syntactic.Syntax]
+a_pi [constructor, in Mcltt.Core.Syntactic.Syntax]
a_natrec [constructor, in Mcltt.Core.Syntactic.Syntax]
a_succ [constructor, in Mcltt.Core.Syntactic.Syntax]
a_zero [constructor, in Mcltt.Core.Syntactic.Syntax]
+a_nat [constructor, in Mcltt.Core.Syntactic.Syntax]
+a_typ [constructor, in Mcltt.Core.Syntactic.Syntax]


B

BAR [constructor, in Mcltt.Frontend.Parser]
Base [library]
@@ -3182,15 +3182,15 @@

Constructor Index

a_weaken [in Mcltt.Core.Syntactic.Syntax]
a_id [in Mcltt.Core.Syntactic.Syntax]
a_sub [in Mcltt.Core.Syntactic.Syntax]
-a_pi [in Mcltt.Core.Syntactic.Syntax]
+a_var [in Mcltt.Core.Syntactic.Syntax]
a_app [in Mcltt.Core.Syntactic.Syntax]
a_fn [in Mcltt.Core.Syntactic.Syntax]
-a_var [in Mcltt.Core.Syntactic.Syntax]
-a_typ [in Mcltt.Core.Syntactic.Syntax]
-a_nat [in Mcltt.Core.Syntactic.Syntax]
+a_pi [in Mcltt.Core.Syntactic.Syntax]
a_natrec [in Mcltt.Core.Syntactic.Syntax]
a_succ [in Mcltt.Core.Syntactic.Syntax]
a_zero [in Mcltt.Core.Syntactic.Syntax]
+a_nat [in Mcltt.Core.Syntactic.Syntax]
+a_typ [in Mcltt.Core.Syntactic.Syntax]


B

BAR [in Mcltt.Frontend.Parser]


C

diff --git a/toc.html b/toc.html index 144bd8e..01dfcf0 100644 --- a/toc.html +++ b/toc.html @@ -58,6 +58,27 @@

Mcltt.Core.Semantic.NbE

Mcltt.Core.Semantic.PER

Mcltt.Core.Semantic.PER.CoreTactics

Mcltt.Core.Semantic.PER.Definitions

+

Mcltt.Core.Semantic.PER.Lemmas

Mcltt.Core.Semantic.Readback

Mcltt.Core.Semantic.Readback.Definitions

@@ -70,9 +91,51 @@

Mcltt.Core.Soundness.

Mcltt.Core.Soundness.LogicalRelation

Mcltt.Core.Soundness.LogicalRelation.Core

Mcltt.Core.Soundness.LogicalRelation.CoreLemmas

+

Mcltt.Core.Soundness.LogicalRelation.CoreTactics

Mcltt.Core.Soundness.LogicalRelation.Definitions

Mcltt.Core.Soundness.LogicalRelation.Lemmas

+

Mcltt.Core.Soundness.NatCases

Mcltt.Core.Soundness.Realizability

Mcltt.Core.Soundness.SubstitutionCases

@@ -90,9 +153,45 @@

Mcltt.Core.Syntactic.CtxSubMcltt.Core.Syntactic.ExpNoConfusion

Mcltt.Core.Syntactic.Presup

Mcltt.Core.Syntactic.Syntax

+

Mcltt.Core.Syntactic.System

Mcltt.Core.Syntactic.System.Definitions

Mcltt.Core.Syntactic.System.Lemmas

+

Mcltt.Core.Syntactic.System.Tactics

Mcltt.Core.Syntactic.SystemOpt

Mcltt.Entrypoint

@@ -103,8 +202,38 @@

Mcltt.Extraction.Readback

Mcltt.Extraction.Subtyping

Mcltt.Extraction.TypeCheck

Mcltt.Frontend.Elaborator

+

Mcltt.Frontend.Parser

Mcltt.LibTactics

+