Use consistent naming

theories/Algorithmic/Subtyping/Definitions.v

@@ -13,27 +13,26 @@ Definition not_univ_pi (A : nf) : Prop :=
   end.
 
 Inductive alg_subtyping_nf : nf -> nf -> Prop :=
-| asnf_refl : forall M N,
-    not_univ_pi M ->
-    M = N ->
-    {{ ⊢anf M ⊆ N }}
+| asnf_refl : forall A A',
+    not_univ_pi A ->
+    A = A' ->
+    {{ ⊢anf A ⊆ A' }}
 | asnf_univ : forall i j,
     i <= j ->
     {{ ⊢anf Type@i ⊆ Type@j }}
 | asnf_pi : forall A B A' B',
     A = A' ->
     {{ ⊢anf B ⊆ B' }} ->
     {{ ⊢anf Π A B ⊆ Π A' B' }}
-where "⊢anf M ⊆ N" := (alg_subtyping_nf M N) (in custom judg) : type_scope.
-
+where "⊢anf A ⊆ A'" := (alg_subtyping_nf A A') (in custom judg) : type_scope.
 
 Inductive alg_subtyping : ctx -> typ -> typ -> Prop :=
-| alg_subtyp_run : forall Γ M N A B,
-    nbe_ty Γ M A ->
-    nbe_ty Γ N B ->
-    {{ ⊢anf A ⊆ B }} ->
-    {{ Γ ⊢a M ⊆ N }}
-where "Γ ⊢a M ⊆ N" := (alg_subtyping Γ M N) (in custom judg) : type_scope.
+| alg_subtyp_run : forall Γ A B A' B',
+    nbe_ty Γ A A' ->
+    nbe_ty Γ B B' ->
+    {{ ⊢anf A' ⊆ B' }} ->
+    {{ Γ ⊢a A ⊆ B }}
+where "Γ ⊢a A ⊆ B" := (alg_subtyping Γ A B) (in custom judg) : type_scope.
 
 #[export]
-  Hint Constructors alg_subtyping_nf alg_subtyping: mcltt.
+Hint Constructors alg_subtyping_nf alg_subtyping: mcltt.

theories/Algorithmic/Subtyping/Lemmas.v

@@ -8,17 +8,17 @@ Import Syntax_Notations.
 #[local]
 Ltac apply_subtyping :=
   repeat match goal with
-    | H : {{ ~?Γ ⊢ ~?A : ~?M }},
-        H1 : {{ ~?Γ ⊢ ~?M ⊆ ~?N }} |- _ =>
-        assert {{ Γ ⊢ A : N }} by mauto; clear H
+    | H : {{ ~?Γ ⊢ ~?M : ~?A }},
+        H1 : {{ ~?Γ ⊢ ~?A ⊆ ~?B }} |- _ =>
+        assert {{ Γ ⊢ M : B }} by mauto; clear H
     end.
 
-Lemma alg_subtyping_nf_sound : forall M N,
-    {{ ⊢anf M ⊆ N }} ->
+Lemma alg_subtyping_nf_sound : forall A B,
+    {{ ⊢anf A ⊆ B }} ->
     forall Γ i,
-      {{ Γ ⊢ M : Type@i }} ->
-      {{ Γ ⊢ N : Type@i }} ->
-      {{ Γ ⊢ M ⊆ N }}.
+      {{ Γ ⊢ A : Type@i }} ->
+      {{ Γ ⊢ B : Type@i }} ->
+      {{ Γ ⊢ A ⊆ B }}.
 Proof.
   induction 1; intros; subst; simpl in *.
   - eapply wf_subtyp_refl'; mauto.
@@ -27,7 +27,7 @@ Proof.
     destruct_all.
     gen_presups.
     repeat match goal with
-           | H : {{ ~?Γ ⊢ ~?M ⊆ ~?N }}, H1: {{ ⊢ ~?Γ , ~_ }} |- _ =>
+           | H : {{ ~?Γ ⊢ ~?A ⊆ ~?B }}, H1: {{ ⊢ ~?Γ , ~_ }} |- _ =>
                pose proof (wf_subtyp_univ_weaken _ _ _ _ H H1);
                fail_if_dup
            end.
@@ -38,12 +38,12 @@ Proof.
     mauto 3.
 Qed.
 
-Lemma alg_subtyping_nf_trans : forall M1 M0 M2,
-    {{ ⊢anf M0 ⊆ M1 }} ->
-    {{ ⊢anf M1 ⊆ M2 }} ->
-    {{ ⊢anf M0 ⊆ M2 }}.
+Lemma alg_subtyping_nf_trans : forall A0 A1 A2,
+    {{ ⊢anf A0 ⊆ A1 }} ->
+    {{ ⊢anf A1 ⊆ A2 }} ->
+    {{ ⊢anf A0 ⊆ A2 }}.
 Proof.
-  intros * H1; gen M2.
+  intros * H1; gen A2.
   induction H1; subst; intros ? H2;
     dependent destruction H2;
     simpl in *;
@@ -53,20 +53,20 @@ Proof.
   constructor; lia.
 Qed.
 
-Lemma alg_subtyping_nf_refl : forall M,
-    {{ ⊢anf M ⊆ M }}.
+Lemma alg_subtyping_nf_refl : forall A,
+    {{ ⊢anf A ⊆ A }}.
 Proof.
-  intro M; induction M;
+  induction A;
     solve [constructor; simpl; trivial].
 Qed.
 
 #[local]
 Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mcltt.
 
-Lemma alg_subtyping_trans : forall Γ M0 M1 M2,
-    {{ Γ ⊢a M0 ⊆ M1 }} ->
-    {{ Γ ⊢a M1 ⊆ M2 }} ->
-    {{ Γ ⊢a M0 ⊆ M2 }}.
+Lemma alg_subtyping_trans : forall Γ A0 A1 A2,
+    {{ Γ ⊢a A0 ⊆ A1 }} ->
+    {{ Γ ⊢a A1 ⊆ A2 }} ->
+    {{ Γ ⊢a A0 ⊆ A2 }}.
 Proof.
   intros. progressive_inversion.
   functional_nbe_rewrite_clear.
@@ -76,9 +76,9 @@ Qed.
 #[local]
 Hint Resolve alg_subtyping_trans : mcltt.
 
-Lemma alg_subtyping_complete : forall Γ M N,
-    {{ Γ ⊢ M ⊆ N }} ->
-    {{ Γ ⊢a M ⊆ N }}.
+Lemma alg_subtyping_complete : forall Γ A B,
+    {{ Γ ⊢ A ⊆ B }} ->
+    {{ Γ ⊢a A ⊆ B }}.
 Proof.
   induction 1; mauto.
   - apply completeness in H0 as [W [? ?]].
@@ -106,20 +106,20 @@ Proof.
     mauto 2.
 Qed.
 
-Lemma alg_subtyping_sound : forall Γ M N i,
-    {{ Γ ⊢a M ⊆ N }} ->
-    {{ Γ ⊢ M : Type@i }} ->
-    {{ Γ ⊢ N : Type@i }} ->
-    {{ Γ ⊢ M ⊆ N }}.
+Lemma alg_subtyping_sound : forall Γ A B i,
+    {{ Γ ⊢a A ⊆ B }} ->
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ B : Type@i }} ->
+    {{ Γ ⊢ A ⊆ B }}.
 Proof.
   intros. destruct H.
   on_all_hyp: fun H => apply soundness in H.
   destruct_all.
   on_all_hyp: fun H => apply nbe_type_to_nbe_ty in H.
   functional_nbe_rewrite_clear.
   gen_presups.
-  assert {{ Γ ⊢ A ⊆ B }} by mauto 3 using alg_subtyping_nf_sound.
-  transitivity A; [mauto |].
-  transitivity B; [eassumption |].
+  assert {{ Γ ⊢ A' ⊆ B' }} by mauto 3 using alg_subtyping_nf_sound.
+  transitivity A'; [mauto |].
+  transitivity B'; [eassumption |].
   mauto.
 Qed.

theories/Algorithmic/Typing/Lemmas.v

@@ -125,7 +125,7 @@ Proof with (f_equiv; mautosolve 4).
     simplify_evals.
     dir_inversion_by_head read_typ; subst.
     functional_initial_env_rewrite_clear.
-    assert (initial_env {{{ Γ, ~(C : exp) }}} d{{{ p ↦ ⇑! 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.
@@ -148,9 +148,9 @@ Lemma alg_type_check_typ_implies_alg_type_infer_typ : forall {Γ A i},
     exists j, {{ Γ ⊢a A ⟹ Type@j }} /\ j <= i.
 Proof.
   intros * ? Hcheck.
-  inversion Hcheck as [? ? ? ? Hinfer Hsub]; subst.
-  inversion Hsub as [? ? ? ? ? Hnbe1 Hnbe2 Hnfsub]; subst.
-  replace A0 with A1 in * by (symmetry; mauto 3).
+  inversion Hcheck as [? A' ? ? Hinfer Hsub]; subst.
+  inversion Hsub as [? ? ? A'' ? Hnbe1 Hnbe2 Hnfsub]; subst.
+  replace A' with A'' in * by (symmetry; mauto 3).
   inversion Hnbe2; subst.
   dir_inversion_by_head eval_exp; subst.
   dir_inversion_by_head read_typ; subst.
@@ -169,9 +169,9 @@ Lemma alg_type_check_pi_implies_alg_type_infer_pi : forall {Γ M A B i},
 Proof.
   intros * ? ? Hcheck.
   assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [] by mauto 3.
-  inversion Hcheck as [? ? ? ? Hinfer Hsub]; subst.
-  inversion Hsub as [? ? ? ? C Hnbe1 Hnbe2 Hnfsub]; subst.
-  replace A0 with A1 in * by (symmetry; mauto 3).
+  inversion Hcheck as [? A' ? ? Hinfer Hsub]; subst.
+  inversion Hsub as [? ? ? A'' C Hnbe1 Hnbe2 Hnfsub]; subst.
+  replace A' with A'' in * by (symmetry; mauto 3).
   inversion Hnbe2; subst.
   dir_inversion_by_head eval_exp; subst.
   dir_inversion_by_head read_typ; subst.
@@ -181,18 +181,18 @@ Proof.
   dir_inversion_by_head eval_exp; subst.
   dir_inversion_by_head read_typ; subst.
   simpl in *.
-  assert {{ Γ ⊢ M : ~n{{{ Π A2 B0 }}} }} by mauto 3 using alg_type_infer_sound.
-  assert (exists j, {{ Γ ⊢ Π A2 B0 : Type@j }}) as [j] by (gen_presups; eauto 2).
-  assert ({{ Γ ⊢ A2 : Type@j }} /\ {{ Γ, ~(A2 : exp) ⊢ B0 : Type@j }}) as [] by mauto 3.
+  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.
   do 2 eexists.
-  assert (nbe_ty Γ A A2) by mauto 3.
-  assert {{ Γ ⊢ A ≈ A2 : Type@i }} by mauto 3 using soundness_ty'.
+  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{{{ p ↦ ⇑! a (length Γ) }}}) by mauto 3.
+  assert (initial_env {{{ Γ, A }}} d{{{ ρ ↦ ⇑! a (length Γ) }}}) by mauto 3.
   assert (nbe_ty {{{ Γ, A }}} B B') by mauto 3.
-  assert (initial_env {{{ Γ, ~(A2 : exp) }}} d{{{ p ↦ ⇑! a0 (length Γ) }}}) by mauto 3.
-  assert (nbe_ty {{{ Γ, ~(A2 : exp) }}} B0 B0) by mauto 3.
-  assert {{ ⊢ Γ, A ≈ Γ, ~(A2 : 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.
@@ -312,4 +312,3 @@ Qed.
 
 #[export]
 Hint Resolve alg_type_infer_pi_complete : mcltt.
-

theories/Core/Completeness/ContextCases.v

@@ -25,9 +25,9 @@ Proof with intuition.
   handle_per_ctx_env_irrel.
   eexists.
   per_ctx_env_econstructor; eauto.
-  - instantiate (1 := fun p p' (equiv_p_p' : env_relΓ p p') m m' =>
+  - instantiate (1 := fun ρ ρ' (equiv_ρ_ρ' : env_relΓ ρ ρ') m m' =>
                         forall i R,
-                          rel_typ i A p A' p' R ->
+                          rel_typ i A ρ A' ρ' R ->
                           R m m').
     intros.
     (on_all_hyp: destruct_rel_by_assumption env_relΓ).

theories/Core/Completeness/FunctionCases.v

@@ -7,11 +7,11 @@ Import Domain_Notations.
 Lemma rel_exp_of_pi_inversion : forall {Γ M M' A B},
     {{ Γ ⊨ M ≈ M' : Π A B }} ->
     exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
-    forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+    forall ρ ρ' (equiv_ρ_ρ' : {{ Dom ρ ≈ ρ' ∈ env_rel }}),
     exists in_rel out_rel,
-      rel_typ i A p A p' in_rel /\
-        (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_typ i B d{{{ p ↦ c }}} B d{{{ p' ↦ c' }}} (out_rel c c' equiv_c_c')) /\
-        rel_exp M p M' p'
+      rel_typ i A ρ A ρ' in_rel /\
+        (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_typ i B d{{{ ρ ↦ c }}} B d{{{ ρ' ↦ c' }}} (out_rel c c' equiv_c_c')) /\
+        rel_exp M ρ M' ρ'
           (fun f f' : domain => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app f c f' c' (out_rel c c' equiv_c_c')).
 Proof.
   intros * [env_relΓ].
@@ -26,11 +26,11 @@ Qed.
 
 Lemma rel_exp_of_pi : forall {Γ M M' A B},
     (exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i j,
-      forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+      forall ρ ρ' (equiv_ρ_ρ' : {{ Dom ρ ≈ ρ' ∈ env_rel }}),
       exists in_rel out_rel,
-        rel_typ i A p A p' in_rel /\
-          (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_typ j B d{{{ p ↦ c }}} B d{{{ p' ↦ c' }}} (out_rel c c' equiv_c_c')) /\
-          rel_exp M p M' p'
+        rel_typ i A ρ A ρ' in_rel /\
+          (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_typ j B d{{{ ρ ↦ c }}} B d{{{ ρ' ↦ c' }}} (out_rel c c' equiv_c_c')) /\
+          rel_exp M ρ M' ρ'
             (fun f f' : domain => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app f c f' c' (out_rel c c' equiv_c_c'))) ->
     {{ Γ ⊨ M ≈ M' : Π A B }}.
 Proof.
@@ -57,9 +57,9 @@ Ltac eexists_rel_exp_of_pi :=
   eexists.
 
 #[local]
-Ltac extract_output_info_with p c p' c' env_rel :=
+Ltac extract_output_info_with ρ c ρ' c' env_rel :=
   let Hequiv := fresh "equiv" in
-  (assert (Hequiv : {{ Dom p ↦ c ≈ p' ↦ c' ∈ env_rel }}) by (apply_relation_equivalence; mauto 4);
+  (assert (Hequiv : {{ Dom ρ ↦ c ≈ ρ' ↦ c' ∈ env_rel }}) by (apply_relation_equivalence; mauto 4);
    apply_relation_equivalence;
    (on_all_hyp: fun H => destruct (H _ _ Hequiv));
    destruct_conjs;
@@ -130,7 +130,7 @@ Proof with mautosolve.
   eexists_rel_exp_of_typ.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  assert {{ Dom o' ≈ o' ∈ env_relΔ }} by (etransitivity; [symmetry |]; eassumption).
+  assert {{ Dom ρ'σ' ≈ ρ'σ' ∈ env_relΔ }} by (etransitivity; [symmetry |]; eassumption).
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
   destruct_by_head per_univ.
   handle_per_univ_elem_irrel.
@@ -139,7 +139,7 @@ Proof with mautosolve.
   per_univ_elem_econstructor; eauto.
   - eapply rel_exp_pi_core; eauto; try reflexivity.
     intros.
-    extract_output_info_with o c o' c' env_relΔA...
+    extract_output_info_with ρσ c ρ'σ' c' env_relΔA...
   - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
     apply Equivalence_Reflexive.
 Qed.
@@ -166,11 +166,11 @@ Proof with mautosolve.
   repeat split; [econstructor | | econstructor]; mauto.
   - eapply rel_exp_pi_core; eauto; try reflexivity.
     intros.
-    extract_output_info_with p c p' c' env_relΓA.
+    extract_output_info_with ρ c ρ' c' env_relΓA.
     econstructor; eauto.
     eexists...
   - intros.
-    extract_output_info_with p c p' c' env_relΓA.
+    extract_output_info_with ρ c ρ' c' env_relΓA.
     econstructor; mauto.
     intros.
     destruct_by_head rel_typ.
@@ -202,12 +202,12 @@ Proof with mautosolve.
     clear dependent c.
     clear dependent c'.
     intros.
-    extract_output_info_with o c o' c' env_relΔA.
+    extract_output_info_with ρσ c ρ'σ' c' env_relΔA.
     econstructor; eauto.
     eexists.
     eapply per_univ_elem_cumu_max_left...
   - intros ? **.
-    extract_output_info_with o c o' c' env_relΔA.
+    extract_output_info_with ρσ c ρ'σ' c' env_relΔA.
     econstructor; mauto.
     intros.
     destruct_by_head rel_typ.
@@ -228,7 +228,7 @@ Proof with intuition.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
-  assert (equiv_p'_p' : env_relΓ p' p') by (etransitivity; [symmetry |]; eassumption).
+  assert (equiv_p'_p' : env_relΓ ρ' ρ') by (etransitivity; [symmetry |]; eassumption).
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   rename x2 into in_rel.
   destruct_by_head rel_typ.
@@ -290,7 +290,7 @@ Proof with mautosolve.
   destruct_by_head rel_exp.
   rename m into n.
   rename m' into n'.
-  extract_output_info_with p n p' n' env_relΓA.
+  extract_output_info_with ρ n ρ' n' env_relΓA.
   eexists.
   split; econstructor...
 Qed.