Merge pull request #692 from MetaCoq/writing_cleanups

Writing cleanups

pcuic/theories/Bidirectional/BDFromPCUIC.v

@@ -9,7 +9,7 @@ Require Import Equations.Prop.DepElim.
 
 Implicit Types (cf : checker_flags) (Σ : global_env_ext).
 
-(** Preliminary lemmata missing from MetaCoq *)
+(** Preliminary lemmas missing from MetaCoq *)
 Lemma is_allowed_elimination_monotone `{checker_flags} Σ s1 s2 allowed :
   leq_universe Σ s1 s2 -> is_allowed_elimination Σ allowed s2 -> is_allowed_elimination Σ allowed s1.
 Proof.
@@ -54,7 +54,7 @@ Proof.
     constructor; auto.
 Qed.
 
-(** Lemmata to get checking and constrained inference from inference + cumulativity. Relies on confluence + injectivity of type constructors *)
+(** Lemmas to get checking and constrained inference from inference + cumulativity. Relies on confluence + injectivity of type constructors *)
 
 Lemma conv_check `{checker_flags} Σ (wfΣ : wf Σ) Γ t T :
   (∑ T' : term, Σ ;;; Γ |- t ▹ T' × Σ ;;; Γ ⊢ T' ≤ T) ->

pcuic/theories/Bidirectional/BDToPCUIC.v

@@ -7,7 +7,7 @@ Require Import ssreflect ssrbool.
 From Equations Require Import Equations.
 Require Import Equations.Prop.DepElim.
 
-(** Various generic lemmatas missing from the MetaCoq library *)
+(** Various generic lemmas missing from the MetaCoq library *)
 
 Lemma All2i_prod (A B : Type) (P Q : nat -> A -> B -> Type) (n : nat) (l : list A) (l' : list B) :
   All2i P n l l' -> All2i Q n l l' -> All2i (fun i x y => (P i x y) × (Q i x y)) n l l'.
@@ -107,7 +107,8 @@ Section BDToPCUICTyping.
   Context (Σ : global_env_ext).
   Context (wfΣ : wf Σ).
 
-  (** The predicates we wish to prove, note the extra well-formedness hypothesis depending on the modding of the judgement *)
+  (** The predicates we wish to prove, note the extra well-formedness hypothesis on the context
+  and type whenever they are inputs to the algorithm *)
 
   Let Pinfer Γ t T :=
     wf_local Σ Γ -> Σ ;;; Γ |- t : T.
@@ -130,7 +131,7 @@ Section BDToPCUICTyping.
   Let PΓ_rel Γ Γ' :=
     wf_local Σ Γ -> wf_local_rel Σ Γ Γ'.
 
-  (** Preliminary lemmata to go from a bidirectional judgement to the corresponding undirected one *)
+  (** Preliminary lemmas to go from a bidirectional judgement to the corresponding undirected one *)
 
   Lemma bd_wf_local Γ (all: wf_local_bd Σ Γ) :
     All_local_env_over_sorting checking infering_sort 

pcuic/theories/Bidirectional/BDTyping.v

@@ -76,8 +76,7 @@ Inductive infering `{checker_flags} (Σ : global_env_ext) (Γ : context) : term
   Σ ;;; Γ |- c ▹{ci} (u,args) ->
   declared_inductive Σ.1 ci.(ci_ind) mdecl idecl ->
   Σ ;;; Γ ,,, predctx |- p.(preturn) ▹□ ps ->
-  (* case_side_conditions (fun Σ Γ => wf_local Σ Γ) checking Σ Γ ci p ps
-    mdecl idecl indices predctx -> *) (*issue with wf_local_rel vs wf_local *)
+  (* case_side_conditions *)
   mdecl.(ind_npars) = ci.(ci_npar) ->
   eq_context_upto_names p.(pcontext) (ind_predicate_context ci.(ci_ind) mdecl idecl) ->
   wf_predicate mdecl idecl p ->
@@ -141,7 +140,7 @@ with infering_indu `{checker_flags} (Σ : global_env_ext) (Γ : context) : induc
   Σ ;;; Γ |- t ▹{ind} (u,args) 
 
 with checking `{checker_flags} (Σ : global_env_ext) (Γ : context) : term -> term -> Type :=
-| check_Cons t T T':
+| check_Cumul t T T':
   Σ ;;; Γ |- t ▹ T ->
   Σ ;;; Γ |- T <= T' ->
   Σ ;;; Γ |- t ◃ T'

pcuic/theories/README.md

@@ -30,7 +30,7 @@
 | [PCUICInduction] | Induction principle on syntax
 | [PCUICSize]      | Size of terms
 | [PCUICDepth]     | Depth of terms
-| [PCUICReflect]   | Decidability of ws_cumul_pb between terms
+| [PCUICReflect]   | Decidability of equality between terms
 | [PCUICContextRelations] | Helper lemmas for relations between contexts
 | [PCUICPosition]  | Notions of position and stack, well-order on positions
 
@@ -208,7 +208,7 @@
 | [PCUICContexts]     | Various properties on contexts
 | [PCUICArities]    | Properties on lists of terms
 | [PCUICSpine]      | Properties on spines (lists of terms) relating to typing, substitutions, and so on
-| [PCUICInductives] | Technical typing and conversion lemmass related to inductive definitions
+| [PCUICInductives] | Technical typing and conversion lemmas related to inductive definitions
 | [PCUICValidity] | Every term `A` such that `Γ ⊢ t : A` is a type
 | [PCUICInductiveInversion] | Typing properties and inversions for inductive types, constructors and projections
 | [PCUICAlpha] | Typing does not depend on names