From 9a3980ad77c951d96c06558e6751fa78cf1f3dbf Mon Sep 17 00:00:00 2001 From: Meven Date: Mon, 25 Apr 2022 10:56:39 +0200 Subject: [PATCH] writing cleanups --- pcuic/theories/Bidirectional/BDFromPCUIC.v | 4 ++-- pcuic/theories/Bidirectional/BDToPCUIC.v | 7 ++++--- pcuic/theories/Bidirectional/BDTyping.v | 5 ++--- pcuic/theories/README.md | 4 ++-- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/pcuic/theories/Bidirectional/BDFromPCUIC.v b/pcuic/theories/Bidirectional/BDFromPCUIC.v index e67d65852..fa29bd414 100644 --- a/pcuic/theories/Bidirectional/BDFromPCUIC.v +++ b/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) -> diff --git a/pcuic/theories/Bidirectional/BDToPCUIC.v b/pcuic/theories/Bidirectional/BDToPCUIC.v index fa1fbd5ed..7d5ce6d56 100644 --- a/pcuic/theories/Bidirectional/BDToPCUIC.v +++ b/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 diff --git a/pcuic/theories/Bidirectional/BDTyping.v b/pcuic/theories/Bidirectional/BDTyping.v index 8c1733e23..0a3441ab8 100644 --- a/pcuic/theories/Bidirectional/BDTyping.v +++ b/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' diff --git a/pcuic/theories/README.md b/pcuic/theories/README.md index 866896c6c..d1e2cee83 100644 --- a/pcuic/theories/README.md +++ b/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