Reflect comments

theories/Core/Semantic/Domain.v

@@ -12,7 +12,7 @@ Inductive domain : Set :=
 | d_pi : domain -> env -> exp -> domain
 | d_fn : env -> exp -> domain
 | d_eq : domain -> domain -> domain -> domain
-| d_refl : domain -> domain -> domain
+| d_refl : domain -> domain
 | d_neut : domain -> domain_ne -> domain
 with domain_ne : Set :=
 (** Notice that the number x here is not a de Bruijn index but an absolute
@@ -64,7 +64,7 @@ Module Domain_Notations.
   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.
   Notation "'Eq' a m n" := (d_eq a m n) (in custom domain at level 1, a custom domain at level 30, m custom domain at level 35, n custom domain at level 40) : mcltt_scope.
-  Notation "'refl' a m" := (d_refl a m) (in custom domain at level 1, a custom domain at level 30, m custom domain at level 40) : mcltt_scope.
+  Notation "'refl' m" := (d_refl m) (in custom domain at level 1, m custom domain at level 40) : mcltt_scope.
   Notation "'eqrec' n 'under' ρ 'as' 'Eq' a m1 m2 'return' B | 'refl' -> BR 'end'" := (d_eqrec ρ a B BR m1 m2 n) (in custom domain at level 0, a custom domain at level 30, B custom domain at level 60, BR custom domain at level 60, m1 custom domain at level 35, m2 custom domain at level 40, n custom domain at level 60) : mcltt_scope.
   Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : mcltt_scope.
   Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mcltt_scope.

theories/Core/Semantic/Evaluation/Definitions.v

@@ -42,9 +42,8 @@ Inductive eval_exp : exp -> env -> domain -> Prop :=
      {{ ⟦ M2 ⟧ ρ ↘ m2 }} ->
      {{ ⟦ Eq A M1 M2 ⟧ ρ ↘ Eq a m1 m2 }} )
 | eval_exp_refl :
