summaryrefslogtreecommitdiff
path: root/theories/NArith/Ndigits.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /theories/NArith/Ndigits.v
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/NArith/Ndigits.v')
-rw-r--r--theories/NArith/Ndigits.v289
1 files changed, 135 insertions, 154 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index dcdb5f92..fb32274e 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ndigits.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: Ndigits.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
Require Import Bool.
Require Import Bvector.
@@ -52,8 +52,8 @@ Proof.
destruct n; destruct n'; simpl; auto.
generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl;
auto.
- destruct p0; simpl; trivial; intros; rewrite Hrecp; trivial.
- destruct p0; simpl; trivial; intros; rewrite Hrecp; trivial.
+ destruct p0; trivial; rewrite Hrecp; trivial.
+ destruct p0; trivial; rewrite Hrecp; trivial.
destruct p0 as [p| p| ]; simpl; auto.
Qed.
@@ -115,7 +115,7 @@ Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n).
Lemma xorf_eq :
forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'.
Proof.
- unfold eqf, xorf. intros. apply xorb_eq. apply H.
+ unfold eqf, xorf. intros. apply xorb_eq, H.
Qed.
Lemma xorf_assoc :
@@ -166,14 +166,12 @@ Lemma Nbit_faithful_3 :
(forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') ->
eqf (Nbit (Npos (xO p))) (Nbit a) -> Npos (xO p) = a.
Proof.
- destruct a. intros. cut (eqf (Nbit N0) (Nbit (Npos (xO p)))).
+ destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xO p)))).
intro. rewrite (Nbit_faithful_1 (Npos (xO p)) H1). reflexivity.
unfold eqf. intro. unfold eqf in H0. rewrite H0. reflexivity.
- case p. intros. absurd (false = true). discriminate.
- exact (H0 0).
- intros. rewrite (H p0 (fun n => H0 (S n))). reflexivity.
- intros. absurd (false = true). discriminate.
- exact (H0 0).
+ destruct p. discriminate (H0 O).
+ rewrite (H p (fun n => H0 (S n))). reflexivity.
+ discriminate (H0 0).
Qed.
Lemma Nbit_faithful_4 :
@@ -181,27 +179,26 @@ Lemma Nbit_faithful_4 :
(forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') ->
eqf (Nbit (Npos (xI p))) (Nbit a) -> Npos (xI p) = a.
Proof.
- destruct a. intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))).
+ destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))).
intro. rewrite (Nbit_faithful_1 (Npos (xI p)) H1). reflexivity.
- unfold eqf. intro. unfold eqf in H0. rewrite H0. reflexivity.
- case p. intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity.
- intros. absurd (true = false). discriminate.
- exact (H0 0).
- intros. absurd (N0 = Npos p0). discriminate.
+ intro. rewrite H0. reflexivity.
+ destruct p. rewrite (H p (fun n:nat => H0 (S n))). reflexivity.
+ discriminate (H0 0).
cut (eqf (Nbit (Npos 1)) (Nbit (Npos (xI p0)))).
- intro. exact (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))).
- unfold eqf in *. intro. rewrite H0. reflexivity.
+ intro. discriminate (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))).
+ intro. rewrite H0. reflexivity.
Qed.
Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'.
Proof.
destruct a. exact Nbit_faithful_1.
- induction p. intros a' H. apply Nbit_faithful_4. intros. cut (Npos p = Npos p').
- intro. inversion H1. reflexivity.
- exact (IHp (Npos p') H0).
+ induction p. intros a' H. apply Nbit_faithful_4. intros.
+ assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
+ inversion H1. reflexivity.
assumption.
- intros. apply Nbit_faithful_3. intros. cut (Npos p = Npos p'). intro. inversion H1. reflexivity.
- exact (IHp (Npos p') H0).
+ intros. apply Nbit_faithful_3. intros.
+ assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
+ inversion H1. reflexivity.
assumption.
exact Nbit_faithful_2.
Qed.
@@ -216,40 +213,37 @@ Qed.
Lemma Nxor_sem_2 :
forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0).
Proof.
- intro. case a'. trivial.
- simpl. intro.
- case p; trivial.
+ intro. destruct a'. trivial.
+ destruct p; trivial.
Qed.
Lemma Nxor_sem_3 :
forall (p:positive) (a':N),
Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0.
Proof.
- intros. case a'. trivial.
- simpl. intro.
- case p0; trivial. intro.
- case (Pxor p p1); trivial.
- intro. case (Pxor p p1); trivial.
+ intros. destruct a'. trivial.
+ simpl. destruct p0; trivial.
+ destruct (Pxor p p0); trivial.
+ destruct (Pxor p p0); trivial.
Qed.
Lemma Nxor_sem_4 :
forall (p:positive) (a':N),
Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0).
Proof.
- intros. case a'. trivial.
- simpl. intro. case p0; trivial. intro.
- case (Pxor p p1); trivial.
- intro.
- case (Pxor p p1); trivial.
+ intros. destruct a'. trivial.
+ simpl. destruct p0; trivial.
+ destruct (Pxor p p0); trivial.
+ destruct (Pxor p p0); trivial.
Qed.
Lemma Nxor_sem_5 :
forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0.
Proof.
- destruct a. intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial.
- case p. exact Nxor_sem_4.
- intros. change (Nbit (Nxor (Npos (xO p0)) a') 0 = xorb false (Nbit a' 0)).
- rewrite false_xorb. apply Nxor_sem_3. exact Nxor_sem_2.
+ destruct a; intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial.
+ destruct p. apply Nxor_sem_4.
+ change (Nbit (Nxor (Npos (xO p)) a') 0 = xorb false (Nbit a' 0)).
+ rewrite false_xorb. apply Nxor_sem_3. apply Nxor_sem_2.
Qed.
Lemma Nxor_sem_6 :
@@ -258,28 +252,29 @@ Lemma Nxor_sem_6 :
forall a a':N,
Nbit (Nxor a a') (S n) = xorf (Nbit a) (Nbit a') (S n).
Proof.
- intros.
+ intros.
+(* pose proof (fun p1 p2 => H (Npos p1) (Npos p2)) as H'. clear H. rename H' into H.*)
generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H.
unfold xorf in *.
- case a. simpl Nbit; rewrite false_xorb. reflexivity.
- case a'; intros.
+ destruct a as [|p]. simpl Nbit; rewrite false_xorb. reflexivity.
+ destruct a' as [|p0].
simpl Nbit; rewrite xorb_false. reflexivity.
- case p0. case p; intros; simpl Nbit in *.
- rewrite <- H; simpl; case (Pxor p2 p1); trivial.
- rewrite <- H; simpl; case (Pxor p2 p1); trivial.
+ destruct p. destruct p0; simpl Nbit in *.
+ rewrite <- H; simpl; case (Pxor p p0); trivial.
+ rewrite <- H; simpl; case (Pxor p p0); trivial.
rewrite xorb_false. reflexivity.
- case p; intros; simpl Nbit in *.
- rewrite <- H; simpl; case (Pxor p2 p1); trivial.
- rewrite <- H; simpl; case (Pxor p2 p1); trivial.
+ destruct p0; simpl Nbit in *.
+ rewrite <- H; simpl; case (Pxor p p0); trivial.
+ rewrite <- H; simpl; case (Pxor p p0); trivial.
rewrite xorb_false. reflexivity.
- simpl Nbit. rewrite false_xorb. simpl. case p; trivial.
+ simpl Nbit. rewrite false_xorb. destruct p0; trivial.
Qed.
Lemma Nxor_semantics :
forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')).
Proof.
- unfold eqf. intros. generalize a a'. elim n. exact Nxor_sem_5.
- exact Nxor_sem_6.
+ unfold eqf. intros; generalize a, a'. induction n.
+ apply Nxor_sem_5. apply Nxor_sem_6; assumption.
Qed.
(** Consequences:
@@ -289,8 +284,8 @@ Qed.
Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'.
Proof.
- intros. apply Nbit_faithful. apply xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')).
- apply eqf_sym. apply Nxor_semantics.
+ intros. apply Nbit_faithful, xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')).
+ apply eqf_sym, Nxor_semantics.
rewrite H. unfold eqf. trivial.
Qed.
@@ -298,19 +293,17 @@ Lemma Nxor_assoc :
forall a a' a'':N, Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'').
Proof.
intros. apply Nbit_faithful.
- apply eqf_trans with
- (f' := xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')).
- apply eqf_trans with (f' := xorf (Nbit (Nxor a a')) (Nbit a'')).
+ apply eqf_trans with (xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')).
+ apply eqf_trans with (xorf (Nbit (Nxor a a')) (Nbit a'')).
apply Nxor_semantics.
apply eqf_xorf. apply Nxor_semantics.
apply eqf_refl.
- apply eqf_trans with
- (f' := xorf (Nbit a) (xorf (Nbit a') (Nbit a''))).
+ apply eqf_trans with (xorf (Nbit a) (xorf (Nbit a') (Nbit a''))).
apply xorf_assoc.
- apply eqf_trans with (f' := xorf (Nbit a) (Nbit (Nxor a' a''))).
+ apply eqf_trans with (xorf (Nbit a) (Nbit (Nxor a' a''))).
apply eqf_xorf. apply eqf_refl.
- apply eqf_sym. apply Nxor_semantics.
- apply eqf_sym. apply Nxor_semantics.
+ apply eqf_sym, Nxor_semantics.
+ apply eqf_sym, Nxor_semantics.
Qed.
(** Checking whether a number is odd, i.e.
@@ -370,18 +363,16 @@ Qed.
Lemma Nxor_bit0 :
forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a').
Proof.
- intros. rewrite <- Nbit0_correct. rewrite (Nxor_semantics a a' 0).
- unfold xorf. rewrite Nbit0_correct. rewrite Nbit0_correct. reflexivity.
+ intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' 0).
+ unfold xorf. rewrite Nbit0_correct, Nbit0_correct. reflexivity.
Qed.
Lemma Nxor_div2 :
forall a a':N, Ndiv2 (Nxor a a') = Nxor (Ndiv2 a) (Ndiv2 a').
Proof.
intros. apply Nbit_faithful. unfold eqf. intro.
- rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n).
- rewrite Ndiv2_correct.
- rewrite (Nxor_semantics a a' (S n)).
- unfold xorf. rewrite Ndiv2_correct. rewrite Ndiv2_correct.
+ rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
+ unfold xorf. rewrite 2! Ndiv2_correct.
reflexivity.
Qed.
@@ -389,8 +380,9 @@ Lemma Nneg_bit0 :
forall a a':N,
Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a').
Proof.
- intros. rewrite <- true_xorb. rewrite <- H. rewrite Nxor_bit0.
- rewrite xorb_assoc. rewrite xorb_nilpotent. rewrite xorb_false. reflexivity.
+ intros.
+ rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false.
+ reflexivity.
Qed.
Lemma Nneg_bit0_1 :
@@ -410,10 +402,9 @@ Lemma Nsame_bit0 :
forall (a a':N) (p:positive),
Nxor a a' = Npos (xO p) -> Nbit0 a = Nbit0 a'.
Proof.
- intros. rewrite <- (xorb_false (Nbit0 a)). cut (Nbit0 (Npos (xO p)) = false).
- intro. rewrite <- H0. rewrite <- H. rewrite Nxor_bit0. rewrite <- xorb_assoc.
- rewrite xorb_nilpotent. rewrite false_xorb. reflexivity.
- reflexivity.
+ intros. rewrite <- (xorb_false (Nbit0 a)).
+ assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity.
+ rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity.
Qed.
(** a lexicographic order on bits, starting from the lowest bit *)
@@ -434,42 +425,40 @@ Lemma Nbit0_less :
forall a a',
Nbit0 a = false -> Nbit0 a' = true -> Nless a a' = true.
Proof.
- intros. elim (Ndiscr (Nxor a a')). intro H1. elim H1. intros p H2. unfold Nless in |- *.
- rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity.
- intros. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H5.
- rewrite H in H5. rewrite H0 in H5. discriminate H5.
- rewrite H4. reflexivity.
- intro. simpl in |- *. rewrite H. rewrite H0. reflexivity.
- intro H1. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H2.
- rewrite H in H2. rewrite H0 in H2. discriminate H2.
- rewrite H1. reflexivity.
+ intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+ rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
+ assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+ rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
+ simpl. rewrite H, H0. reflexivity.
+ assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+ rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
Qed.
Lemma Nbit0_gt :
forall a a',
Nbit0 a = true -> Nbit0 a' = false -> Nless a a' = false.
Proof.
- intros. elim (Ndiscr (Nxor a a')). intro H1. elim H1. intros p H2. unfold Nless in |- *.
- rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity.
- intros. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H5.
- rewrite H in H5. rewrite H0 in H5. discriminate H5.
- rewrite H4. reflexivity.
- intro. simpl in |- *. rewrite H. rewrite H0. reflexivity.
- intro H1. unfold Nless in |- *. rewrite H1. reflexivity.
+ intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+ rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
+ assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+ rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
+ simpl. rewrite H, H0. reflexivity.
+ assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+ rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
Qed.
Lemma Nless_not_refl : forall a, Nless a a = false.
Proof.
- intro. unfold Nless in |- *. rewrite (Nxor_nilpotent a). reflexivity.
+ intro. unfold Nless. rewrite (Nxor_nilpotent a). reflexivity.
Qed.
Lemma Nless_def_1 :
forall a a', Nless (Ndouble a) (Ndouble a') = Nless a a'.
Proof.
- simple induction a. simple induction a'. reflexivity.
+ destruct a; destruct a'. reflexivity.
trivial.
- simple induction a'. unfold Nless in |- *. simpl in |- *. elim p; trivial.
- unfold Nless in |- *. simpl in |- *. intro. case (Pxor p p0). reflexivity.
+ unfold Nless. simpl. destruct p; trivial.
+ unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
trivial.
Qed.
@@ -477,10 +466,10 @@ Lemma Nless_def_2 :
forall a a',
Nless (Ndouble_plus_one a) (Ndouble_plus_one a') = Nless a a'.
Proof.
- simple induction a. simple induction a'. reflexivity.
+ destruct a; destruct a'. reflexivity.
trivial.
- simple induction a'. unfold Nless in |- *. simpl in |- *. elim p; trivial.
- unfold Nless in |- *. simpl in |- *. intro. case (Pxor p p0). reflexivity.
+ unfold Nless. simpl. destruct p; trivial.
+ unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
trivial.
Qed.
@@ -500,79 +489,71 @@ Qed.
Lemma Nless_z : forall a, Nless a N0 = false.
Proof.
- simple induction a. reflexivity.
- unfold Nless in |- *. intro. rewrite (Nxor_neutral_right (Npos p)). elim p; trivial.
+ induction a. reflexivity.
+ unfold Nless. rewrite (Nxor_neutral_right (Npos p)). induction p; trivial.
Qed.
Lemma N0_less_1 :
forall a, Nless N0 a = true -> {p : positive | a = Npos p}.
Proof.
- simple induction a. intro. discriminate H.
- intros. split with p. reflexivity.
+ destruct a. intros. discriminate.
+ intros. exists p. reflexivity.
Qed.
Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0.
Proof.
- simple induction a. trivial.
- unfold Nless in |- *. simpl in |- *.
- cut (forall p:positive, Nless_aux N0 (Npos p) p = false -> False).
- intros. elim (H p H0).
- simple induction p. intros. discriminate H0.
- intros. exact (H H0).
- intro. discriminate H.
+ induction a as [|p]; intro H. trivial.
+ elimtype False. induction p as [|p IHp|]; discriminate || simpl; auto using IHp.
Qed.
Lemma Nless_trans :
forall a a' a'',
Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
Proof.
- intro a. pattern a; apply N_ind_double.
- intros. case_eq (Nless N0 a''). trivial.
- intro H1. rewrite (N0_less_2 a'' H1) in H0. rewrite (Nless_z a') in H0. discriminate H0.
- intros a0 H a'. pattern a'; apply N_ind_double.
- intros. rewrite (Nless_z (Ndouble a0)) in H0. discriminate H0.
- intros a1 H0 a'' H1. rewrite (Nless_def_1 a0 a1) in H1.
- pattern a''; apply N_ind_double; clear a''.
- intro. rewrite (Nless_z (Ndouble a1)) in H2. discriminate H2.
- intros. rewrite (Nless_def_1 a1 a2) in H3. rewrite (Nless_def_1 a0 a2).
- exact (H a1 a2 H1 H3).
- intros. apply Nless_def_3.
- intros a1 H0 a'' H1. pattern a''; apply N_ind_double.
- intro. rewrite (Nless_z (Ndouble_plus_one a1)) in H2. discriminate H2.
- intros. rewrite (Nless_def_4 a1 a2) in H3. discriminate H3.
- intros. apply Nless_def_3.
- intros a0 H a'. pattern a'; apply N_ind_double.
- intros. rewrite (Nless_z (Ndouble_plus_one a0)) in H0. discriminate H0.
- intros. rewrite (Nless_def_4 a0 a1) in H1. discriminate H1.
- intros a1 H0 a'' H1. pattern a''; apply N_ind_double.
- intro. rewrite (Nless_z (Ndouble_plus_one a1)) in H2. discriminate H2.
- intros. rewrite (Nless_def_4 a1 a2) in H3. discriminate H3.
- rewrite (Nless_def_2 a0 a1) in H1. intros. rewrite (Nless_def_2 a1 a2) in H3.
- rewrite (Nless_def_2 a0 a2). exact (H a1 a2 H1 H3).
+ induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0.
+ destruct (Nless N0 a'') as []_eqn:Heqb. trivial.
+ rewrite (N0_less_2 a'' Heqb), (Nless_z a') in H0. discriminate H0.
+ induction a' as [|a' _|a' _] using N_ind_double.
+ rewrite (Nless_z (Ndouble a)) in H. discriminate H.
+ rewrite (Nless_def_1 a a') in H.
+ induction a'' using N_ind_double.
+ rewrite (Nless_z (Ndouble a')) in H0. discriminate H0.
+ rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a'').
+ exact (IHa _ _ H H0).
+ apply Nless_def_3.
+ induction a'' as [|a'' _|a'' _] using N_ind_double.
+ rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+ rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
+ apply Nless_def_3.
+ induction a' as [|a' _|a' _] using N_ind_double.
+ rewrite (Nless_z (Ndouble_plus_one a)) in H. discriminate H.
+ rewrite (Nless_def_4 a a') in H. discriminate H.
+ induction a'' using N_ind_double.
+ rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+ rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
+ rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H.
+ rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0).
Qed.
Lemma Nless_total :
forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
Proof.
- intro a.
- pattern a; apply N_rec_double; clear a.
- intro. case_eq (Nless N0 a'). intro H. left. left. auto.
- intro H. right. rewrite (N0_less_2 a' H). reflexivity.
- intros a0 H a'.
- pattern a'; apply N_rec_double; clear a'.
- case_eq (Nless N0 (Ndouble a0)). intro H0. left. right. auto.
- intro H0. right. exact (N0_less_2 _ H0).
- intros a1 H0. rewrite Nless_def_1. rewrite Nless_def_1. elim (H a1). intro H1.
- left. assumption.
- intro H1. right. rewrite H1. reflexivity.
- intros a1 H0. left. left. apply Nless_def_3.
- intros a0 H a'.
- pattern a'; apply N_rec_double; clear a'.
- left. right. case a0; reflexivity.
- intros a1 H0. left. right. apply Nless_def_3.
- intros a1 H0. rewrite Nless_def_2. rewrite Nless_def_2. elim (H a1). intro H1.
- left. assumption.
- intro H1. right. rewrite H1. reflexivity.
+ induction a using N_rec_double; intro a'.
+ destruct (Nless N0 a') as []_eqn:Heqb. left. left. auto.
+ right. rewrite (N0_less_2 a' Heqb). reflexivity.
+ induction a' as [|a' _|a' _] using N_rec_double.
+ destruct (Nless N0 (Ndouble a)) as []_eqn:Heqb. left. right. auto.
+ right. exact (N0_less_2 _ Heqb).
+ rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
+ left. assumption.
+ right. reflexivity.
+ left. left. apply Nless_def_3.
+ induction a' as [|a' _|a' _] using N_rec_double.
+ left. right. destruct a; reflexivity.
+ left. right. apply Nless_def_3.
+ rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->].
+ left. assumption.
+ right. reflexivity.
Qed.
(** Number of digits in a number *)
@@ -621,7 +602,7 @@ Proof.
induction n; intros.
rewrite (V0_eq _ bv); simpl; auto.
rewrite (VSn_eq _ _ bv); simpl.
-generalize (IHn (Vtail _ _ bv)); clear IHn.
+specialize IHn with (Vtail _ _ bv).
destruct (Vhead _ _ bv);
destruct (Bv2N n (Vtail bool n bv));
simpl; auto with arith.
@@ -701,7 +682,7 @@ Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
Proof.
intros.
unfold Blow.
-pattern bv at 1; rewrite (VSn_eq _ _ bv).
+rewrite (VSn_eq _ _ bv) at 1.
simpl.
destruct (Bv2N n (Vtail bool n bv)); simpl;
destruct (Vhead bool n bv); auto.
@@ -750,9 +731,9 @@ Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
Proof.
induction n.
intros.
-rewrite (V0_eq _ bv); rewrite (V0_eq _ bv'); simpl; auto.
+rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
intros.
-rewrite (VSn_eq _ _ bv); rewrite (VSn_eq _ _ bv'); simpl; auto.
+rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
rewrite IHn.
destruct (Vhead bool n bv); destruct (Vhead bool n bv');
destruct (Bv2N n (Vtail bool n bv)); destruct (Bv2N n (Vtail bool n bv')); simpl; auto.