From 052fdbc9ca3289bf3d35b6db553b9432f2907d97 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 16 Jan 2024 13:47:08 -0500 Subject: [PATCH] Spaces.Nat: get rid of lots of universe variables; adjust Classes --- .../implementations/natpair_integers.v | 5 +- .../Classes/implementations/peano_naturals.v | 3 +- theories/Spaces/Nat/Arithmetic.v | 89 ++++++++++--------- theories/Spaces/Nat/Core.v | 64 ++++++------- 4 files changed, 81 insertions(+), 80 deletions(-) diff --git a/theories/Classes/implementations/natpair_integers.v b/theories/Classes/implementations/natpair_integers.v index 955c55a4c2d..1c7efea54da 100644 --- a/theories/Classes/implementations/natpair_integers.v +++ b/theories/Classes/implementations/natpair_integers.v @@ -1049,10 +1049,7 @@ Global Instance Z_abs@{} : IntAbs@{UN UN UN UN UN UN UN UN UN UN UN UN UN UN UN UN UN} Z N - := ltac:(first [exact Z_abs'@{Ularge Ularge Ularge Ularge Ularge - Ularge Ularge}| - exact Z_abs'@{Ularge Ularge Ularge Ularge Ularge - Ularge}]). + := Z_abs'. Notation n_to_z := (naturals_to_semiring N Z). diff --git a/theories/Classes/implementations/peano_naturals.v b/theories/Classes/implementations/peano_naturals.v index 4737e3b7211..563eea22c9d 100644 --- a/theories/Classes/implementations/peano_naturals.v +++ b/theories/Classes/implementations/peano_naturals.v @@ -15,6 +15,7 @@ Local Set Universe Minimization ToSet. Section nat_lift. Universe N. +(* It's important that the universe [N] be free. Occasionally, Coq will choose universe variables in proofs that force [N] to be [Set]. To pinpoint where this happens, you can add the line [Constraint Set < N.] here, and see what fails below. *) Let natpaths := @paths@{N} nat. Infix "=N=" := natpaths. @@ -425,7 +426,7 @@ Qed. Instance decidable_nat_apart x y : Decidable (nat_apart x y). Proof. - rapply decidable_sum; apply Nat.Core.decidable_lt. + rapply decidable_sum@{N N N}; apply Nat.Core.decidable_lt. Defined. Global Instance nat_trivial_apart : TrivialApart nat. diff --git a/theories/Spaces/Nat/Arithmetic.v b/theories/Spaces/Nat/Arithmetic.v index 6c4a124f4c0..8ee89b24a98 100644 --- a/theories/Spaces/Nat/Arithmetic.v +++ b/theories/Spaces/Nat/Arithmetic.v @@ -1,7 +1,9 @@ Require Import Basics. Require Import Spaces.Nat.Core. -Local Close Scope trunc_scope. +Local Set Universe Minimization ToSet. + +Local Close Scope trunc_scope. Local Open Scope nat_scope. Ltac nat_absurd_trivial := @@ -37,7 +39,7 @@ Local Definition transitive_paths_nat (n m k : nat) Proposition assoc_nat_add (n m k : nat) : n + (m + k) = (n + m) + k. Proof. - revert m k; induction n. + revert m k; simple_induction n n IHn. - reflexivity. - intros m k. change (n.+1 + (m + k)) with (n + (m + k)).+1. apply (transitive_paths _ _ _ (nat_add_n_Sm _ _)). @@ -167,7 +169,7 @@ Defined. Proposition sub_n_n (n : nat) : n - n = 0. Proof. - induction n. + simple_induction n n IHn. - reflexivity. - simpl; exact IHn. Defined. @@ -194,10 +196,10 @@ Ltac rewrite_subnn := Proposition add_n_sub_n_eq (m n : nat) : m + n - n = m. Proof. destruct m. - - induction n. + - simple_induction' n. + reflexivity. + assumption. - - induction n. + - simple_induction' n. + simpl. destruct (add_n_O m); reflexivity. + simpl. destruct (add_n_Sm m n). assumption. Defined. @@ -226,17 +228,17 @@ Defined. Proposition n_leq_add_n_k (n m : nat) : n <= n + m. Proof. - induction n. + simple_induction n n IHn. - apply leq_0_n. - simpl; apply leq_S_n', IHn. Defined. Proposition n_leq_add_n_k' (n m : nat) : n <= m + n. Proof. - induction m. + simple_induction' m. - exact(leq_n n). - simpl. apply leq_S. assumption. -Defined. +Defined. Proposition natineq0eq0 {n : nat} : n <= 0 -> n = 0. Proof. @@ -247,9 +249,9 @@ Defined. Proposition subsubadd (n m k : nat) : n - (m + k) = n - m - k. Proof. - revert m k; induction n. + revert m k; simple_induction n n IHn. - reflexivity. - - intro m; induction m; intro k. + - intro m; destruct m; intro k. + change (0 + k) with k; reflexivity. + change (m.+1 + k) with (m + k).+1; apply IHn. Defined. @@ -264,12 +266,12 @@ Defined. Definition nleqSm_dichot {n m : nat} : (n <= m.+1) -> sum (n <= m) (n = m.+1). Proof. - revert m; induction n. + revert m; simple_induction n n IHn. - intro. left. exact (leq_0_n m). - - induction m. + - destruct m. + intro l. apply leq_S_n, natineq0eq0 in l. right; apply ap; exact l. - + intro l. apply leq_S_n, IHn in l; induction l as [a | b]. + + intro l. apply leq_S_n, IHn in l; destruct l as [a | b]. * left. apply leq_S_n'; exact a. * right. apply ap; exact b. Defined. @@ -288,7 +290,7 @@ Defined. Proposition sub_leq_0_converse (n m : nat) : n - m = 0 -> n <= m. Proof. - revert m; induction n. + revert m; simple_induction n n IHn. - auto with nat. - intros m eq. destruct m. + simpl in eq. apply symmetric_paths in eq. @@ -306,9 +308,9 @@ Defined. Proposition lt_sub_gt_0 (n m : nat) : m < n -> 0 < n - m. Proof. - revert m; induction n. + revert m; simple_induction n n IHn. - intros m ineq. contradiction (not_lt_n_0 m). - - induction m. + - destruct m. + simpl. easy. + simpl. intro ineq. apply leq_S_n in ineq. now apply IHn in ineq. @@ -317,10 +319,10 @@ Defined. Proposition natminuspluseq (n m : nat) : n <= m -> (m - n) + n = m. Proof. - revert m; induction n. + revert m; simple_induction n n IHn. - intros. destruct m; [reflexivity |]. simpl. apply (ap S), symmetric_paths, add_n_O. - - intros m l. induction m. + - intros m l. destruct m. + contradiction (not_leq_Sn_0 n). + simpl. apply leq_S_n, IHn in l. destruct (nat_add_n_Sm (m - n) n). @@ -336,7 +338,7 @@ Proof. - apply n_lt_m_n_leq_m in g. now destruct (symmetric_paths _ _ (sub_leq_0 n m _)). Defined. - + Proposition natminuspluseq' (n m : nat) : n <= m -> n + (m - n) = m. Proof. @@ -363,7 +365,7 @@ Proposition nataddpreservesleq { n m k : nat } : n <= m -> n + k <= m + k. Proof. intro l. - induction k. + simple_induction k k IHk. - destruct (add_n_O n), (add_n_O m); exact l. - destruct (nat_add_n_Sm n k), (nat_add_n_Sm m k); apply leq_S_n'; exact IHk. @@ -387,7 +389,7 @@ Proof. unfold "<". change (n + k).+1 with (n.+1 + k). generalize (n.+1). intros n' l. - induction k. + simple_induction k k IHk. - destruct (add_n_O n'), (add_n_O m); exact l. - destruct (nat_add_n_Sm n' k), (nat_add_n_Sm m k); apply leq_S_n'; exact IHk. @@ -404,7 +406,7 @@ Defined. Proposition nataddreflectslt { n m k : nat } : n + k < m + k -> n < m. Proof. - induction k. + simple_induction k k IHk. - destruct (add_n_O n), (add_n_O m); trivial. - intro l. destruct (nat_add_n_Sm n k), (nat_add_n_Sm m k) in l. apply leq_S_n, IHk in l; exact l. @@ -448,9 +450,9 @@ Defined. Proposition nataddsub_assoc_lemma {k m : nat} : (k <= m) -> m.+1 - k = (m - k).+1. Proof. - revert m; induction k. + revert m; simple_induction k k IHk. - intros m l; simpl. destruct m; reflexivity. - - induction m. + - destruct m. + simpl; intro g; contradiction (not_leq_Sn_0 _ g). + intro l; apply leq_S_n in l. change (m.+2 - k.+1) with (m.+1 - k). @@ -461,7 +463,7 @@ Defined. Proposition nataddsub_assoc (n : nat) {m k : nat} : (k <= m) -> n + (m - k) = n + m - k. Proof. - revert m k. induction n. + revert m k. simple_induction n n IHn. - reflexivity. - intros m k l. change (n.+1 + (m - k)) with (n + (m - k)).+1; @@ -492,9 +494,9 @@ Proposition nataddsub_comm_ineq_lemma (n m : nat) : n.+1 - m <= (n - m).+1. Proof. revert m. - induction n. - - induction m; [ apply leq_n | apply leq_S; apply leq_n ]. - - intro m; induction m. + simple_induction n n IHn. + - simple_induction m m IHm; [ apply leq_n | apply leq_S; apply leq_n ]. + - intro m; simple_induction m m IHm. + apply leq_n. + apply IHn. Defined. @@ -502,7 +504,7 @@ Defined. Proposition nataddsub_comm_ineq (n m k : nat) : (n + k) - m <= (n - m) + k. Proof. - induction k. + simple_induction k k IHk. - destruct (add_n_O n), (add_n_O (n - m)); constructor. - destruct (add_n_Sm n k). refine (leq_trans (nataddsub_comm_ineq_lemma (n+k) m) _). @@ -524,9 +526,9 @@ Defined. Proposition i_lt_n_sum_m (n m i : nat) : i < n - m -> m <= n. Proof. - revert m i; induction n. + revert m i; simple_induction n n IHn. - intros m i l. simpl in l. contradiction (not_lt_n_0 _ _). - - intros m i l. induction m. + - intros m i l. destruct m. + apply leq_0_n. + apply leq_S_n'. simpl in l. apply (IHn m i l). Defined. @@ -552,7 +554,7 @@ Defined. Proposition predeqminus1 { n : nat } : n - 1 = pred n. Proof. - induction n. + simple_induction' n. - reflexivity. - apply sub_n_0. Defined. @@ -566,8 +568,7 @@ Defined. Proposition S_predn (n i: nat) : (i < n) -> S(pred n) = n. Proof. - intros l. - induction n. + simple_induction' n; intros l. - contradiction (not_lt_n_0 i). - reflexivity. Defined. @@ -649,7 +650,7 @@ Defined. Proposition natsubpreservesleq { n m k : nat } : n <= m -> n - k <= m - k. Proof. - induction k. + simple_induction k k IHk. - destruct (symmetric_paths _ _ (sub_n_0 n)), (symmetric_paths _ _ (sub_n_0 m)); done. - intro l. change (k.+1) with (1 + k). @@ -666,9 +667,9 @@ Defined. Proposition sub_less { n k : nat } : n - k <= n. Proof. revert k. - induction n. + simple_induction n n IHn. - intros; apply leq_0_n. - - induction k. + - destruct k. + apply leq_n. + simpl; apply (@leq_trans _ n _); [ apply IHn | apply leq_S, leq_n]. @@ -744,10 +745,10 @@ Defined. Proposition nat_add_bifunctor (n n' m m' : nat) : n <= m -> n' <= m' -> n + n' <= m + m'. Proof. - revert n' m m'; induction n. + revert n' m m'; simple_induction n n IHn. - intros n' m m' l l'. simpl. apply (leq_trans l'). exact (n_leq_add_n_k' m' m). - - intros n' m; induction m. + - intros n' m; destruct m. + intros. contradiction (not_leq_Sn_0 n). + intros m' l l'. apply leq_S_n in l. simpl. apply leq_S_n', IHn. @@ -782,7 +783,7 @@ Proposition strong_induction (P : nat -> Type) Proof. intro a. assert (forall n m: nat, m < n -> P m) as X. { - induction n. + simple_induction n n IHn. - intros m l. contradiction (not_lt_n_0 m). - intros m l. apply leq_S_n in l. destruct l as [ | n]. @@ -816,9 +817,9 @@ Proof. - now constructor. Defined. -Proposition increasing_geq_n_0 (n :nat) : increasing_geq n 0. +Proposition increasing_geq_n_0 (n : nat) : increasing_geq n 0. Proof. - induction n. + simple_induction n n IHn. - constructor. - induction IHn. + constructor; now constructor. @@ -828,7 +829,7 @@ Defined. Lemma increasing_geq_minus (n k : nat) : increasing_geq n (n - k). Proof. - induction k. + simple_induction k k IHk. - destruct (symmetric_paths _ _ (sub_n_0 n)); constructor. - destruct (@leq_dichot n k) as [l | g]. + destruct (symmetric_paths _ _ (sub_leq_0 _ _ _)) in IHk. @@ -854,7 +855,7 @@ Defined. Lemma ineq_sub (n m : nat) : n <= m -> m - (m - n) = n. Proof. - revert m; induction n. + revert m; simple_induction n n IHn. - intros. destruct (symmetric_paths _ _ (sub_n_0 m)), (symmetric_paths _ _ (sub_n_n m)); reflexivity. diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v index c3004256adc..e2171a9b00e 100644 --- a/theories/Spaces/Nat/Core.v +++ b/theories/Spaces/Nat/Core.v @@ -3,6 +3,8 @@ Require Import Basics Types. Require Export Basics.Nat. Require Export HoTT.DProp. +Local Set Universe Minimization ToSet. + Local Unset Elimination Schemes. Scheme nat_ind := Induction for nat Sort Type. @@ -220,10 +222,10 @@ Defined. #[export] Hint Resolve not_eq_S : core. (** TODO: keep or remove? *) -Definition IsSucc (n: nat) : Type := +Definition IsSucc (n: nat) : Type0 := match n with - | O => False - | S p => True + | O => Empty + | S p => Unit end. (** Zero is not the successor of a number *) @@ -236,7 +238,7 @@ Defined. Theorem not_eq_n_Sn : forall n:nat, n <> S n. Proof. - induction n; auto. + simple_induction' n; auto. Defined. #[export] Hint Resolve not_eq_n_Sn : core. @@ -247,7 +249,7 @@ Local Definition ap011_nat := @ap011 nat nat. Lemma add_n_O : forall (n : nat), n = n + 0. Proof. - induction n; simpl; auto. + simple_induction' n; simpl; auto. Defined. #[export] Hint Resolve add_n_O : core. @@ -258,7 +260,7 @@ Defined. Lemma add_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. - intros n m; induction n; simpl; auto. + simple_induction' n; simpl; auto. Defined. #[export] Hint Resolve add_n_Sm: core. @@ -274,13 +276,13 @@ Local Definition ap011_mul := @ap011 _ _ _ mul. Lemma mul_n_O : forall n:nat, 0 = n * 0. Proof. - induction n; simpl; auto. + simple_induction' n; simpl; auto. Defined. #[export] Hint Resolve mul_n_O : core. Lemma mul_n_Sm : forall n m:nat, n * m + n = n * S m. Proof. - intros; induction n as [| p H]; simpl; auto. + intros; simple_induction n p H; simpl; auto. destruct H; rewrite <- add_n_Sm; apply ap. pattern m at 1 3; elim m; simpl; auto. Defined. @@ -295,7 +297,7 @@ Notation mul_succ_r_reverse := mul_n_Sm (only parsing). (** *** Boolean equality and its properties *) -Fixpoint code_nat (m n : nat) {struct m} : DHProp := +Fixpoint code_nat (m n : nat) {struct m} : DHProp@{Set} := match m, n with | 0, 0 => True | m'.+1, n'.+1 => code_nat m' n' @@ -341,7 +343,7 @@ Global Instance hset_nat : IsHSet nat := _. (** ** Inequality of natural numbers *) -Inductive leq (n : nat) : nat -> Type0 := +Cumulative Inductive leq (n : nat) : nat -> Type0 := | leq_n : leq n n | leq_S : forall m, leq n m -> leq n (S m). @@ -385,7 +387,7 @@ Global Existing Instance leq_S_n' | 100. Lemma not_leq_Sn_n n : ~ (n.+1 <= n). Proof. - induction n. + simple_induction n n IHn. { intro p. inversion p. } intros p. @@ -395,7 +397,7 @@ Defined. (** A general form for injectivity of this constructor *) Definition leq_n_inj_gen n k (p : n <= k) (r : n = k) : p = r # leq_n n. Proof. - induction p. + destruct p. + assert (c : idpath = r) by apply path_ishprop. destruct c. reflexivity. @@ -411,7 +413,7 @@ Fixpoint leq_S_inj_gen n m k (p : n <= k) (q : n <= m) (r : m.+1 = k) : p = r # leq_S n m q. Proof. revert m q r. - induction p. + destruct p. + intros k p r. destruct r. contradiction (not_leq_Sn_n _ p). @@ -442,7 +444,7 @@ Defined. Global Instance leq_0_n n : 0 <= n | 10. Proof. - induction n; auto. + simple_induction' n; auto. Defined. Lemma not_leq_Sn_0 n : ~ (n.+1 <= 0). @@ -461,7 +463,7 @@ Defined. Global Instance decidable_leq n m : Decidable (n <= m). Proof. revert n. - induction m; intros n. + simple_induction' m; intros n. - destruct n. + left; exact _. + right; apply not_leq_Sn_0. @@ -511,7 +513,7 @@ Defined. (** We define the less-than relation [lt] in terms of [leq] *) Definition lt n m : Type0 := leq (S n) m. - + (** We declare it as an existing class so typeclass search is performed on its goals. *) Existing Class lt. #[export] Hint Unfold lt : core typeclass_instances. @@ -561,7 +563,7 @@ Theorem nat_double_ind (R : nat -> nat -> Type) (H3 : forall n m, R n m -> R (S n) (S m)) : forall n m:nat, R n m. Proof. - induction n; auto. + simple_induction' n; auto. destruct m; auto. Defined. @@ -569,19 +571,19 @@ Defined. Lemma max_n_n n : max n n = n. Proof. - induction n; cbn; auto. + simple_induction' n; cbn; auto. Defined. #[export] Hint Resolve max_n_n : core. Lemma max_Sn_n n : max (S n) n = S n. Proof. - induction n; cbn; auto. + simple_induction' n; cbn; auto. Defined. #[export] Hint Resolve max_Sn_n : core. Lemma max_comm n m : max n m = max m n. Proof. - revert m; induction n; destruct m; cbn; auto. + revert m; simple_induction' n; destruct m; cbn; auto. Defined. Lemma max_0_n n : max 0 n = n. @@ -598,7 +600,7 @@ Defined. Theorem max_l : forall n m, m <= n -> max n m = n. Proof. - intros n m; revert n; induction m; auto. + intros n m; revert n; simple_induction m m IHm; auto. intros [] p. 1: inversion p. cbn; by apply ap_S, IHm, leq_S_n. @@ -611,12 +613,12 @@ Defined. Lemma min_comm : forall n m, min n m = min m n. Proof. - induction n; destruct m; cbn; auto. -Defined. + simple_induction' n; destruct m; cbn; auto. +Defined. Theorem min_l : forall n m : nat, n <= m -> min n m = n. Proof. - intros n m; revert m; induction n; auto. + simple_induction n n IHn; auto. intros [] p. 1: inversion p. cbn; by apply ap_S, IHn, leq_S_n. @@ -638,14 +640,14 @@ Notation nat_iter n f x Lemma nat_iter_succ_r n {A} (f : A -> A) (x : A) : nat_iter (S n) f x = nat_iter n f (f x). Proof. - induction n as [|n IHn]; simpl; trivial. + simple_induction n n IHn; simpl; trivial. exact (ap f IHn). Defined. Theorem nat_iter_add (n m : nat) {A} (f : A -> A) (x : A) : nat_iter (n + m) f x = nat_iter n f (nat_iter m f x). Proof. - induction n as [|n IHn]; simpl; trivial. + simple_induction n n IHn; simpl; trivial. exact (ap f IHn). Defined. @@ -653,7 +655,7 @@ Defined. Theorem nat_iter_invariant (n : nat) {A} (f : A -> A) (P : A -> Type) : (forall x, P x -> P (f x)) -> forall x, P x -> P (nat_iter n f x). Proof. - induction n as [|n IHn]; simpl; trivial. + simple_induction n n IHn; simpl; trivial. intros Hf x Hx. apply Hf, IHn; trivial. Defined. @@ -662,14 +664,14 @@ Defined. Lemma nat_add_n_Sm (n m : nat) : (n + m).+1 = n + m.+1. Proof. - induction n; simpl. + simple_induction' n; simpl. - reflexivity. - apply ap; assumption. Defined. Definition nat_add_comm (n m : nat) : n + m = m + n. Proof. - induction n as [|n IHn]; simpl. + simple_induction n n IHn; simpl. - exact (add_n_O m). - transitivity (m + n).+1. + apply ap, IHn. @@ -713,12 +715,12 @@ Definition leq_1_Sn {n} : 1 <= n.+1 := leq_S_n' 0 n (leq_0_n _). Fixpoint leq_dichot {m} {n} : (m <= n) + (m > n). Proof. - induction m, n. + simple_induction' m; simple_induction' n. - left; reflexivity. - left; apply leq_0_n. - right; unfold lt; apply leq_1_Sn. - assert ((m <= n) + (n < m)) as X by apply leq_dichot. - induction X as [leqmn|ltnm]. + destruct X as [leqmn|ltnm]. + left; apply leq_S_n'; assumption. + right; apply leq_S_n'; assumption. Defined.