-  `( {{ ⟦ A ⟧ ρ ↘ a }} ->
-     {{ ⟦ M ⟧ ρ ↘ m }} ->
-     {{ ⟦ refl A M ⟧ ρ ↘ refl a m }} )
+  `( {{ ⟦ M ⟧ ρ ↘ m }} ->
+     {{ ⟦ refl A M ⟧ ρ ↘ refl m }} )
 | eval_exp_eqrec :
   `( {{ ⟦ A ⟧ ρ ↘ a }} ->
      {{ ⟦ M1 ⟧ ρ ↘ m1 }} ->
@@ -81,7 +80,7 @@ where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
 with eval_eqrec : domain -> exp -> exp -> domain -> domain -> domain -> env -> domain -> Prop :=
 | eval_eqrec_refl :
   `( {{ ⟦ BR ⟧ ρ ↦ n ↘ br }} ->
-     {{ eqrec refl a' n as Eq a m1 m2 ⟦return B | refl -> BR end⟧ ρ ↘ br }} )
+     {{ eqrec refl n as Eq a m1 m2 ⟦return B | refl -> BR end⟧ ρ ↘ br }} )
 | eval_eqrec_neut :
   `( {{ ⟦ B ⟧ ρ ↦ m1 ↦ m2 ↦ ⇑ (Eq a m1 m2) n ↘ b }} ->
      {{ eqrec ⇑ c n as Eq a m1 m2 ⟦return B | refl -> BR end⟧ ρ ↘ ⇑ b (eqrec n under ρ as Eq a m1 m2 return B | refl -> BR end) }} )

theories/Core/Semantic/PER/Definitions.v

@@ -74,7 +74,7 @@ Hint Constructors per_nat : mcltt.
 Variant per_eq (point_rel : relation domain) : relation domain :=
 | per_eq_refl :
   `{ {{ Dom n ≈ n' ∈ point_rel }} ->
-     {{ Dom refl b n ≈ refl b' n' ∈ per_eq point_rel }} }
+     {{ Dom refl n ≈ refl n' ∈ per_eq point_rel }} }
 | per_eq_neut :
   `{ {{ Dom m ≈ m' ∈ per_bot }} ->
      {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ per_eq point_rel }} }
@@ -289,13 +289,11 @@ Inductive per_subtyp : nat -> domain -> domain -> Prop :=
             {{ Sub b <: b' at i }}) ->
         {{ DF Π a ρ B ≈ Π a ρ B ∈ per_univ_elem i ↘ elem_rel }} ->
         {{ DF Π a' ρ' B' ≈ Π a' ρ' B' ∈ per_univ_elem i ↘ elem_rel' }} ->
-        {{ Sub Π a ρ B <: Π a' ρ' B' at i }})
+        {{ Sub Π a ρ B <: Π a' ρ' B' at i }} )
 | per_subtyp_eq :
-  `( forall (point_rel : relation domain),
-        {{ DF a ≈ a' ∈ per_univ_elem i ↘ point_rel }} ->
-        {{ Dom m1 ≈ m1' ∈ point_rel }} ->
-        {{ Dom m2 ≈ m2' ∈ point_rel }} ->
-        {{ Sub Eq a m1 m2 <: Eq a' m1' m2' at i }})
+  `( forall elem_rel,
+        {{ DF Eq a m1 m2 ≈ Eq a' m1' m2' ∈ per_univ_elem i ↘ elem_rel }} ->
+        {{ Sub Eq a m1 m2 <: Eq a' m1' m2' at i }} )
 | per_subtyp_neut :
   `( {{ Dom b ≈ b' ∈ per_bot }} ->
      {{ Sub ⇑ a b <: ⇑ a' b' at i }} )

theories/Core/Semantic/PER/Lemmas.v

@@ -711,13 +711,12 @@ Lemma per_subtyp_to_univ_elem : forall a b i,
         {{ DF b ≈ b ∈ per_univ_elem i ↘ R' }}.
 Proof.
   destruct 1; do 2 eexists; mauto;
-    split; per_univ_elem_econstructor; mauto 3;
-    match goal with
-    | |- _ <~> _ => apply Equivalence_Reflexive
-    | |- _ ?a ?a => etransitivity; try eassumption; symmetry; eassumption
-    | |- PER _ => eapply per_elem_PER; eassumption
-    | _ => lia
-    end.
+    split;
+    try (etransitivity; try eassumption; symmetry; eassumption);
+    per_univ_elem_econstructor; mauto 3;
+    try apply Equivalence_Reflexive.
+
+  lia.
 Qed.
 
 Lemma per_elem_subtyping : forall A B i,
@@ -764,9 +763,12 @@ Proof.
   simpl; induction 1 using per_univ_elem_ind;
     subst;
     mauto;
-    destruct_all.
-  assert ({{ DF Π a ρ B ≈ Π a' ρ' B' ∈ per_univ_elem i ↘ elem_rel }})
-    by (eapply per_univ_elem_pi'; eauto; intros; destruct_rel_mod_eval; mauto).
+    destruct_all;
+    [ assert ({{ DF Π a ρ B ≈ Π a' ρ' B' ∈ per_univ_elem i ↘ elem_rel }})
+      by (per_univ_elem_econstructor; intuition; destruct_rel_mod_eval; mauto)
+    | enough {{ DF Eq a m1 m2 ≈ Eq a' m1' m2' ∈ per_univ_elem i ↘ elem_rel }} by mauto 3;
+      solve [per_univ_elem_econstructor; eauto]
+    ].
   saturate_refl_for per_univ_elem.
   econstructor; eauto.
   intros;
@@ -811,7 +813,7 @@ Proof.
       intuition.
   - dependent destruction Hsub.
     handle_per_univ_elem_irrel.
-    econstructor; [etransitivity; eauto | |]; etransitivity; eauto.
+    econstructor; etransitivity; eauto.
 Qed.
 
 #[export]

theories/Core/Semantic/Readback/Definitions.v

@@ -33,7 +33,7 @@ Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
 | read_nf_refl :
   `( {{ Rtyp a in s ↘ A }} ->
      {{ Rnf ⇓ a m' in s ↘ M' }} ->
-     {{ Rnf ⇓ (Eq a m1 m2) (refl a' m') in s ↘ refl A M' }} )
+     {{ Rnf ⇓ (Eq a m1 m2) (refl m') in s ↘ refl A M' }} )
 | read_nf_eq_neut :
   `( {{ Rne n in s ↘ N }} ->
      {{ Rnf ⇓ (Eq a m1 m2) (⇑ b n) in s ↘ ⇑ N }} )
@@ -77,7 +77,7 @@ with read_ne : nat -> domain_ne -> ne -> Prop :=
      {{ Rtyp b in S (S (S s)) ↘ B' }} ->
 
      (** Normal form of BR *)
-     {{ ⟦ B ⟧ ρ ↦ ⇑! a s ↦ ⇑! a s ↦ refl a (⇑! a s) ↘ bbr }} ->
+     {{ ⟦ B ⟧ ρ ↦ ⇑! a s ↦ ⇑! a s ↦ refl (⇑! a s) ↘ bbr }} ->
      {{ ⟦ BR ⟧ ρ ↦ ⇑! a s ↘ br }} ->
      {{ Rnf ⇓ bbr br in S s ↘ BR' }} ->