From a3c563dcdc8bd32fc7e5d71b241b8c55a41d4378 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 3 Jul 2023 18:30:52 +0200 Subject: [PATCH] Use : Set explicitly instead of relying on inductive minimization As minimization to set is disabled relying on inductive minimization means relying on bugs. --- Instance/Comp.v | 4 ++-- Instance/Lambda/Eval.v | 10 +++++----- Instance/Lambda/Exp.v | 4 ++-- Instance/Lambda/Full.v | 10 +++++----- Instance/Lambda/Ren.v | 2 +- Instance/Lambda/Step.v | 2 +- Instance/Lambda/Sub.v | 2 +- Instance/Lambda/Ty.v | 2 +- Instance/Lambda/Value.v | 2 +- Instance/Parallel.v | 4 ++-- Instance/Roof.v | 4 ++-- Instance/Shapes.v | 2 +- Instance/Two.v | 4 ++-- Instance/Two/Discrete.v | 4 ++-- Lib/MapDecide.v | 6 +++--- Theory/Metacategory/ArrowsOnly.v | 4 ++-- 16 files changed, 33 insertions(+), 33 deletions(-) diff --git a/Instance/Comp.v b/Instance/Comp.v index c45d469f..8364d5db 100644 --- a/Instance/Comp.v +++ b/Instance/Comp.v @@ -250,7 +250,7 @@ Section Examples. and long. *) (* Group operations *) -Inductive Group_operation := +Inductive Group_operation : Set := | one : Group_operation (* unit *) | mul : Group_operation (* multiplication *) | inv : Group_operation. (* inverse *) @@ -283,7 +283,7 @@ Definition inv' {G : OpAlgebra GroupOp} (x : G) := op G inv (fun _ => x). (* There are five group equations. *) -Inductive Group_equation := +Inductive Group_equation : Set := | assoc : Group_equation | unit_left : Group_equation | unit_right : Group_equation diff --git a/Instance/Lambda/Eval.v b/Instance/Lambda/Eval.v index d015bddf..f30bc3e4 100644 --- a/Instance/Lambda/Eval.v +++ b/Instance/Lambda/Eval.v @@ -17,14 +17,14 @@ Section Eval. Import ListNotations. -Inductive Closed : Ty → Type := +Inductive Closed : Ty → Set := | Closure {Γ τ} : Exp Γ τ → ClEnv Γ → Closed τ -with ClEnv : Env → Type := +with ClEnv : Env → Set := | NoCl : ClEnv [] | AddCl {Γ τ} : Value τ → ClEnv Γ → ClEnv (τ :: Γ) -with Value : Ty → Type := +with Value : Ty → Set := | Val {Γ τ} (x : Exp Γ τ) : ValueP x → ClEnv Γ → Value τ. Derive Signature NoConfusion NoConfusionHom Subterm for ClEnv Closed Value. @@ -43,7 +43,7 @@ Fixpoint snoc {a : Type} (x : a) (xs : list a) : list a := | x :: xs => x :: snoc x xs end. -Inductive EvalContext : Ty → Ty → Type := +Inductive EvalContext : Ty → Ty → Set := | MT {τ} : EvalContext τ τ | AR {dom cod τ} : Closed dom → EvalContext cod τ → EvalContext (dom ⟶ cod) τ @@ -56,7 +56,7 @@ Inductive EvalContext : Ty → Ty → Type := Derive Signature NoConfusion NoConfusionHom Subterm for EvalContext. -Inductive Σ : Ty → Type := +Inductive Σ : Ty → Set := | MkΣ {u : Ty} (exp : Closed u) {τ : Ty} diff --git a/Instance/Lambda/Exp.v b/Instance/Lambda/Exp.v index e7ace8e4..1295869c 100644 --- a/Instance/Lambda/Exp.v +++ b/Instance/Lambda/Exp.v @@ -19,13 +19,13 @@ Open Scope Ty_scope. Definition Env := list Ty. -Inductive Var : Env → Ty → Type := +Inductive Var : Env → Ty → Set := | ZV {Γ τ} : Var (τ :: Γ) τ | SV {Γ τ τ'} : Var Γ τ → Var (τ' :: Γ) τ. Derive Signature NoConfusion EqDec for Var. -Inductive Exp Γ : Ty → Type := +Inductive Exp Γ : Ty → Set := | EUnit : Exp Γ TyUnit | Pair {τ1 τ2} : Exp Γ τ1 → Exp Γ τ2 → Exp Γ (TyPair τ1 τ2) diff --git a/Instance/Lambda/Full.v b/Instance/Lambda/Full.v index 0db9263a..19a94ee0 100644 --- a/Instance/Lambda/Full.v +++ b/Instance/Lambda/Full.v @@ -24,7 +24,7 @@ Open Scope Ty_scope. (* A context defines a hole which, after substitution, yields an expression of the index type. *) -Inductive Frame Γ : Ty → Ty → Type := +Inductive Frame Γ : Ty → Ty → Set := | F_PairL {τ1 τ2} : Exp Γ τ2 → Frame τ1 (τ1 × τ2) | F_PairR {τ1 τ2} : Exp Γ τ1 → Frame τ2 (τ1 × τ2) | F_Fst {τ1 τ2} : Frame (τ1 × τ2) τ1 @@ -34,7 +34,7 @@ Inductive Frame Γ : Ty → Ty → Type := Derive Signature NoConfusion Subterm for Frame. -Inductive Ctxt Γ : Ty → Ty → Type := +Inductive Ctxt Γ : Ty → Ty → Set := | C_Nil {τ} : Ctxt τ τ | C_Cons {τ τ' τ''} : Frame Γ τ' τ → Ctxt τ'' τ' → Ctxt τ'' τ. @@ -65,7 +65,7 @@ Theorem Ctxt_comp_assoc {Γ τ τ' τ'' τ'''} Ctxt_comp C (Ctxt_comp C' C'') = Ctxt_comp (Ctxt_comp C C') C''. Proof. induction C; simpl; auto; now f_equal. Qed. -Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Type := +Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Set := | R_Beta {dom cod} (e : Exp (dom :: Γ) cod) v : ValueP v → Redex (APP (LAM e) v) (SubExp {|| v ||} e) @@ -82,7 +82,7 @@ Derive Signature for Redex. Unset Elimination Schemes. -Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Type := +Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Set := | Plug_Hole : Plug (C_Nil _) e | Plug_PairL {τ1 τ2} {C : Ctxt Γ τ' τ1} {e' : Exp Γ τ1} {e2 : Exp Γ τ2} : @@ -147,7 +147,7 @@ Theorem Plug_id_left {Γ τ τ'} {C : Ctxt Γ τ' τ} {x : Exp Γ τ'} {y : Exp Plug_comp Plug_id P ~= P. *) -Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Type := +Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Set := | StepRule {τ'} {C : Ctxt Γ τ' τ} {e1 e2 : Exp Γ τ'} {e1' e2' : Exp Γ τ} : Plug e1 C e1' → Plug e2 C e2' → diff --git a/Instance/Lambda/Ren.v b/Instance/Lambda/Ren.v index a0990a52..ff81fad2 100644 --- a/Instance/Lambda/Ren.v +++ b/Instance/Lambda/Ren.v @@ -15,7 +15,7 @@ Section Ren. Import ListNotations. -Inductive Ren : Env → Env → Type := +Inductive Ren : Env → Env → Set := | NoRen : Ren [] [] | Drop {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) Γ' | Keep {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) (τ :: Γ'). diff --git a/Instance/Lambda/Step.v b/Instance/Lambda/Step.v index be30f8c1..42c4004b 100644 --- a/Instance/Lambda/Step.v +++ b/Instance/Lambda/Step.v @@ -25,7 +25,7 @@ Open Scope Ty_scope. Reserved Notation " t '--->' t' " (at level 40). -Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Type := +Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Set := | ST_Pair1 Γ τ1 τ2 (x x' : Exp Γ τ1) (y : Exp Γ τ2) : x ---> x' → Pair x y ---> Pair x' y diff --git a/Instance/Lambda/Sub.v b/Instance/Lambda/Sub.v index 3682a294..a3be8ad7 100644 --- a/Instance/Lambda/Sub.v +++ b/Instance/Lambda/Sub.v @@ -16,7 +16,7 @@ Section Sub. Import ListNotations. -Inductive Sub (Γ : Env) : Env → Type := +Inductive Sub (Γ : Env) : Env → Set := | NoSub : Sub [] | Push {Γ' τ} : Exp Γ τ → Sub Γ' → Sub (τ :: Γ'). diff --git a/Instance/Lambda/Ty.v b/Instance/Lambda/Ty.v index 22fb14f9..741ca879 100644 --- a/Instance/Lambda/Ty.v +++ b/Instance/Lambda/Ty.v @@ -7,7 +7,7 @@ Set Transparent Obligations. Section Ty. -Inductive Ty : Type := +Inductive Ty : Set := | TyUnit : Ty | TyPair : Ty → Ty → Ty | TyArrow : Ty → Ty → Ty. diff --git a/Instance/Lambda/Value.v b/Instance/Lambda/Value.v index 35d1091f..dde8fca1 100644 --- a/Instance/Lambda/Value.v +++ b/Instance/Lambda/Value.v @@ -16,7 +16,7 @@ Open Scope Ty_scope. (* [ValueP] is an inductive proposition that indicates whether an expression represents a value, i.e., that it does reduce any further. *) -Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Type := +Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Set := | UnitP : ValueP EUnit | PairP {τ1 τ2} {x : Exp Γ τ1} {y : Exp Γ τ2} : ValueP x → ValueP y → ValueP (Pair x y) diff --git a/Instance/Parallel.v b/Instance/Parallel.v index a1df091d..3038744c 100644 --- a/Instance/Parallel.v +++ b/Instance/Parallel.v @@ -12,9 +12,9 @@ Generalizable All Variables. This is used to build diagrams that identify equalizers. *) -Inductive ParObj : Type := ParX | ParY. +Inductive ParObj : Set := ParX | ParY. -Inductive ParHom : bool → ParObj → ParObj → Type := +Inductive ParHom : bool → ParObj → ParObj → Set := | ParIdX : ParHom true ParX ParX | ParIdY : ParHom true ParY ParY | ParOne : ParHom true ParX ParY diff --git a/Instance/Roof.v b/Instance/Roof.v index 3aa1b4b5..a57898eb 100644 --- a/Instance/Roof.v +++ b/Instance/Roof.v @@ -15,9 +15,9 @@ Generalizable All Variables. This is used to build diagrams that identify spans and pullbacks. *) -Inductive RoofObj : Type := RNeg | RZero | RPos. +Inductive RoofObj : Set := RNeg | RZero | RPos. -Inductive RoofHom : RoofObj → RoofObj → Type := +Inductive RoofHom : RoofObj → RoofObj → Set := | IdNeg : RoofHom RNeg RNeg | ZeroNeg : RoofHom RZero RNeg | IdZero : RoofHom RZero RZero diff --git a/Instance/Shapes.v b/Instance/Shapes.v index aec78941..79a43222 100644 --- a/Instance/Shapes.v +++ b/Instance/Shapes.v @@ -78,7 +78,7 @@ Qed. (**************************************************************************) -Inductive Shape := +Inductive Shape : Set := | Bottom | Top | Plus (x y : Shape) diff --git a/Instance/Two.v b/Instance/Two.v index c9bfede5..5169ad44 100644 --- a/Instance/Two.v +++ b/Instance/Two.v @@ -4,9 +4,9 @@ Require Import Category.Theory.Functor. Generalizable All Variables. -Inductive TwoObj : Type := TwoX | TwoY. +Inductive TwoObj : Set := TwoX | TwoY. -Inductive TwoHom : TwoObj → TwoObj → Type := +Inductive TwoHom : TwoObj → TwoObj → Set := | TwoIdX : TwoHom TwoX TwoX | TwoIdY : TwoHom TwoY TwoY | TwoXY : TwoHom TwoX TwoY. diff --git a/Instance/Two/Discrete.v b/Instance/Two/Discrete.v index 8e563757..b941a8a9 100644 --- a/Instance/Two/Discrete.v +++ b/Instance/Two/Discrete.v @@ -4,9 +4,9 @@ Require Import Category.Theory.Functor. Generalizable All Variables. -Inductive TwoDObj : Type := TwoDX | TwoDY. +Inductive TwoDObj : Set := TwoDX | TwoDY. -Inductive TwoDHom : TwoDObj → TwoDObj → Type := +Inductive TwoDHom : TwoDObj → TwoDObj → Set := | TwoDIdX : TwoDHom TwoDX TwoDX | TwoDIdY : TwoDHom TwoDY TwoDY. diff --git a/Lib/MapDecide.v b/Lib/MapDecide.v index 701162ce..eff09be4 100644 --- a/Lib/MapDecide.v +++ b/Lib/MapDecide.v @@ -41,11 +41,11 @@ Notation "x && y" := (if x then Reduce y else No) : partial_scope. * A term language for theorems involving FMaps *) -Record environment := { +Record environment : Set := { vars : positive → N }. -Inductive term := +Inductive term : Set := | Var : positive → term | Value : N → term. @@ -118,7 +118,7 @@ Fixpoint map_expr_denote env (m : map_expr) : M.t N := (term_denote env f) (map_expr_denote env m') end. -Inductive formula := +Inductive formula : Set := | Top : formula | Bottom : formula | Maps : term → term → term → map_expr → formula diff --git a/Theory/Metacategory/ArrowsOnly.v b/Theory/Metacategory/ArrowsOnly.v index 727b2e3d..5abe3c3e 100644 --- a/Theory/Metacategory/ArrowsOnly.v +++ b/Theory/Metacategory/ArrowsOnly.v @@ -48,13 +48,13 @@ Section Category. Context (M : Metacategory). -Record object := { +Record object : Set := { obj_arr : arrow M; obj_def : composite M obj_arr obj_arr obj_arr; obj_id : is_identity M obj_arr }. -Record morphism (dom cod : object) := { +Record morphism (dom cod : object) : Set := { mor_arr : arrow M; mor_dom : composite M mor_arr (obj_arr dom) mor_arr; mor_cod : composite M (obj_arr cod) mor_arr mor_arr