summaryrefslogtreecommitdiff
path: root/theories/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Div2.v64
-rw-r--r--theories/Arith/Even.v158
-rw-r--r--theories/Arith/Max.v6
3 files changed, 78 insertions, 150 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 1216a545..7cab976f 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Div2.v 10625 2008-03-06 11:21:01Z notin $ i*)
+(*i $Id: Div2.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
Require Import Lt.
Require Import Plus.
@@ -60,45 +60,38 @@ Hint Resolve lt_div2: arith.
(** Properties related to the parity *)
-Lemma even_odd_div2 :
- forall n,
- (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Lemma even_div2 : forall n, even n -> div2 n = div2 (S n)
+with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
Proof.
- intro n. pattern n in |- *. apply ind_0_1_SS.
- (* n = 0 *)
- split. split; auto with arith.
- split. intro H. inversion H.
- intro H. absurd (S (div2 0) = div2 1); auto with arith.
- (* n = 1 *)
- split. split. intro. inversion H. inversion H1.
- intro H. absurd (div2 1 = div2 2).
- simpl in |- *. discriminate. assumption.
- split; auto with arith.
- (* n = (S (S n')) *)
- intros. decompose [and] H. unfold iff in H0, H1.
- decompose [and] H0. decompose [and] H1. clear H H0 H1.
- split; split; auto with arith.
- intro H. inversion H. inversion H1.
- change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
- intro H. inversion H. inversion H1.
- change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
+ destruct n; intro H.
+ (* 0 *) trivial.
+ (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial.
+ destruct n; intro.
+ (* 0 *) inversion H.
+ (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
Qed.
-(** Specializations *)
-
-Lemma even_div2 : forall n, even n -> div2 n = div2 (S n).
-Proof fun n => proj1 (proj1 (even_odd_div2 n)).
+Lemma div2_even : forall n, div2 n = div2 (S n) -> even n
+with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Proof.
+ destruct n; intro H.
+ (* 0 *) constructor.
+ (* S n *) constructor. apply div2_odd. rewrite H. trivial.
+ destruct n; intro H.
+ (* 0 *) discriminate.
+ (* S n *) constructor. apply div2_even. injection H as <-. trivial.
+Qed.
-Lemma div2_even : forall n, div2 n = div2 (S n) -> even n.
-Proof fun n => proj2 (proj1 (even_odd_div2 n)).
+Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
-Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
-Proof fun n => proj1 (proj2 (even_odd_div2 n)).
+Lemma even_odd_div2 :
+ forall n,
+ (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Proof.
+ auto decomp using div2_odd, div2_even, odd_div2, even_div2.
+Qed.
-Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
-Proof fun n => proj2 (proj2 (even_odd_div2 n)).
-Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
(** Properties related to the double ([2n]) *)
@@ -132,8 +125,7 @@ Proof.
split; split; auto with arith.
intro H. inversion H. inversion H1.
(* n = (S (S n')) *)
- intros. decompose [and] H. unfold iff in H0, H1.
- decompose [and] H0. decompose [and] H1. clear H H0 H1.
+ intros. destruct H as ((IH1,IH2),(IH3,IH4)).
split; split.
intro H. inversion H. inversion H1.
simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
@@ -142,8 +134,6 @@ Proof.
simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
Qed.
-
-
(** Specializations *)
Lemma even_double : forall n, even n -> n = double (div2 n).
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 1484666b..59209370 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Even.v 10410 2007-12-31 13:11:55Z msozeau $ i*)
+(*i $Id: Even.v 11512 2008-10-27 12:28:36Z herbelin $ i*)
(** Here we define the predicates [even] and [odd] by mutual induction
and we prove the decidability and the exclusion of those predicates.
@@ -52,153 +52,91 @@ Qed.
(** * Facts about [even] & [odd] wrt. [plus] *)
-Lemma even_plus_aux :
- forall n m,
- (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
- (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
+Lemma even_plus_split : forall n m,
+ (even (n + m) -> even n /\ even m \/ odd n /\ odd m)
+with odd_plus_split : forall n m,
+ odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
- intros n; elim n; simpl in |- *; auto with arith.
- intros m; split; auto.
- split.
- intros H; right; split; auto with arith.
- intros H'; case H'; auto with arith.
- intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
- intros H; elim H; auto.
- split; auto with arith.
- intros H'; elim H'; auto with arith.
- intros H; elim H; auto.
- intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
- intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2;
- intros E3 E4; clear H'1 H'2.
- split; split.
- intros H'0; case E3.
- inversion H'0; auto.
- intros H; elim H; intros H0 H1; clear H; auto with arith.
- intros H; elim H; intros H0 H1; clear H; auto with arith.
- intros H'0; case H'0; intros C0; case C0; intros C1 C2.
- apply odd_S.
- apply E4; left; split; auto with arith.
- inversion C1; auto.
- apply odd_S.
- apply E4; right; split; auto with arith.
- inversion C1; auto.
- intros H'0.
- case E1.
- inversion H'0; auto.
- intros H; elim H; intros H0 H1; clear H; auto with arith.
- intros H; elim H; intros H0 H1; clear H; auto with arith.
- intros H'0; case H'0; intros C0; case C0; intros C1 C2.
- apply even_S.
- apply E2; left; split; auto with arith.
- inversion C1; auto.
- apply even_S.
- apply E2; right; split; auto with arith.
- inversion C1; auto.
+intros. clear even_plus_split. destruct n; simpl in *.
+ auto with arith.
+ inversion_clear H;
+ apply odd_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
+intros. clear odd_plus_split. destruct n; simpl in *.
+ auto with arith.
+ inversion_clear H;
+ apply even_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
Qed.
-
-Lemma even_even_plus : forall n m, even n -> even m -> even (n + m).
+
+Lemma even_even_plus : forall n m, even n -> even m -> even (n + m)
+with odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
Proof.
- intros n m; case (even_plus_aux n m).
- intros H H0; case H0; auto.
+intros n m [|] ?. trivial. apply even_S, odd_plus_l; trivial.
+intros n m [] ?. apply odd_S, even_even_plus; trivial.
Qed.
-
-Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
+
+Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m)
+with odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
Proof.
- intros n m; case (even_plus_aux n m).
- intros H H0; case H0; auto.
+intros n m [|] ?. trivial. apply odd_S, odd_even_plus; trivial.
+intros n m [] ?. apply even_S, odd_plus_r; trivial.
+Qed.
+
+Lemma even_plus_aux : forall n m,
+ (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
+ (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
+Proof.
+split; split; auto using odd_plus_split, even_plus_split.
+intros [[]|[]]; auto using odd_plus_r, odd_plus_l.
+intros [[]|[]]; auto using even_even_plus, odd_even_plus.
Qed.
Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'0.
- intros H'1; case H'1; auto.
- intros H0; elim H0; auto.
- intros H0 H1 H2; case (not_even_and_odd n); auto.
- case H0; auto.
+ intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd n); auto.
Qed.
Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'0.
- intros H'1; case H'1; auto.
- intros H0; elim H0; auto.
- intros H0 H1 H2; case (not_even_and_odd m); auto.
- case H0; auto.
+ intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd m); auto.
Qed.
Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'0.
- intros H'1; case H'1; auto.
- intros H0 H1 H2; case (not_even_and_odd n); auto.
- case H0; auto.
- intros H0; case H0; auto.
+ intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd n); auto.
Qed.
Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'0.
- intros H'1; case H'1; auto.
- intros H0 H1 H2; case (not_even_and_odd m); auto.
- case H0; auto.
- intros H0; case H0; auto.
+ intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd m); auto.
Qed.
Hint Resolve even_even_plus odd_even_plus: arith.
-Lemma odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
-Proof.
- intros n m; case (even_plus_aux n m).
- intros H; case H; auto.
-Qed.
-
-Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m).
-Proof.
- intros n m; case (even_plus_aux n m).
- intros H; case H; auto.
-Qed.
-
Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'.
- intros H'1; case H'1; auto.
- intros H0 H1 H2; case (not_even_and_odd m); auto.
- case H0; auto.
- intros H0; case H0; auto.
+ intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd m); auto.
Qed.
Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'.
- intros H'1; case H'1; auto.
- intros H0; case H0; auto.
- intros H0 H1 H2; case (not_even_and_odd n); auto.
- case H0; auto.
+ intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd n); auto.
Qed.
Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'.
- intros H'1; case H'1; auto.
- intros H0; case H0; auto.
- intros H0 H1 H2; case (not_even_and_odd m); auto.
- case H0; auto.
+ intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd m); auto.
Qed.
Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m.
Proof.
- intros n m H; case (even_plus_aux n m).
- intros H' H'0; elim H'.
- intros H'1; case H'1; auto.
- intros H0 H1 H2; case (not_even_and_odd n); auto.
- case H0; auto.
- intros H0; case H0; auto.
+ intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+ intro; destruct (not_even_and_odd n); auto.
Qed.
Hint Resolve odd_plus_l odd_plus_r: arith.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 95af67f8..5de2298d 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Max.v 9883 2007-06-07 18:44:59Z letouzey $ i*)
+(*i $Id: Max.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
Require Import Le.
@@ -74,13 +74,13 @@ Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
Proof.
induction n; induction m; simpl in |- *; auto with arith.
elim (IHn m); intro H; elim H; auto.
-Qed.
+Defined.
Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
Proof.
induction n; simpl in |- *; auto with arith.
induction m; intros; simpl in |- *; auto with arith.
pattern (max n m) in |- *; apply IHn; auto with arith.
-Qed.
+Defined.
Notation max_case2 := max_case (only parsing).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 15:40:50 +0000