From b40eb1628b85bbf4605fad2222c86ea796425e2a Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Tue, 3 Oct 2017 16:19:17 +0200 Subject: Add leb_not_le: (n <=? m) = false -> n > m. --- theories/Arith/PeanoNat.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'theories') diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index bde6f1bb4..ffa56a6c3 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -172,6 +172,17 @@ Proof. apply leb_le. Qed. + +Lemma leb_not_le n m : (n <=? m) = false -> n > m. +Proof. + revert m; induction n; destruct m; simpl; intros H_nm. + - congruence. + - congruence. + - apply lt_succ_r, le_0_n. + - specialize (IHn _ H_nm). + now apply lt_succ_r in IHn. +Qed. + (** ** Decidability of equality over [nat]. *) Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}. -- cgit v1.2.3 From d4009edb53ab7780bc85d83ccf01c6920c7f09e1 Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Tue, 3 Oct 2017 16:19:37 +0200 Subject: Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x. --- theories/QArith/QArith_base.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'theories') diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a19f9f902..16963b021 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -171,6 +171,19 @@ Proof. auto with qarith. Qed. +Lemma Qeq_bool_sym x y: Qeq_bool x y = Qeq_bool y x. +Proof. + case_eq (Qeq_bool x y); intros H_eq_xy. + - unfold Qeq_bool in *. + rewrite <- Zeq_is_eq_bool in H_eq_xy. + rewrite H_eq_xy; symmetry. + rewrite <- Zeq_is_eq_bool; auto. + - apply Zeq_bool_neq in H_eq_xy. + case_eq (Qeq_bool y x); intros H_eq_yx. + + apply Zeq_is_eq_bool in H_eq_yx; congruence. + + auto. +Qed. + Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) -- cgit v1.2.3 From dfa56fb57b09296cdf311ec5972d2d33b787e48c Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Tue, 3 Oct 2017 16:20:08 +0200 Subject: Add Qabs_Qinv: Qabs (/ q) == / (Qabs q). --- theories/QArith/Qabs.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'theories') diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 116aa0d42..ec2ac7832 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -100,6 +100,13 @@ rewrite Z.abs_mul. reflexivity. Qed. +Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q). +Proof. + intros [n d]; simpl. + unfold Qinv. + case_eq n; intros; simpl in *; apply Qeq_refl. +Qed. + Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x). Proof. unfold Qminus, Qopp. simpl. -- cgit v1.2.3 From b4b778f1a1657e0b65f5ac3fe466ca9a1e8d55d3 Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Tue, 3 Oct 2017 20:45:13 +0200 Subject: Changed the statement of leb_not_le; shortened the proof --- theories/Arith/PeanoNat.v | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'theories') diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index ffa56a6c3..95fd4cf86 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -172,15 +172,9 @@ Proof. apply leb_le. Qed. - -Lemma leb_not_le n m : (n <=? m) = false -> n > m. +Lemma leb_not_le n m : (n <=? m) = false <-> ~n <= m. Proof. - revert m; induction n; destruct m; simpl; intros H_nm. - - congruence. - - congruence. - - apply lt_succ_r, le_0_n. - - specialize (IHn _ H_nm). - now apply lt_succ_r in IHn. + now rewrite <- leb_le, <- not_true_iff_false. Qed. (** ** Decidability of equality over [nat]. *) -- cgit v1.2.3 From 2ac3427a8366c28be37b33deb47e7823378263a3 Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Sun, 8 Oct 2017 21:17:00 +0200 Subject: Removed leb_not_le (already existing as Nat.leb_nle) --- theories/Arith/PeanoNat.v | 5 ----- 1 file changed, 5 deletions(-) (limited to 'theories') diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index 95fd4cf86..bde6f1bb4 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -172,11 +172,6 @@ Proof. apply leb_le. Qed. -Lemma leb_not_le n m : (n <=? m) = false <-> ~n <= m. -Proof. - now rewrite <- leb_le, <- not_true_iff_false. -Qed. - (** ** Decidability of equality over [nat]. *) Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}. -- cgit v1.2.3 From 0a65d234346a73c98a9f65d2248edbbbe5e9fccb Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Sun, 8 Oct 2017 21:27:14 +0200 Subject: Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey. --- theories/QArith/QArith_base.v | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'theories') diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 16963b021..a94435c3f 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -171,17 +171,9 @@ Proof. auto with qarith. Qed. -Lemma Qeq_bool_sym x y: Qeq_bool x y = Qeq_bool y x. -Proof. - case_eq (Qeq_bool x y); intros H_eq_xy. - - unfold Qeq_bool in *. - rewrite <- Zeq_is_eq_bool in H_eq_xy. - rewrite H_eq_xy; symmetry. - rewrite <- Zeq_is_eq_bool; auto. - - apply Zeq_bool_neq in H_eq_xy. - case_eq (Qeq_bool y x); intros H_eq_yx. - + apply Zeq_is_eq_bool in H_eq_yx; congruence. - + auto. +Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x. +Proof. + apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry. Qed. Hint Resolve Qnot_eq_sym : qarith. -- cgit v1.2.3 From e5b43dcd5f449ccbc84c32868f9a9f6c3b73b263 Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Thu, 12 Oct 2017 13:45:19 +0200 Subject: Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans. --- theories/QArith/QArith_base.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'theories') diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a94435c3f..121527c63 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -176,6 +176,21 @@ Proof. apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry. Qed. +Lemma Qeq_bool_refl x: is_true (Qeq_bool x x). +Proof. + unfold is_true. rewrite Qeq_bool_iff. now reflexivity. +Qed. + +Lemma Qeq_bool_sym x y: is_true (Qeq_bool x y) -> is_true (Qeq_bool y x). +Proof. + unfold is_true. rewrite !Qeq_bool_iff. now symmetry. +Qed. + +Lemma Qeq_bool_trans x y z: is_true (Qeq_bool x y) -> is_true (Qeq_bool y z) -> is_true (Qeq_bool x z). +Proof. + unfold is_true. rewrite !Qeq_bool_iff. apply Qeq_trans. +Qed. + Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) -- cgit v1.2.3 From 5431b0f17cd73a09472093e779cc1508b3b3ac4f Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Wed, 25 Oct 2017 16:14:10 +0200 Subject: Moving from `is_true` to `= true` --- theories/QArith/QArith_base.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'theories') diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 121527c63..66740512b 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -176,19 +176,19 @@ Proof. apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry. Qed. -Lemma Qeq_bool_refl x: is_true (Qeq_bool x x). +Lemma Qeq_bool_refl x: Qeq_bool x x = true. Proof. - unfold is_true. rewrite Qeq_bool_iff. now reflexivity. + rewrite Qeq_bool_iff. now reflexivity. Qed. -Lemma Qeq_bool_sym x y: is_true (Qeq_bool x y) -> is_true (Qeq_bool y x). +Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true. Proof. - unfold is_true. rewrite !Qeq_bool_iff. now symmetry. + rewrite !Qeq_bool_iff. now symmetry. Qed. -Lemma Qeq_bool_trans x y z: is_true (Qeq_bool x y) -> is_true (Qeq_bool y z) -> is_true (Qeq_bool x z). +Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true. Proof. - unfold is_true. rewrite !Qeq_bool_iff. apply Qeq_trans. + rewrite !Qeq_bool_iff. apply Qeq_trans. Qed. Hint Resolve Qnot_eq_sym : qarith. -- cgit v1.2.3 From 84e274fb6d36bbd8306c2977520ebe1cf410349a Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Fri, 27 Oct 2017 10:46:41 +0200 Subject: Chaining two tactics in a proof --- theories/QArith/QArith_base.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 66740512b..5996d30f2 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -188,7 +188,7 @@ Qed. Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true. Proof. - rewrite !Qeq_bool_iff. apply Qeq_trans. + rewrite !Qeq_bool_iff; apply Qeq_trans. Qed. Hint Resolve Qnot_eq_sym : qarith. -- cgit v1.2.3