Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove deprecated files in Coq.Arith #121

Merged
merged 1 commit into from
Oct 16, 2023
Merged

Remove deprecated files in Coq.Arith #121

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 19 additions & 18 deletions implementations/peano_naturals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
Require
MathClasses.theory.ua_homomorphisms.
Require Import
Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base
Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base Coq.Arith.PeanoNat
MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories
MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.semirings.

Expand All @@ -20,14 +20,14 @@ Instance nat_mult: Mult nat := Peano.mult.
Instance: SemiRing nat.
Proof.
repeat (split; try apply _); repeat intro.
now apply plus_assoc.
now apply plus_0_r.
now apply plus_comm.
now apply mult_assoc.
now apply mult_1_l.
now apply mult_1_r.
now apply mult_comm.
now apply mult_plus_distr_l.
now apply Nat.add_assoc.
now apply Nat.add_0_r.
now apply Nat.add_comm.
now apply Nat.mul_assoc.
now apply Nat.mul_1_l.
now apply Nat.mul_1_r.
now apply Nat.mul_comm.
now apply Nat.mul_add_distr_l.
Qed.

(* misc *)
Expand Down Expand Up @@ -115,7 +115,7 @@ Instance: Naturals nat := {}.
(* Misc *)
#[global]
Instance: NoZeroDivisors nat.
Proof. intros x [Ex [y [Ey1 Ey2]]]. destruct (Mult.mult_is_O x y Ey2); intuition. Qed.
Proof. now intros x [Ex [y [Ey1 [H | H]%Nat.eq_mul_0]]]. Qed.

#[global]
Instance: ∀ z : nat, PropHolds (z ≠ 0) → LeftCancellation (.*.) z.
Expand All @@ -133,13 +133,14 @@ Proof.
assert (TotalRelation nat_le).
intros x y. now destruct (le_ge_dec x y); intuition.
assert (PartialOrder nat_le).
split; try apply _. intros x y E. now apply Le.le_antisym.
split; try apply _. intros x y E. now apply Nat.le_antisymm.
assert (SemiRingOrder nat_le).
repeat (split; try apply _).
intros x y E. exists (y - x)%nat. now apply le_plus_minus.
intros. now apply Plus.plus_le_compat_l.
intros. now apply plus_le_reg_l with z.
intros x y ? ?. change (0 * 0 <= x * y)%nat. now apply Mult.mult_le_compat.
intros x y E. exists (y - x)%nat.
now rewrite Nat.add_comm, Nat.sub_add by (exact E).
intros. now apply Nat.add_le_mono_l.
intros. now apply Nat.add_le_mono_l with z.
intros x y ? ?. change (0 * 0 <= x * y)%nat. now apply Nat.mul_le_mono.
apply dec_full_pseudo_srorder.
now apply Nat.le_neq.
Qed.
Expand All @@ -162,8 +163,8 @@ Instance: CutMinusSpec nat nat_cut_minus.
Proof.
split.
symmetry. rewrite commutativity.
now apply le_plus_minus.
now rewrite Nat.add_comm, Nat.sub_add by (exact H).
intros x y E. destruct (orders.le_equiv_lt x y E) as [E2|E2].
rewrite E2. now apply minus_diag.
apply not_le_minus_0. now apply orders.lt_not_le_flip.
rewrite E2. now apply Nat.sub_diag.
apply Nat.sub_0_le; exact E.
Qed.
9 changes: 5 additions & 4 deletions theory/naturals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
Require Import
Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings
Coq.Arith.PeanoNat
MathClasses.categories.varieties MathClasses.theory.ua_transference.
Require Export
MathClasses.interfaces.naturals.
Expand Down Expand Up @@ -128,7 +129,7 @@ Section borrowed_from_nat.
Proof.
intros x y z.
rapply (from_nat_stmt (x' + y' === x' + z' -=> y' === z') (three_vars x y z)).
intro. simpl. apply Plus.plus_reg_l.
intro. simpl. apply Nat.add_cancel_l.
Qed.

Global Instance: ∀ z : N, RightCancellation (+) z.
Expand Down Expand Up @@ -156,20 +157,20 @@ Section borrowed_from_nat.
Lemma zero_sum (x y : N) : x + y = 0 → x = 0 ∧ y = 0.
Proof.
rapply (from_nat_stmt (x' + y' === 0 -=> Conj _ (x' === 0) (y' === 0)) (two_vars x y)).
intro. simpl. apply Plus.plus_is_O.
intro. simpl. apply Nat.eq_add_0.
Qed.

Lemma one_sum (x y : N) : x + y = 1 → (x = 1 ∧ y = 0) ∨ (x = 0 ∧ y = 1).
Proof.
rapply (from_nat_stmt (x' + y' === 1 -=> Disj _ (Conj _ (x' === 1) (y' === 0)) (Conj _ (x' === 0) (y' === 1))) (two_vars x y)).
intros. simpl. intros. edestruct Plus.plus_is_one; eauto.
intros. simpl. intros. edestruct Nat.eq_add_1; eauto.
Qed.

Global Instance: ZeroProduct N.
Proof.
intros x y.
rapply (from_nat_stmt (x' * y' === 0 -=>Disj _ (x' === 0) (y' === 0)) (two_vars x y)).
intros ? E. destruct (Mult.mult_is_O _ _ E); red; intuition.
intros ? E. destruct ((proj1 (Nat.eq_mul_0 _ _)) E); red; intuition.
Qed.
End borrowed_from_nat.

Expand Down
Loading