diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 213 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 1135 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Pnat.v | 599 |
4 files changed, 1018 insertions, 931 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index e11194a5d9..edaa3130f4 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -8,198 +8,205 @@ (*i $Id$ i*) -Require BinPos. +Require Import BinPos. (**********************************************************************) (** Binary natural numbers *) -Inductive entier: Set := Nul : entier | Pos : positive -> entier. +Inductive N : Set := + | N0 : N + | Npos : positive -> N. (** Declare binding key for scope positive_scope *) -Delimits Scope N_scope with N. +Delimit Scope N_scope with N. (** Automatically open scope N_scope for the constructors of N *) -Bind Scope N_scope with entier. -Arguments Scope Pos [ N_scope ]. +Bind Scope N_scope with N. +Arguments Scope Npos [N_scope]. Open Local Scope N_scope. (** Operation x -> 2*x+1 *) -Definition Un_suivi_de := [x] - Cases x of Nul => (Pos xH) | (Pos p) => (Pos (xI p)) end. +Definition Ndouble_plus_one x := + match x with + | N0 => Npos 1%positive + | Npos p => Npos (xI p) + end. (** Operation x -> 2*x *) -Definition Zero_suivi_de := - [n] Cases n of Nul => Nul | (Pos p) => (Pos (xO p)) end. +Definition Ndouble n := match n with + | N0 => N0 + | Npos p => Npos (xO p) + end. (** Successor *) -Definition Nsucc := - [n] Cases n of Nul => (Pos xH) | (Pos p) => (Pos (add_un p)) end. +Definition Nsucc n := + match n with + | N0 => Npos 1%positive + | Npos p => Npos (Psucc p) + end. (** Addition *) -Definition Nplus := [n,m] - Cases n m of - | Nul _ => m - | _ Nul => n - | (Pos p) (Pos q) => (Pos (add p q)) +Definition Nplus n m := + match n, m with + | N0, _ => m + | _, N0 => n + | Npos p, Npos q => Npos (p + q)%positive end. -V8Infix "+" Nplus : N_scope. +Infix "+" := Nplus : N_scope. (** Multiplication *) -Definition Nmult := [n,m] - Cases n m of - | Nul _ => Nul - | _ Nul => Nul - | (Pos p) (Pos q) => (Pos (times p q)) +Definition Nmult n m := + match n, m with + | N0, _ => N0 + | _, N0 => N0 + | Npos p, Npos q => Npos (p * q)%positive end. -V8Infix "*" Nmult : N_scope. +Infix "*" := Nmult : N_scope. (** Order *) -Definition Ncompare := [n,m] - Cases n m of - | Nul Nul => EGAL - | Nul (Pos m') => INFERIEUR - | (Pos n') Nul => SUPERIEUR - | (Pos n') (Pos m') => (compare n' m' EGAL) +Definition Ncompare n m := + match n, m with + | N0, N0 => Eq + | N0, Npos m' => Lt + | Npos n', N0 => Gt + | Npos n', Npos m' => (n' ?= m')%positive Eq end. -V8Infix "?=" Ncompare (at level 70, no associativity) : N_scope. +Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. (** Peano induction on binary natural numbers *) -Theorem Nind : (P:(entier ->Prop)) - (P Nul) ->((n:entier)(P n) ->(P (Nsucc n))) ->(n:entier)(P n). +Theorem Nind : + forall P:N -> Prop, + P N0 -> (forall n:N, P n -> P (Nsucc n)) -> forall n:N, P n. Proof. -NewDestruct n. - Assumption. - Apply Pind with P := [p](P (Pos p)). -Exact (H0 Nul H). -Intro p'; Exact (H0 (Pos p')). +destruct n. + assumption. + apply Pind with (P := fun p => P (Npos p)). +exact (H0 N0 H). +intro p'; exact (H0 (Npos p')). Qed. (** Properties of addition *) -Theorem Nplus_0_l : (n:entier)(Nplus Nul n)=n. +Theorem Nplus_0_l : forall n:N, N0 + n = n. Proof. -Reflexivity. +reflexivity. Qed. -Theorem Nplus_0_r : (n:entier)(Nplus n Nul)=n. +Theorem Nplus_0_r : forall n:N, n + N0 = n. Proof. -NewDestruct n; Reflexivity. +destruct n; reflexivity. Qed. -Theorem Nplus_comm : (n,m:entier)(Nplus n m)=(Nplus m n). +Theorem Nplus_comm : forall n m:N, n + m = m + n. Proof. -Intros. -NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. -Rewrite add_sym; Reflexivity. +intros. +destruct n; destruct m; simpl in |- *; try reflexivity. +rewrite Pplus_comm; reflexivity. Qed. -Theorem Nplus_assoc : - (n,m,p:entier)(Nplus n (Nplus m p))=(Nplus (Nplus n m) p). +Theorem Nplus_assoc : forall n m p:N, n + (m + p) = n + m + p. Proof. -Intros. -NewDestruct n; Try Reflexivity. -NewDestruct m; Try Reflexivity. -NewDestruct p; Try Reflexivity. -Simpl; Rewrite add_assoc; Reflexivity. +intros. +destruct n; try reflexivity. +destruct m; try reflexivity. +destruct p; try reflexivity. +simpl in |- *; rewrite Pplus_assoc; reflexivity. Qed. -Theorem Nplus_succ : (n,m:entier)(Nplus (Nsucc n) m)=(Nsucc (Nplus n m)). +Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m). Proof. -NewDestruct n; NewDestruct m. - Simpl; Reflexivity. - Unfold Nsucc Nplus; Rewrite <- ZL12bis; Reflexivity. - Simpl; Reflexivity. - Simpl; Rewrite ZL14bis; Reflexivity. +destruct n; destruct m. + simpl in |- *; reflexivity. + unfold Nsucc, Nplus in |- *; rewrite <- Pplus_one_succ_l; reflexivity. + simpl in |- *; reflexivity. + simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. Qed. -Theorem Nsucc_inj : (n,m:entier)(Nsucc n)=(Nsucc m)->n=m. +Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m. Proof. -NewDestruct n; NewDestruct m; Simpl; Intro H; - Reflexivity Orelse Injection H; Clear H; Intro H. - Symmetry in H; Contradiction add_un_not_un with p. - Contradiction add_un_not_un with p. - Rewrite add_un_inj with 1:=H; Reflexivity. +destruct n; destruct m; simpl in |- *; intro H; reflexivity || injection H; + clear H; intro H. + symmetry in H; contradiction Psucc_not_one with p. + contradiction Psucc_not_one with p. + rewrite Psucc_inj with (1 := H); reflexivity. Qed. -Theorem Nplus_reg_l : (n,m,p:entier)(Nplus n m)=(Nplus n p)->m=p. +Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p. Proof. -Intro n; Pattern n; Apply Nind; Clear n; Simpl. - Trivial. - Intros n IHn m p H0; Do 2 Rewrite Nplus_succ in H0. - Apply IHn; Apply Nsucc_inj; Assumption. +intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *. + trivial. + intros n IHn m p H0; do 2 rewrite Nplus_succ in H0. + apply IHn; apply Nsucc_inj; assumption. Qed. (** Properties of multiplication *) -Theorem Nmult_1_l : (n:entier)(Nmult (Pos xH) n)=n. +Theorem Nmult_1_l : forall n:N, Npos 1%positive * n = n. Proof. -NewDestruct n; Reflexivity. +destruct n; reflexivity. Qed. -Theorem Nmult_1_r : (n:entier)(Nmult n (Pos xH))=n. +Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n. Proof. -NewDestruct n; Simpl; Try Reflexivity. -Rewrite times_x_1; Reflexivity. +destruct n; simpl in |- *; try reflexivity. +rewrite Pmult_1_r; reflexivity. Qed. -Theorem Nmult_comm : (n,m:entier)(Nmult n m)=(Nmult m n). +Theorem Nmult_comm : forall n m:N, n * m = m * n. Proof. -Intros. -NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. -Rewrite times_sym; Reflexivity. +intros. +destruct n; destruct m; simpl in |- *; try reflexivity. +rewrite Pmult_comm; reflexivity. Qed. -Theorem Nmult_assoc : - (n,m,p:entier)(Nmult n (Nmult m p))=(Nmult (Nmult n m) p). +Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p. Proof. -Intros. -NewDestruct n; Try Reflexivity. -NewDestruct m; Try Reflexivity. -NewDestruct p; Try Reflexivity. -Simpl; Rewrite times_assoc; Reflexivity. +intros. +destruct n; try reflexivity. +destruct m; try reflexivity. +destruct p; try reflexivity. +simpl in |- *; rewrite Pmult_assoc; reflexivity. Qed. -Theorem Nmult_plus_distr_r : - (n,m,p:entier)(Nmult (Nplus n m) p)=(Nplus (Nmult n p) (Nmult m p)). +Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p. Proof. -Intros. -NewDestruct n; Try Reflexivity. -NewDestruct m; NewDestruct p; Try Reflexivity. -Simpl; Rewrite times_add_distr_l; Reflexivity. +intros. +destruct n; try reflexivity. +destruct m; destruct p; try reflexivity. +simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity. Qed. -Theorem Nmult_reg_r : (n,m,p:entier) ~p=Nul->(Nmult n p)=(Nmult m p) -> n=m. +Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m. Proof. -NewDestruct p; Intros Hp H. -Contradiction Hp; Reflexivity. -NewDestruct n; NewDestruct m; Reflexivity Orelse Try Discriminate H. -Injection H; Clear H; Intro H; Rewrite simpl_times_r with 1:=H; Reflexivity. +destruct p; intros Hp H. +contradiction Hp; reflexivity. +destruct n; destruct m; reflexivity || (try discriminate H). +injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity. Qed. -Theorem Nmult_0_l : (n:entier) (Nmult Nul n) = Nul. +Theorem Nmult_0_l : forall n:N, N0 * n = N0. Proof. -Reflexivity. +reflexivity. Qed. (** Properties of comparison *) -Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m. +Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m. Proof. -NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H; - Reflexivity Orelse Try Discriminate H. - Rewrite (compare_convert_EGAL n m H); Reflexivity. +destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H; + reflexivity || (try discriminate H). + rewrite (Pcompare_Eq_eq n m H); reflexivity. Qed. - diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index b5fa6694ba..6ef509d064 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -14,202 +14,212 @@ (** Original development by Pierre Crégut, CNET, Lannion, France *) Inductive positive : Set := - xI : positive -> positive -| xO : positive -> positive -| xH : positive. + | xI : positive -> positive + | xO : positive -> positive + | xH : positive. (** Declare binding key for scope positive_scope *) -Delimits Scope positive_scope with positive. +Delimit Scope positive_scope with positive. (** Automatically open scope positive_scope for type positive, xO and xI *) Bind Scope positive_scope with positive. -Arguments Scope xO [ positive_scope ]. -Arguments Scope xI [ positive_scope ]. +Arguments Scope xO [positive_scope]. +Arguments Scope xI [positive_scope]. (** Successor *) -Fixpoint add_un [x:positive]:positive := - Cases x of - (xI x') => (xO (add_un x')) - | (xO x') => (xI x') - | xH => (xO xH) +Fixpoint Psucc (x:positive) : positive := + match x with + | xI x' => xO (Psucc x') + | xO x' => xI x' + | xH => xO xH end. (** Addition *) -Fixpoint add [x:positive]:positive -> positive := [y:positive] - Cases x y of - | (xI x') (xI y') => (xO (add_carry x' y')) - | (xI x') (xO y') => (xI (add x' y')) - | (xI x') xH => (xO (add_un x')) - | (xO x') (xI y') => (xI (add x' y')) - | (xO x') (xO y') => (xO (add x' y')) - | (xO x') xH => (xI x') - | xH (xI y') => (xO (add_un y')) - | xH (xO y') => (xI y') - | xH xH => (xO xH) +Fixpoint Pplus (x y:positive) {struct x} : positive := + match x, y with + | xI x', xI y' => xO (Pplus_carry x' y') + | xI x', xO y' => xI (Pplus x' y') + | xI x', xH => xO (Psucc x') + | xO x', xI y' => xI (Pplus x' y') + | xO x', xO y' => xO (Pplus x' y') + | xO x', xH => xI x' + | xH, xI y' => xO (Psucc y') + | xH, xO y' => xI y' + | xH, xH => xO xH end -with add_carry [x:positive]:positive -> positive := [y:positive] - Cases x y of - | (xI x') (xI y') => (xI (add_carry x' y')) - | (xI x') (xO y') => (xO (add_carry x' y')) - | (xI x') xH => (xI (add_un x')) - | (xO x') (xI y') => (xO (add_carry x' y')) - | (xO x') (xO y') => (xI (add x' y')) - | (xO x') xH => (xO (add_un x')) - | xH (xI y') => (xI (add_un y')) - | xH (xO y') => (xO (add_un y')) - | xH xH => (xI xH) + + with Pplus_carry (x y:positive) {struct x} : positive := + match x, y with + | xI x', xI y' => xI (Pplus_carry x' y') + | xI x', xO y' => xO (Pplus_carry x' y') + | xI x', xH => xI (Psucc x') + | xO x', xI y' => xO (Pplus_carry x' y') + | xO x', xO y' => xI (Pplus x' y') + | xO x', xH => xO (Psucc x') + | xH, xI y' => xI (Psucc y') + | xH, xO y' => xO (Psucc y') + | xH, xH => xI xH end. -V7only [Notation "x + y" := (add x y) : positive_scope.]. -V8Infix "+" add : positive_scope. +Infix "+" := Pplus : positive_scope. Open Local Scope positive_scope. (** From binary positive numbers to Peano natural numbers *) -Fixpoint positive_to_nat [x:positive]:nat -> nat := - [pow2:nat] - Cases x of - (xI x') => (plus pow2 (positive_to_nat x' (plus pow2 pow2))) - | (xO x') => (positive_to_nat x' (plus pow2 pow2)) - | xH => pow2 - end. +Fixpoint Pmult_nat (x:positive) (pow2:nat) {struct x} : nat := + match x with + | xI x' => (pow2 + Pmult_nat x' (pow2 + pow2))%nat + | xO x' => Pmult_nat x' (pow2 + pow2)%nat + | xH => pow2 + end. -Definition convert := [x:positive] (positive_to_nat x (S O)). +Definition nat_of_P (x:positive) := Pmult_nat x 1. (** From Peano natural numbers to binary positive numbers *) -Fixpoint anti_convert [n:nat]: positive := - Cases n of - O => xH - | (S x') => (add_un (anti_convert x')) - end. +Fixpoint P_of_succ_nat (n:nat) : positive := + match n with + | O => xH + | S x' => Psucc (P_of_succ_nat x') + end. (** Operation x -> 2*x-1 *) -Fixpoint double_moins_un [x:positive]:positive := - Cases x of - (xI x') => (xI (xO x')) - | (xO x') => (xI (double_moins_un x')) - | xH => xH - end. +Fixpoint Pdouble_minus_one (x:positive) : positive := + match x with + | xI x' => xI (xO x') + | xO x' => xI (Pdouble_minus_one x') + | xH => xH + end. (** Predecessor *) -Definition sub_un := [x:positive] - Cases x of - (xI x') => (xO x') - | (xO x') => (double_moins_un x') - | xH => xH - end. +Definition Ppred (x:positive) := + match x with + | xI x' => xO x' + | xO x' => Pdouble_minus_one x' + | xH => xH + end. (** An auxiliary type for subtraction *) -Inductive positive_mask: Set := - IsNul : positive_mask - | IsPos : positive -> positive_mask - | IsNeg : positive_mask. +Inductive positive_mask : Set := + | IsNul : positive_mask + | IsPos : positive -> positive_mask + | IsNeg : positive_mask. (** Operation x -> 2*x+1 *) -Definition Un_suivi_de_mask := [x:positive_mask] - Cases x of IsNul => (IsPos xH) | IsNeg => IsNeg | (IsPos p) => (IsPos (xI p)) end. +Definition Pdouble_plus_one_mask (x:positive_mask) := + match x with + | IsNul => IsPos xH + | IsNeg => IsNeg + | IsPos p => IsPos (xI p) + end. (** Operation x -> 2*x *) -Definition Zero_suivi_de_mask := [x:positive_mask] - Cases x of IsNul => IsNul | IsNeg => IsNeg | (IsPos p) => (IsPos (xO p)) end. +Definition Pdouble_mask (x:positive_mask) := + match x with + | IsNul => IsNul + | IsNeg => IsNeg + | IsPos p => IsPos (xO p) + end. (** Operation x -> 2*x-2 *) -Definition double_moins_deux := - [x:positive] Cases x of - (xI x') => (IsPos (xO (xO x'))) - | (xO x') => (IsPos (xO (double_moins_un x'))) - | xH => IsNul - end. +Definition Pdouble_minus_two (x:positive) := + match x with + | xI x' => IsPos (xO (xO x')) + | xO x' => IsPos (xO (Pdouble_minus_one x')) + | xH => IsNul + end. (** Subtraction of binary positive numbers into a positive numbers mask *) -Fixpoint sub_pos[x,y:positive]:positive_mask := - Cases x y of - | (xI x') (xI y') => (Zero_suivi_de_mask (sub_pos x' y')) - | (xI x') (xO y') => (Un_suivi_de_mask (sub_pos x' y')) - | (xI x') xH => (IsPos (xO x')) - | (xO x') (xI y') => (Un_suivi_de_mask (sub_neg x' y')) - | (xO x') (xO y') => (Zero_suivi_de_mask (sub_pos x' y')) - | (xO x') xH => (IsPos (double_moins_un x')) - | xH xH => IsNul - | xH _ => IsNeg +Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask := + match x, y with + | xI x', xI y' => Pdouble_mask (Pminus_mask x' y') + | xI x', xO y' => Pdouble_plus_one_mask (Pminus_mask x' y') + | xI x', xH => IsPos (xO x') + | xO x', xI y' => Pdouble_plus_one_mask (Pminus_mask_carry x' y') + | xO x', xO y' => Pdouble_mask (Pminus_mask x' y') + | xO x', xH => IsPos (Pdouble_minus_one x') + | xH, xH => IsNul + | xH, _ => IsNeg end -with sub_neg [x,y:positive]:positive_mask := - Cases x y of - (xI x') (xI y') => (Un_suivi_de_mask (sub_neg x' y')) - | (xI x') (xO y') => (Zero_suivi_de_mask (sub_pos x' y')) - | (xI x') xH => (IsPos (double_moins_un x')) - | (xO x') (xI y') => (Zero_suivi_de_mask (sub_neg x' y')) - | (xO x') (xO y') => (Un_suivi_de_mask (sub_neg x' y')) - | (xO x') xH => (double_moins_deux x') - | xH _ => IsNeg + + with Pminus_mask_carry (x y:positive) {struct y} : positive_mask := + match x, y with + | xI x', xI y' => Pdouble_plus_one_mask (Pminus_mask_carry x' y') + | xI x', xO y' => Pdouble_mask (Pminus_mask x' y') + | xI x', xH => IsPos (Pdouble_minus_one x') + | xO x', xI y' => Pdouble_mask (Pminus_mask_carry x' y') + | xO x', xO y' => Pdouble_plus_one_mask (Pminus_mask_carry x' y') + | xO x', xH => Pdouble_minus_two x' + | xH, _ => IsNeg end. (** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) -Definition true_sub := [x,y:positive] - Cases (sub_pos x y) of (IsPos z) => z | _ => xH end. +Definition Pminus (x y:positive) := + match Pminus_mask x y with + | IsPos z => z + | _ => xH + end. -V8Infix "-" true_sub : positive_scope. +Infix "-" := Pminus : positive_scope. (** Multiplication on binary positive numbers *) -Fixpoint times [x:positive] : positive -> positive:= - [y:positive] - Cases x of - (xI x') => (add y (xO (times x' y))) - | (xO x') => (xO (times x' y)) +Fixpoint Pmult (x y:positive) {struct x} : positive := + match x with + | xI x' => y + xO (Pmult x' y) + | xO x' => xO (Pmult x' y) | xH => y end. -V8Infix "*" times : positive_scope. +Infix "*" := Pmult : positive_scope. (** Division by 2 rounded below but for 1 *) -Definition Zdiv2_pos := - [z:positive]Cases z of xH => xH - | (xO p) => p - | (xI p) => p - end. +Definition Pdiv2 (z:positive) := + match z with + | xH => xH + | xO p => p + | xI p => p + end. -V8Infix "/" Zdiv2_pos : positive_scope. +Infix "/" := Pdiv2 : positive_scope. (** Comparison on binary positive numbers *) -Fixpoint compare [x,y:positive]: relation -> relation := - [r:relation] - Cases x y of - | (xI x') (xI y') => (compare x' y' r) - | (xI x') (xO y') => (compare x' y' SUPERIEUR) - | (xI x') xH => SUPERIEUR - | (xO x') (xI y') => (compare x' y' INFERIEUR) - | (xO x') (xO y') => (compare x' y' r) - | (xO x') xH => SUPERIEUR - | xH (xI y') => INFERIEUR - | xH (xO y') => INFERIEUR - | xH xH => r +Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := + match x, y with + | xI x', xI y' => Pcompare x' y' r + | xI x', xO y' => Pcompare x' y' Gt + | xI x', xH => Gt + | xO x', xI y' => Pcompare x' y' Lt + | xO x', xO y' => Pcompare x' y' r + | xO x', xH => Gt + | xH, xI y' => Lt + | xH, xO y' => Lt + | xH, xH => r end. -V8Infix "?=" compare (at level 70, no associativity) : positive_scope. +Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. (**********************************************************************) (** Miscellaneous properties of binary positive numbers *) -Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH). +Lemma ZL11 : forall p:positive, p = xH \/ p <> xH. Proof. -Intros x;Case x;Intros; (Left;Reflexivity) Orelse (Right;Discriminate). +intros x; case x; intros; (left; reflexivity) || (right; discriminate). Qed. (**********************************************************************) @@ -217,72 +227,78 @@ Qed. (** Specification of [xI] in term of [Psucc] and [xO] *) -Lemma xI_add_un_xO : (x:positive)(xI x) = (add_un (xO x)). +Lemma xI_succ_xO : forall p:positive, xI p = Psucc (xO p). Proof. -Reflexivity. +reflexivity. Qed. -Lemma add_un_discr : (x:positive)x<>(add_un x). +Lemma Psucc_discr : forall p:positive, p <> Psucc p. Proof. -Intro x; NewDestruct x; Discriminate. +intro x; destruct x as [p| p| ]; discriminate. Qed. (** Successor and double *) -Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x). +Lemma Psucc_o_double_minus_one_eq_xO : + forall p:positive, Psucc (Pdouble_minus_one p) = xO p. Proof. -Intro x; NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity. +intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx; + reflexivity. Qed. -Lemma double_moins_un_add_un_xI : - (x:positive)(double_moins_un (add_un x))=(xI x). +Lemma Pdouble_minus_one_o_succ_eq_xI : + forall p:positive, Pdouble_minus_one (Psucc p) = xI p. Proof. -Intro x;NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity. +intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx; + reflexivity. Qed. -Lemma ZL1: (y:positive)(xO (add_un y)) = (add_un (add_un (xO y))). +Lemma xO_succ_permute : + forall p:positive, xO (Psucc p) = Psucc (Psucc (xO p)). Proof. -Intro y; Induction y; Simpl; Auto. +intro y; induction y as [y Hrecy| y Hrecy| ]; simpl in |- *; auto. Qed. -Lemma double_moins_un_xO_discr : (x:positive)(double_moins_un x)<>(xO x). +Lemma double_moins_un_xO_discr : + forall p:positive, Pdouble_minus_one p <> xO p. Proof. -Intro x; NewDestruct x; Discriminate. +intro x; destruct x as [p| p| ]; discriminate. Qed. (** Successor and predecessor *) -Lemma add_un_not_un : (x:positive) (add_un x) <> xH. +Lemma Psucc_not_one : forall p:positive, Psucc p <> xH. Proof. -Intro x; NewDestruct x as [x|x|]; Discriminate. +intro x; destruct x as [x| x| ]; discriminate. Qed. -Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x. +Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p. Proof. -(Intro x; NewDestruct x as [p|p|]; [Idtac | Idtac | Simpl;Auto]); -(NewInduction p as [p IHp||]; [Idtac | Reflexivity | Reflexivity ]); -Simpl; Simpl in IHp; Try Rewrite <- IHp; Reflexivity. +intro x; destruct x as [p| p| ]; [ idtac | idtac | simpl in |- *; auto ]; + (induction p as [p IHp| | ]; [ idtac | reflexivity | reflexivity ]); + simpl in |- *; simpl in IHp; try rewrite <- IHp; reflexivity. Qed. -Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x. +Lemma Psucc_pred : forall p:positive, p = xH \/ Psucc (Ppred p) = p. Proof. -Intro x; Induction x; [ - Simpl; Auto -| Simpl; Intros;Right;Apply is_double_moins_un -| Auto ]. +intro x; induction x as [x Hrecx| x Hrecx| ]; + [ simpl in |- *; auto + | simpl in |- *; intros; right; apply Psucc_o_double_minus_one_eq_xO + | auto ]. Qed. (** Injectivity of successor *) -Lemma add_un_inj : (x,y:positive) (add_un x)=(add_un y) -> x=y. +Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q. Proof. -Intro x;NewInduction x; Intro y; NewDestruct y as [y|y|]; Simpl; - Intro H; Discriminate H Orelse Try (Injection H; Clear H; Intro H). -Rewrite (IHx y H); Reflexivity. -Absurd (add_un x)=xH; [ Apply add_un_not_un | Assumption ]. -Apply f_equal with 1:=H; Assumption. -Absurd (add_un y)=xH; [ Apply add_un_not_un | Symmetry; Assumption ]. -Reflexivity. +intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H; + discriminate H || (try (injection H; clear H; intro H)). +rewrite (IHx y H); reflexivity. +absurd (Psucc x = xH); [ apply Psucc_not_one | assumption ]. +apply f_equal with (1 := H); assumption. +absurd (Psucc y = xH); + [ apply Psucc_not_one | symmetry in |- *; assumption ]. +reflexivity. Qed. (**********************************************************************) @@ -290,605 +306,656 @@ Qed. (** Specification of [Psucc] in term of [Pplus] *) -Lemma ZL12: (q:positive) (add_un q) = (add q xH). +Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + xH. Proof. -Intro q; NewDestruct q; Reflexivity. +intro q; destruct q as [p| p| ]; reflexivity. Qed. -Lemma ZL12bis: (q:positive) (add_un q) = (add xH q). +Lemma Pplus_one_succ_l : forall p:positive, Psucc p = xH + p. Proof. -Intro q; NewDestruct q; Reflexivity. +intro q; destruct q as [p| p| ]; reflexivity. Qed. (** Specification of [Pplus_carry] *) -Theorem ZL13: (x,y:positive)(add_carry x y) = (add_un (add x y)). +Theorem Pplus_carry_spec : + forall p q:positive, Pplus_carry p q = Psucc (p + q). Proof. -(Intro x; NewInduction x as [p IHp|p IHp|];Intro y; NewDestruct y;Simpl;Auto); - Rewrite IHp; Auto. +intro x; induction x as [p IHp| p IHp| ]; intro y; + [ destruct y as [p0| p0| ] + | destruct y as [p0| p0| ] + | destruct y as [p| p| ] ]; simpl in |- *; auto; rewrite IHp; + auto. Qed. (** Commutativity *) -Theorem add_sym : (x,y:positive) (add x y) = (add y x). +Theorem Pplus_comm : forall p q:positive, p + q = q + p. Proof. -Intro x; NewInduction x as [p IHp|p IHp|];Intro y; NewDestruct y;Simpl;Auto; - Try Do 2 Rewrite ZL13; Rewrite IHp;Auto. +intro x; induction x as [p IHp| p IHp| ]; intro y; + [ destruct y as [p0| p0| ] + | destruct y as [p0| p0| ] + | destruct y as [p| p| ] ]; simpl in |- *; auto; + try do 2 rewrite Pplus_carry_spec; rewrite IHp; auto. Qed. (** Permutation of [Pplus] and [Psucc] *) -Theorem ZL14: (x,y:positive)(add x (add_un y)) = (add_un (add x y)). +Theorem Pplus_succ_permute_r : + forall p q:positive, p + Psucc q = Psucc (p + q). Proof. -Intro x; NewInduction x as [p IHp|p IHp|];Intro y; NewDestruct y;Simpl;Auto; [ - Rewrite ZL13; Rewrite IHp; Auto -| Rewrite ZL13; Auto -| NewDestruct p;Simpl;Auto -| Rewrite IHp;Auto -| NewDestruct p;Simpl;Auto ]. +intro x; induction x as [p IHp| p IHp| ]; intro y; + [ destruct y as [p0| p0| ] + | destruct y as [p0| p0| ] + | destruct y as [p| p| ] ]; simpl in |- *; auto; + [ rewrite Pplus_carry_spec; rewrite IHp; auto + | rewrite Pplus_carry_spec; auto + | destruct p; simpl in |- *; auto + | rewrite IHp; auto + | destruct p; simpl in |- *; auto ]. Qed. -Theorem ZL14bis: (x,y:positive)(add (add_un x) y) = (add_un (add x y)). +Theorem Pplus_succ_permute_l : + forall p q:positive, Psucc p + q = Psucc (p + q). Proof. -Intros x y; Rewrite add_sym; Rewrite add_sym with x:=x; Apply ZL14. +intros x y; rewrite Pplus_comm; rewrite Pplus_comm with (p := x); + apply Pplus_succ_permute_r. Qed. -Theorem ZL15: (q,z:positive) ~z=xH -> (add_carry q (sub_un z)) = (add q z). +Theorem Pplus_carry_pred_eq_plus : + forall p q:positive, q <> xH -> Pplus_carry p (Ppred q) = p + q. Proof. -Intros q z H; Elim (add_sub_one z); [ - Intro;Absurd z=xH;Auto -| Intros E;Pattern 2 z ;Rewrite <- E; Rewrite ZL14; Rewrite ZL13; Trivial ]. +intros q z H; elim (Psucc_pred z); + [ intro; absurd (z = xH); auto + | intros E; pattern z at 2 in |- *; rewrite <- E; + rewrite Pplus_succ_permute_r; rewrite Pplus_carry_spec; + trivial ]. Qed. (** No neutral for addition on strictly positive numbers *) -Lemma add_no_neutral : (x,y:positive) ~(add y x)=x. +Lemma Pplus_no_neutral : forall p q:positive, q + p <> p. Proof. -Intro x;NewInduction x; Intro y; NewDestruct y as [y|y|]; Simpl; Intro H; - Discriminate H Orelse Injection H; Clear H; Intro H; Apply (IHx y H). +intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H; + discriminate H || injection H; clear H; intro H; apply (IHx y H). Qed. -Lemma add_carry_not_add_un : (x,y:positive) ~(add_carry y x)=(add_un x). +Lemma Pplus_carry_no_neutral : + forall p q:positive, Pplus_carry q p <> Psucc p. Proof. -Intros x y H; Absurd (add y x)=x; - [ Apply add_no_neutral - | Apply add_un_inj; Rewrite <- ZL13; Assumption ]. +intros x y H; absurd (y + x = x); + [ apply Pplus_no_neutral + | apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption ]. Qed. (** Simplification *) -Lemma add_carry_add : - (x,y,z,t:positive) (add_carry x z)=(add_carry y t) -> (add x z)=(add y t). +Lemma Pplus_carry_plus : + forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s. Proof. -Intros x y z t H; Apply add_un_inj; Do 2 Rewrite <- ZL13; Assumption. +intros x y z t H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec; + assumption. Qed. -Lemma simpl_add_r : (x,y,z:positive) (add x z)=(add y z) -> x=y. +Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q. Proof. -Intros x y z; Generalize x y; Clear x y. -NewInduction z as [z|z|]. - NewDestruct x as [x|x|]; Intro y; NewDestruct y as [y|y|]; Simpl; Intro H; - Discriminate H Orelse Try (Injection H; Clear H; Intro H). - Rewrite IHz with 1:=(add_carry_add ? ? ? ? H); Reflexivity. - Absurd (add_carry x z)=(add_un z); - [ Apply add_carry_not_add_un | Assumption ]. - Rewrite IHz with 1:=H; Reflexivity. - Symmetry in H; Absurd (add_carry y z)=(add_un z); - [ Apply add_carry_not_add_un | Assumption ]. - Reflexivity. - NewDestruct x as [x|x|]; Intro y; NewDestruct y as [y|y|]; Simpl; Intro H; - Discriminate H Orelse Try (Injection H; Clear H; Intro H). - Rewrite IHz with 1:=H; Reflexivity. - Absurd (add x z)=z; [ Apply add_no_neutral | Assumption ]. - Rewrite IHz with 1:=H; Reflexivity. - Symmetry in H; Absurd y+z=z; [ Apply add_no_neutral | Assumption ]. - Reflexivity. - Intros H x y; Apply add_un_inj; Do 2 Rewrite ZL12; Assumption. +intros x y z; generalize x y; clear x y. +induction z as [z| z| ]. + destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *; + intro H; discriminate H || (try (injection H; clear H; intro H)). + rewrite IHz with (1 := Pplus_carry_plus _ _ _ _ H); reflexivity. + absurd (Pplus_carry x z = Psucc z); + [ apply Pplus_carry_no_neutral | assumption ]. + rewrite IHz with (1 := H); reflexivity. + symmetry in H; absurd (Pplus_carry y z = Psucc z); + [ apply Pplus_carry_no_neutral | assumption ]. + reflexivity. + destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *; + intro H; discriminate H || (try (injection H; clear H; intro H)). + rewrite IHz with (1 := H); reflexivity. + absurd (x + z = z); [ apply Pplus_no_neutral | assumption ]. + rewrite IHz with (1 := H); reflexivity. + symmetry in H; absurd (y + z = z); + [ apply Pplus_no_neutral | assumption ]. + reflexivity. + intros H x y; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption. Qed. -Lemma simpl_add_l : (x,y,z:positive) (add x y)=(add x z) -> y=z. +Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r. Proof. -Intros x y z H;Apply simpl_add_r with z:=x; - Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Assumption. +intros x y z H; apply Pplus_reg_r with (r := x); + rewrite Pplus_comm with (p := z); rewrite Pplus_comm with (p := y); + assumption. Qed. -Lemma simpl_add_carry_r : - (x,y,z:positive) (add_carry x z)=(add_carry y z) -> x=y. +Lemma Pplus_carry_reg_r : + forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q. Proof. -Intros x y z H; Apply simpl_add_r with z:=z; Apply add_carry_add; Assumption. +intros x y z H; apply Pplus_reg_r with (r := z); apply Pplus_carry_plus; + assumption. Qed. -Lemma simpl_add_carry_l : - (x,y,z:positive) (add_carry x y)=(add_carry x z) -> y=z. +Lemma Pplus_carry_reg_l : + forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r. Proof. -Intros x y z H;Apply simpl_add_r with z:=x; -Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Apply add_carry_add; -Assumption. +intros x y z H; apply Pplus_reg_r with (r := x); + rewrite Pplus_comm with (p := z); rewrite Pplus_comm with (p := y); + apply Pplus_carry_plus; assumption. Qed. (** Addition on positive is associative *) -Theorem add_assoc: (x,y,z:positive)(add x (add y z)) = (add (add x y) z). -Proof. -Intros x y; Generalize x; Clear x. -NewInduction y as [y|y|]; Intro x. - NewDestruct x as [x|x|]; - Intro z; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13; - Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse - Repeat Apply f_equal with A:=positive; Apply IHy. - NewDestruct x as [x|x|]; - Intro z; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13; - Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse - Repeat Apply f_equal with A:=positive; Apply IHy. - Intro z; Rewrite add_sym with x:=xH; Do 2 Rewrite <- ZL12; Rewrite ZL14bis; Rewrite ZL14; Reflexivity. +Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r. +Proof. +intros x y; generalize x; clear x. +induction y as [y| y| ]; intro x. + destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *; + repeat rewrite Pplus_carry_spec; repeat rewrite Pplus_succ_permute_r; + repeat rewrite Pplus_succ_permute_l; + reflexivity || (repeat apply f_equal with (A := positive)); + apply IHy. + destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *; + repeat rewrite Pplus_carry_spec; repeat rewrite Pplus_succ_permute_r; + repeat rewrite Pplus_succ_permute_l; + reflexivity || (repeat apply f_equal with (A := positive)); + apply IHy. + intro z; rewrite Pplus_comm with (p := xH); + do 2 rewrite <- Pplus_one_succ_r; rewrite Pplus_succ_permute_l; + rewrite Pplus_succ_permute_r; reflexivity. Qed. (** Commutation of addition with the double of a positive number *) -Lemma add_xI_double_moins_un : - (p,q:positive)(xO (add p q)) = (add (xI p) (double_moins_un q)). +Lemma Pplus_xI_double_minus_one : + forall p q:positive, xO (p + q) = xI p + Pdouble_minus_one q. Proof. -Intros; Change (xI p) with (add (xO p) xH). -Rewrite <- add_assoc; Rewrite <- ZL12bis; Rewrite is_double_moins_un. -Reflexivity. +intros; change (xI p) with (xO p + xH) in |- *. +rewrite <- Pplus_assoc; rewrite <- Pplus_one_succ_l; + rewrite Psucc_o_double_minus_one_eq_xO. +reflexivity. Qed. -Lemma add_xO_double_moins_un : - (p,q:positive) (double_moins_un (add p q)) = (add (xO p) (double_moins_un q)). +Lemma Pplus_xO_double_minus_one : + forall p q:positive, Pdouble_minus_one (p + q) = xO p + Pdouble_minus_one q. Proof. -NewInduction p as [p IHp|p IHp|]; NewDestruct q as [q|q|]; - Simpl; Try Rewrite ZL13; Try Rewrite double_moins_un_add_un_xI; - Try Rewrite IHp; Try Rewrite add_xI_double_moins_un; Try Reflexivity. - Rewrite <- is_double_moins_un; Rewrite ZL12bis; Reflexivity. +induction p as [p IHp| p IHp| ]; destruct q as [q| q| ]; simpl in |- *; + try rewrite Pplus_carry_spec; try rewrite Pdouble_minus_one_o_succ_eq_xI; + try rewrite IHp; try rewrite Pplus_xI_double_minus_one; + try reflexivity. + rewrite <- Psucc_o_double_minus_one_eq_xO; rewrite Pplus_one_succ_l; + reflexivity. Qed. (** Misc *) -Lemma add_x_x : (x:positive) (add x x) = (xO x). +Lemma Pplus_diag : forall p:positive, p + p = xO p. Proof. -Intro x;NewInduction x; Simpl; Try Rewrite ZL13; Try Rewrite IHx; Reflexivity. +intro x; induction x; simpl in |- *; try rewrite Pplus_carry_spec; + try rewrite IHx; reflexivity. Qed. (**********************************************************************) (** Peano induction on binary positive positive numbers *) -Fixpoint plus_iter [x:positive] : positive -> positive := - [y]Cases x of - | xH => (add_un y) - | (xO x) => (plus_iter x (plus_iter x y)) - | (xI x) => (plus_iter x (plus_iter x (add_un y))) +Fixpoint plus_iter (x y:positive) {struct x} : positive := + match x with + | xH => Psucc y + | xO x => plus_iter x (plus_iter x y) + | xI x => plus_iter x (plus_iter x (Psucc y)) end. -Lemma plus_iter_add : (x,y:positive)(plus_iter x y)=(add x y). +Lemma plus_iter_eq_plus : forall p q:positive, plus_iter p q = p + q. Proof. -Intro x;NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y; Simpl; - Reflexivity Orelse Do 2 Rewrite IHp; Rewrite add_assoc; Rewrite add_x_x; - Try Reflexivity. -Rewrite ZL13; Rewrite <- ZL14; Reflexivity. -Rewrite ZL12; Reflexivity. +intro x; induction x as [p IHp| p IHp| ]; intro y; + [ destruct y as [p0| p0| ] + | destruct y as [p0| p0| ] + | destruct y as [p| p| ] ]; simpl in |- *; reflexivity || (do 2 rewrite IHp); + rewrite Pplus_assoc; rewrite Pplus_diag; try reflexivity. +rewrite Pplus_carry_spec; rewrite <- Pplus_succ_permute_r; reflexivity. +rewrite Pplus_one_succ_r; reflexivity. Qed. -Lemma plus_iter_xO : (x:positive)(plus_iter x x)=(xO x). +Lemma plus_iter_xO : forall p:positive, plus_iter p p = xO p. Proof. -Intro; Rewrite <- add_x_x; Apply plus_iter_add. +intro; rewrite <- Pplus_diag; apply plus_iter_eq_plus. Qed. -Lemma plus_iter_xI : (x:positive)(add_un (plus_iter x x))=(xI x). +Lemma plus_iter_xI : forall p:positive, Psucc (plus_iter p p) = xI p. Proof. -Intro; Rewrite xI_add_un_xO; Rewrite <- add_x_x; - Apply (f_equal positive); Apply plus_iter_add. +intro; rewrite xI_succ_xO; rewrite <- Pplus_diag; + apply (f_equal (A:=positive)); apply plus_iter_eq_plus. Qed. -Lemma iterate_add : (P:(positive->Type)) - ((n:positive)(P n) ->(P (add_un n)))->(p,n:positive)(P n) -> - (P (plus_iter p n)). +Lemma iterate_add : + forall P:positive -> Type, + (forall n:positive, P n -> P (Psucc n)) -> + forall p q:positive, P q -> P (plus_iter p q). Proof. -Intros P H; NewInduction p; Simpl; Intros. -Apply IHp; Apply IHp; Apply H; Assumption. -Apply IHp; Apply IHp; Assumption. -Apply H; Assumption. +intros P H; induction p; simpl in |- *; intros. +apply IHp; apply IHp; apply H; assumption. +apply IHp; apply IHp; assumption. +apply H; assumption. Defined. (** Peano induction *) -Theorem Pind : (P:(positive->Prop)) - (P xH) ->((n:positive)(P n) ->(P (add_un n))) ->(n:positive)(P n). +Theorem Pind : + forall P:positive -> Prop, + P xH -> (forall n:positive, P n -> P (Psucc n)) -> forall p:positive, P p. Proof. -Intros P H1 Hsucc n; NewInduction n. -Rewrite <- plus_iter_xI; Apply Hsucc; Apply iterate_add; Assumption. -Rewrite <- plus_iter_xO; Apply iterate_add; Assumption. -Assumption. +intros P H1 Hsucc n; induction n. +rewrite <- plus_iter_xI; apply Hsucc; apply iterate_add; assumption. +rewrite <- plus_iter_xO; apply iterate_add; assumption. +assumption. Qed. (** Peano recursion *) -Definition Prec : (A:Set)A->(positive->A->A)->positive->A := - [A;a;f]Fix Prec { Prec [p:positive] : A := - Cases p of - | xH => a - | (xO p) => (iterate_add [_]A f p p (Prec p)) - | (xI p) => (f (plus_iter p p) (iterate_add [_]A f p p (Prec p))) - end}. +Definition Prec (A:Set) (a:A) (f:positive -> A -> A) : + positive -> A := + (fix Prec (p:positive) : A := + match p with + | xH => a + | xO p => iterate_add (fun _ => A) f p p (Prec p) + | xI p => f (plus_iter p p) (iterate_add (fun _ => A) f p p (Prec p)) + end). (** Peano case analysis *) -Theorem Pcase : (P:(positive->Prop)) - (P xH) ->((n:positive)(P (add_un n))) ->(n:positive)(P n). +Theorem Pcase : + forall P:positive -> Prop, + P xH -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p. Proof. -Intros; Apply Pind; Auto. +intros; apply Pind; auto. Qed. +(* Check - let fact = (Prec positive xH [p;r](times (add_un p) r)) in - let seven = (xI (xI xH)) in - let five_thousand_forty= (xO(xO(xO(xO(xI(xI(xO(xI(xI(xI(xO(xO xH)))))))))))) - in ((refl_equal ? ?) :: (fact seven) = five_thousand_forty). + (let fact := Prec positive xH (fun p r => Psucc p * r) in + let seven := xI (xI xH) in + let five_thousand_forty := + xO (xO (xO (xO (xI (xI (xO (xI (xI (xI (xO (xO xH))))))))))) in + refl_equal _:fact seven = five_thousand_forty). +*) (**********************************************************************) (** Properties of multiplication on binary positive numbers *) (** One is right neutral for multiplication *) -Lemma times_x_1 : (x:positive) (times x xH) = x. +Lemma Pmult_1_r : forall p:positive, p * xH = p. Proof. -Intro x;NewInduction x; Simpl. - Rewrite IHx; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. +intro x; induction x; simpl in |- *. + rewrite IHx; reflexivity. + rewrite IHx; reflexivity. + reflexivity. Qed. (** Right reduction properties for multiplication *) -Lemma times_x_double : (x,y:positive) (times x (xO y)) = (xO (times x y)). +Lemma Pmult_xO_permute_r : forall p q:positive, p * xO q = xO (p * q). Proof. -Intros x y; NewInduction x; Simpl. - Rewrite IHx; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. +intros x y; induction x; simpl in |- *. + rewrite IHx; reflexivity. + rewrite IHx; reflexivity. + reflexivity. Qed. -Lemma times_x_double_plus_one : - (x,y:positive) (times x (xI y)) = (add x (xO (times x y))). +Lemma Pmult_xI_permute_r : forall p q:positive, p * xI q = p + xO (p * q). Proof. -Intros x y; NewInduction x; Simpl. - Rewrite IHx; Do 2 Rewrite add_assoc; Rewrite add_sym with x:=y; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. +intros x y; induction x; simpl in |- *. + rewrite IHx; do 2 rewrite Pplus_assoc; rewrite Pplus_comm with (p := y); + reflexivity. + rewrite IHx; reflexivity. + reflexivity. Qed. (** Commutativity of multiplication *) -Theorem times_sym : (x,y:positive) (times x y) = (times y x). +Theorem Pmult_comm : forall p q:positive, p * q = q * p. Proof. -Intros x y; NewInduction y; Simpl. - Rewrite <- IHy; Apply times_x_double_plus_one. - Rewrite <- IHy; Apply times_x_double. - Apply times_x_1. +intros x y; induction y; simpl in |- *. + rewrite <- IHy; apply Pmult_xI_permute_r. + rewrite <- IHy; apply Pmult_xO_permute_r. + apply Pmult_1_r. Qed. (** Distributivity of multiplication over addition *) -Theorem times_add_distr: - (x,y,z:positive) (times x (add y z)) = (add (times x y) (times x z)). +Theorem Pmult_plus_distr_l : + forall p q r:positive, p * (q + r) = p * q + p * r. Proof. -Intros x y z; NewInduction x; Simpl. - Rewrite IHx; Rewrite <- add_assoc with y := (xO (times x y)); - Rewrite -> add_assoc with x := (xO (times x y)); - Rewrite -> add_sym with x := (xO (times x y)); - Rewrite <- add_assoc with y := (xO (times x y)); - Rewrite -> add_assoc with y := z; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. +intros x y z; induction x; simpl in |- *. + rewrite IHx; rewrite <- Pplus_assoc with (q := xO (x * y)); + rewrite Pplus_assoc with (p := xO (x * y)); + rewrite Pplus_comm with (p := xO (x * y)); + rewrite <- Pplus_assoc with (q := xO (x * y)); + rewrite Pplus_assoc with (q := z); reflexivity. + rewrite IHx; reflexivity. + reflexivity. Qed. -Theorem times_add_distr_l: - (x,y,z:positive) (times (add x y) z) = (add (times x z) (times y z)). +Theorem Pmult_plus_distr_r : + forall p q r:positive, (p + q) * r = p * r + q * r. Proof. -Intros x y z; Do 3 Rewrite times_sym with y:=z; Apply times_add_distr. +intros x y z; do 3 rewrite Pmult_comm with (q := z); apply Pmult_plus_distr_l. Qed. (** Associativity of multiplication *) -Theorem times_assoc : - ((x,y,z:positive) (times x (times y z))= (times (times x y) z)). +Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r. Proof. -Intro x;NewInduction x as [x|x|]; Simpl; Intros y z. - Rewrite IHx; Rewrite times_add_distr_l; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. +intro x; induction x as [x| x| ]; simpl in |- *; intros y z. + rewrite IHx; rewrite Pmult_plus_distr_r; reflexivity. + rewrite IHx; reflexivity. + reflexivity. Qed. (** Parity properties of multiplication *) -Lemma times_discr_xO_xI : - (x,y,z:positive)(times (xI x) z)<>(times (xO y) z). +Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, xI p * r <> xO q * r. Proof. -Intros x y z; NewInduction z as [|z IHz|]; Try Discriminate. -Intro H; Apply IHz; Clear IHz. -Do 2 Rewrite times_x_double in H. -Injection H; Clear H; Intro H; Exact H. +intros x y z; induction z as [| z IHz| ]; try discriminate. +intro H; apply IHz; clear IHz. +do 2 rewrite Pmult_xO_permute_r in H. +injection H; clear H; intro H; exact H. Qed. -Lemma times_discr_xO : (x,y:positive)(times (xO x) y)<>y. +Lemma Pmult_xO_discr : forall p q:positive, xO p * q <> q. Proof. -Intros x y; NewInduction y; Try Discriminate. -Rewrite times_x_double; Injection; Assumption. +intros x y; induction y; try discriminate. +rewrite Pmult_xO_permute_r; injection; assumption. Qed. (** Simplification properties of multiplication *) -Theorem simpl_times_r : (x,y,z:positive) (times x z)=(times y z) -> x=y. +Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q. Proof. -Intro x;NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|]; Intros z H; - Reflexivity Orelse Apply (f_equal positive) Orelse Apply False_ind. - Simpl in H; Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double; - Apply simpl_add_l with 1 := H. - Apply times_discr_xO_xI with 1 := H. - Simpl in H; Rewrite add_sym in H; Apply add_no_neutral with 1 := H. - Symmetry in H; Apply times_discr_xO_xI with 1 := H. - Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double; Assumption. - Apply times_discr_xO with 1:=H. - Simpl in H; Symmetry in H; Rewrite add_sym in H; - Apply add_no_neutral with 1 := H. - Symmetry in H; Apply times_discr_xO with 1:=H. +intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ]; + intros z H; reflexivity || apply (f_equal (A:=positive)) || apply False_ind. + simpl in H; apply IHp with (xO z); simpl in |- *; + do 2 rewrite Pmult_xO_permute_r; apply Pplus_reg_l with (1 := H). + apply Pmult_xI_mult_xO_discr with (1 := H). + simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1 := H). + symmetry in H; apply Pmult_xI_mult_xO_discr with (1 := H). + apply IHp with (xO z); simpl in |- *; do 2 rewrite Pmult_xO_permute_r; + assumption. + apply Pmult_xO_discr with (1 := H). + simpl in H; symmetry in H; rewrite Pplus_comm in H; + apply Pplus_no_neutral with (1 := H). + symmetry in H; apply Pmult_xO_discr with (1 := H). Qed. -Theorem simpl_times_l : (x,y,z:positive) (times z x)=(times z y) -> x=y. +Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q. Proof. -Intros x y z H; Apply simpl_times_r with z:=z. -Rewrite times_sym with x:=x; Rewrite times_sym with x:=y; Assumption. +intros x y z H; apply Pmult_reg_r with (r := z). +rewrite Pmult_comm with (p := x); rewrite Pmult_comm with (p := y); + assumption. Qed. (** Inversion of multiplication *) -Lemma times_one_inversion_l : (x,y:positive) (times x y)=xH -> x=xH. +Lemma Pmult_1_inversion_l : forall p q:positive, p * q = xH -> p = xH. Proof. -Intros x y; NewDestruct x; Simpl. - NewDestruct y; Intro; Discriminate. - Intro; Discriminate. - Reflexivity. +intros x y; destruct x as [p| p| ]; simpl in |- *. + destruct y as [p0| p0| ]; intro; discriminate. + intro; discriminate. + reflexivity. Qed. (**********************************************************************) (** Properties of comparison on binary positive numbers *) -Theorem compare_convert1 : - (x,y:positive) - ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL. +Theorem Pcompare_not_Eq : + forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq. Proof. -Intro x; NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|]; - Split;Simpl;Auto; - Discriminate Orelse (Elim (IHp q); Auto). +intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ]; + split; simpl in |- *; auto; discriminate || (elim (IHp q); auto). Qed. -Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y. +Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q. Proof. -Intro x; NewInduction x as [p IHp|p IHp|]; - Intro y; NewDestruct y as [q|q|];Simpl;Auto; Intro H; [ - Rewrite (IHp q); Trivial -| Absurd (compare p q SUPERIEUR)=EGAL ; - [ Elim (compare_convert1 p q);Auto | Assumption ] -| Discriminate H -| Absurd (compare p q INFERIEUR) = EGAL; - [ Elim (compare_convert1 p q);Auto | Assumption ] -| Rewrite (IHp q);Auto -| Discriminate H -| Discriminate H -| Discriminate H ]. +intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ]; + simpl in |- *; auto; intro H; + [ rewrite (IHp q); trivial + | absurd ((p ?= q) Gt = Eq); + [ elim (Pcompare_not_Eq p q); auto | assumption ] + | discriminate H + | absurd ((p ?= q) Lt = Eq); + [ elim (Pcompare_not_Eq p q); auto | assumption ] + | rewrite (IHp q); auto + | discriminate H + | discriminate H + | discriminate H ]. Qed. -Lemma ZLSI: - (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> - (compare x y EGAL) = INFERIEUR. +Lemma Pcompare_Gt_Lt : + forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt. Proof. -Intro x; Induction x;Intro y; Induction y;Simpl;Auto; - Discriminate Orelse Intros H;Discriminate H. +intro x; induction x as [x Hrecx| x Hrecx| ]; intro y; + [ induction y as [y Hrecy| y Hrecy| ] + | induction y as [y Hrecy| y Hrecy| ] + | induction y as [y Hrecy| y Hrecy| ] ]; simpl in |- *; + auto; discriminate || intros H; discriminate H. Qed. -Lemma ZLIS: - (x,y:positive) (compare x y INFERIEUR) = SUPERIEUR -> - (compare x y EGAL) = SUPERIEUR. +Lemma Pcompare_Lt_Gt : + forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt. Proof. -Intro x; Induction x;Intro y; Induction y;Simpl;Auto; - Discriminate Orelse Intros H;Discriminate H. +intro x; induction x as [x Hrecx| x Hrecx| ]; intro y; + [ induction y as [y Hrecy| y Hrecy| ] + | induction y as [y Hrecy| y Hrecy| ] + | induction y as [y Hrecy| y Hrecy| ] ]; simpl in |- *; + auto; discriminate || intros H; discriminate H. Qed. -Lemma ZLII: - (x,y:positive) (compare x y INFERIEUR) = INFERIEUR -> - (compare x y EGAL) = INFERIEUR \/ x = y. +Lemma Pcompare_Lt_Lt : + forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q. Proof. -(Intro x; NewInduction x as [p IHp|p IHp|]; - Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate); - Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E; - Auto. +intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ]; + simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2); + auto; intros E; rewrite E; auto. Qed. -Lemma ZLSS: - (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR -> - (compare x y EGAL) = SUPERIEUR \/ x = y. +Lemma Pcompare_Gt_Gt : + forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q. Proof. -(Intro x; NewInduction x as [p IHp|p IHp|]; - Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate); - Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E; - Auto. +intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ]; + simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2); + auto; intros E; rewrite E; auto. Qed. -Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR. +Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt. Proof. -Induction r; Auto. +simple induction r; auto. Qed. -Tactic Definition ElimPcompare c1 c2:= - Elim (Dcompare (compare c1 c2 EGAL)); [ Idtac | - Let x = FreshId "H" In Intro x; Case x; Clear x ]. +Ltac ElimPcompare c1 c2 := + elim (Dcompare ((c1 ?= c2) Eq)); + [ idtac | let x := fresh "H" in + (intro x; case x; clear x) ]. -Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL. -Intro x; Induction x; Auto. +Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq. +intro x; induction x as [x Hrecx| x Hrecx| ]; auto. Qed. Lemma Pcompare_antisym : - (x,y:positive)(r:relation) (Op (compare x y r)) = (compare y x (Op r)). + forall (p q:positive) (r:comparison), + CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r). Proof. -Intro x; NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y; -Intro r; Reflexivity Orelse (Symmetry; Assumption) Orelse Discriminate H -Orelse Simpl; Apply IHp Orelse Try Rewrite IHp; Try Reflexivity. +intro x; induction x as [p IHp| p IHp| ]; intro y; + [ destruct y as [p0| p0| ] + | destruct y as [p0| p0| ] + | destruct y as [p| p| ] ]; intro r; + reflexivity || + (symmetry in |- *; assumption) || discriminate H || simpl in |- *; + apply IHp || (try rewrite IHp); try reflexivity. Qed. -Lemma ZC1: - (x,y:positive)(compare x y EGAL)=SUPERIEUR -> (compare y x EGAL)=INFERIEUR. +Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt. Proof. -Intros; Change EGAL with (Op EGAL). -Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity. +intros; change Eq with (CompOpp Eq) in |- *. +rewrite <- Pcompare_antisym; rewrite H; reflexivity. Qed. -Lemma ZC2: - (x,y:positive)(compare x y EGAL)=INFERIEUR -> (compare y x EGAL)=SUPERIEUR. +Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt. Proof. -Intros; Change EGAL with (Op EGAL). -Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity. +intros; change Eq with (CompOpp Eq) in |- *. +rewrite <- Pcompare_antisym; rewrite H; reflexivity. Qed. -Lemma ZC3: (x,y:positive)(compare x y EGAL)=EGAL -> (compare y x EGAL)=EGAL. +Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq. Proof. -Intros; Change EGAL with (Op EGAL). -Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity. +intros; change Eq with (CompOpp Eq) in |- *. +rewrite <- Pcompare_antisym; rewrite H; reflexivity. Qed. -Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)). +Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq). Proof. -Intros; Change 1 EGAL with (Op EGAL). -Symmetry; Apply Pcompare_antisym. +intros; change Eq at 1 with (CompOpp Eq) in |- *. +symmetry in |- *; apply Pcompare_antisym. Qed. (**********************************************************************) (** Properties of subtraction on binary positive numbers *) -Lemma ZS: (p:positive_mask) (Zero_suivi_de_mask p) = IsNul -> p = IsNul. +Lemma double_eq_zero_inversion : + forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul. Proof. -NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ]. +destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ]. Qed. -Lemma US: (p:positive_mask) ~(Un_suivi_de_mask p)=IsNul. +Lemma double_plus_one_zero_discr : + forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul. Proof. -Induction p; Intros; Discriminate. +simple induction p; intros; discriminate. Qed. -Lemma USH: (p:positive_mask) (Un_suivi_de_mask p) = (IsPos xH) -> p = IsNul. +Lemma double_plus_one_eq_one_inversion : + forall p:positive_mask, Pdouble_plus_one_mask p = IsPos xH -> p = IsNul. Proof. -NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ]. +destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ]. Qed. -Lemma ZSH: (p:positive_mask) ~(Zero_suivi_de_mask p)= (IsPos xH). +Lemma double_eq_one_discr : + forall p:positive_mask, Pdouble_mask p <> IsPos xH. Proof. -Induction p; Intros; Discriminate. +simple induction p; intros; discriminate. Qed. -Theorem sub_pos_x_x : (x:positive) (sub_pos x x) = IsNul. +Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul. Proof. -Intro x; NewInduction x as [p IHp|p IHp|]; [ - Simpl; Rewrite IHp;Simpl; Trivial -| Simpl; Rewrite IHp;Auto -| Auto ]. +intro x; induction x as [p IHp| p IHp| ]; + [ simpl in |- *; rewrite IHp; simpl in |- *; trivial + | simpl in |- *; rewrite IHp; auto + | auto ]. Qed. -Lemma ZL10: (x,y:positive) - (sub_pos x y) = (IsPos xH) -> (sub_neg x y) = IsNul. +Lemma ZL10 : + forall p q:positive, + Pminus_mask p q = IsPos xH -> Pminus_mask_carry p q = IsNul. Proof. -Intro x; NewInduction x as [p|p|]; Intro y; NewDestruct y as [q|q|]; Simpl; - Intro H; Try Discriminate H; [ - Absurd (Zero_suivi_de_mask (sub_pos p q))=(IsPos xH); - [ Apply ZSH | Assumption ] -| Assert Heq : (sub_pos p q)=IsNul; - [ Apply USH;Assumption | Rewrite Heq; Reflexivity ] -| Assert Heq : (sub_neg p q)=IsNul; - [ Apply USH;Assumption | Rewrite Heq; Reflexivity ] -| Absurd (Zero_suivi_de_mask (sub_pos p q))=(IsPos xH); - [ Apply ZSH | Assumption ] -| NewDestruct p; Simpl; [ Discriminate H | Discriminate H | Reflexivity ] ]. +intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ]; + simpl in |- *; intro H; try discriminate H; + [ absurd (Pdouble_mask (Pminus_mask p q) = IsPos xH); + [ apply double_eq_one_discr | assumption ] + | assert (Heq : Pminus_mask p q = IsNul); + [ apply double_plus_one_eq_one_inversion; assumption + | rewrite Heq; reflexivity ] + | assert (Heq : Pminus_mask_carry p q = IsNul); + [ apply double_plus_one_eq_one_inversion; assumption + | rewrite Heq; reflexivity ] + | absurd (Pdouble_mask (Pminus_mask p q) = IsPos xH); + [ apply double_eq_one_discr | assumption ] + | destruct p; simpl in |- *; + [ discriminate H | discriminate H | reflexivity ] ]. Qed. (** Properties of subtraction valid only for x>y *) -Lemma sub_pos_SUPERIEUR: - (x,y:positive)(compare x y EGAL)=SUPERIEUR -> - (EX h:positive | (sub_pos x y) = (IsPos h) /\ (add y h) = x /\ - (h = xH \/ (sub_neg x y) = (IsPos (sub_un h)))). -Proof. -Intro x;NewInduction x as [p|p|];Intro y; NewDestruct y as [q|q|]; Simpl; Intro H; - Try Discriminate H. - NewDestruct (IHp q H) as [z [H4 [H6 H7]]]; Exists (xO z); Split. - Rewrite H4; Reflexivity. - Split. - Simpl; Rewrite H6; Reflexivity. - Right; Clear H6; NewDestruct (ZL11 z) as [H8|H8]; [ - Rewrite H8; Rewrite H8 in H4; - Rewrite ZL10; [ Reflexivity | Assumption ] - | Clear H4; NewDestruct H7 as [H9|H9]; [ - Absurd z=xH; Assumption - | Rewrite H9; Clear H9; NewDestruct z; - [ Reflexivity | Reflexivity | Absurd xH=xH; Trivial ]]]. - Case ZLSS with 1:=H; [ - Intros H3;Elim (IHp q H3); Intros z H4; Exists (xI z); - Elim H4;Intros H5 H6;Elim H6;Intros H7 H8; Split; [ - Simpl;Rewrite H5;Auto - | Split; [ - Simpl; Rewrite H7; Trivial - | Right; - Change (Zero_suivi_de_mask (sub_pos p q))=(IsPos (sub_un (xI z))); - Rewrite H5; Auto ]] - | Intros H3; Exists xH; Rewrite H3; Split; [ - Simpl; Rewrite sub_pos_x_x; Auto - | Split; Auto ]]. - Exists (xO p); Auto. - NewDestruct (IHp q) as [z [H4 [H6 H7]]]. - Apply ZLIS; Assumption. - NewDestruct (ZL11 z) as [vZ|]; [ - Exists xH; Split; [ - Rewrite ZL10; [ Reflexivity | Rewrite vZ in H4;Assumption ] - | Split; [ - Simpl; Rewrite ZL12; Rewrite <- vZ; Rewrite H6; Trivial - | Auto ]] - | Exists (xI (sub_un z)); NewDestruct H7 as [|H8];[ - Absurd z=xH;Assumption - | Split; [ - Rewrite H8; Trivial - | Split; [ Simpl; Rewrite ZL15; [ - Rewrite H6;Trivial - | Assumption ] - | Right; Rewrite H8; Reflexivity]]]]. - NewDestruct (IHp q H) as [z [H4 [H6 H7]]]. - Exists (xO z); Split; [ - Rewrite H4;Auto - | Split; [ - Simpl;Rewrite H6;Reflexivity - | Right; - Change (Un_suivi_de_mask (sub_neg p q))=(IsPos (double_moins_un z)); - NewDestruct (ZL11 z) as [H8|H8]; [ - Rewrite H8; Simpl; - Assert H9:(sub_neg p q)=IsNul;[ - Apply ZL10;Rewrite <- H8;Assumption - | Rewrite H9;Reflexivity ] - | NewDestruct H7 as [H9|H9]; [ - Absurd z=xH;Auto - | Rewrite H9; NewDestruct z; Simpl; - [ Reflexivity - | Reflexivity - | Absurd xH=xH; [Assumption | Reflexivity]]]]]]. - Exists (double_moins_un p); Split; [ - Reflexivity - | Clear IHp; Split; [ - NewDestruct p; Simpl; [ - Reflexivity - | Rewrite is_double_moins_un; Reflexivity - | Reflexivity ] - | NewDestruct p; [Right|Right|Left]; Reflexivity ]]. -Qed. - -Theorem sub_add: -(x,y:positive) (compare x y EGAL) = SUPERIEUR -> (add y (true_sub x y)) = x. -Proof. -Intros x y H;Elim sub_pos_SUPERIEUR with 1:=H; -Intros z H1;Elim H1;Intros H2 H3; Elim H3;Intros H4 H5; -Unfold true_sub ;Rewrite H2; Exact H4. +Lemma Pminus_mask_Gt : + forall p q:positive, + (p ?= q) Eq = Gt -> + exists h : positive + | Pminus_mask p q = IsPos h /\ + q + h = p /\ (h = xH \/ Pminus_mask_carry p q = IsPos (Ppred h)). +Proof. +intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ]; + simpl in |- *; intro H; try discriminate H. + destruct (IHp q H) as [z [H4 [H6 H7]]]; exists (xO z); split. + rewrite H4; reflexivity. + split. + simpl in |- *; rewrite H6; reflexivity. + right; clear H6; destruct (ZL11 z) as [H8| H8]; + [ rewrite H8; rewrite H8 in H4; rewrite ZL10; + [ reflexivity | assumption ] + | clear H4; destruct H7 as [H9| H9]; + [ absurd (z = xH); assumption + | rewrite H9; clear H9; destruct z as [p0| p0| ]; + [ reflexivity | reflexivity | absurd (xH = xH); trivial ] ] ]. + case Pcompare_Gt_Gt with (1 := H); + [ intros H3; elim (IHp q H3); intros z H4; exists (xI z); elim H4; + intros H5 H6; elim H6; intros H7 H8; split; + [ simpl in |- *; rewrite H5; auto + | split; + [ simpl in |- *; rewrite H7; trivial + | right; + change (Pdouble_mask (Pminus_mask p q) = IsPos (Ppred (xI z))) + in |- *; rewrite H5; auto ] ] + | intros H3; exists xH; rewrite H3; split; + [ simpl in |- *; rewrite Pminus_mask_diag; auto | split; auto ] ]. + exists (xO p); auto. + destruct (IHp q) as [z [H4 [H6 H7]]]. + apply Pcompare_Lt_Gt; assumption. + destruct (ZL11 z) as [vZ| ]; + [ exists xH; split; + [ rewrite ZL10; [ reflexivity | rewrite vZ in H4; assumption ] + | split; + [ simpl in |- *; rewrite Pplus_one_succ_r; rewrite <- vZ; + rewrite H6; trivial + | auto ] ] + | exists (xI (Ppred z)); destruct H7 as [| H8]; + [ absurd (z = xH); assumption + | split; + [ rewrite H8; trivial + | split; + [ simpl in |- *; rewrite Pplus_carry_pred_eq_plus; + [ rewrite H6; trivial | assumption ] + | right; rewrite H8; reflexivity ] ] ] ]. + destruct (IHp q H) as [z [H4 [H6 H7]]]. + exists (xO z); split; + [ rewrite H4; auto + | split; + [ simpl in |- *; rewrite H6; reflexivity + | right; + change + (Pdouble_plus_one_mask (Pminus_mask_carry p q) = + IsPos (Pdouble_minus_one z)) in |- *; + destruct (ZL11 z) as [H8| H8]; + [ rewrite H8; simpl in |- *; + assert (H9 : Pminus_mask_carry p q = IsNul); + [ apply ZL10; rewrite <- H8; assumption + | rewrite H9; reflexivity ] + | destruct H7 as [H9| H9]; + [ absurd (z = xH); auto + | rewrite H9; destruct z as [p0| p0| ]; simpl in |- *; + [ reflexivity + | reflexivity + | absurd (xH = xH); [ assumption | reflexivity ] ] ] ] ] ]. + exists (Pdouble_minus_one p); split; + [ reflexivity + | clear IHp; split; + [ destruct p; simpl in |- *; + [ reflexivity + | rewrite Psucc_o_double_minus_one_eq_xO; reflexivity + | reflexivity ] + | destruct p; [ right | right | left ]; reflexivity ] ]. +Qed. + +Theorem Pplus_minus : + forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p. +Proof. +intros x y H; elim Pminus_mask_Gt with (1 := H); intros z H1; elim H1; + intros H2 H3; elim H3; intros H4 H5; unfold Pminus in |- *; + rewrite H2; exact H4. Qed. - diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index e3392de4ca..5e5ab1f0d8 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -11,4 +11,4 @@ (** Library for binary natural numbers *) Require Export BinPos. -Require Export BinNat. +Require Export BinNat.
\ No newline at end of file diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index 22c6b5cb90..c0e2bb020f 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require BinPos. +Require Import BinPos. (**********************************************************************) (** Properties of the injection from binary positive numbers to Peano @@ -16,144 +16,142 @@ Require BinPos. (** Original development by Pierre Crégut, CNET, Lannion, France *) -Require Le. -Require Lt. -Require Gt. -Require Plus. -Require Mult. -Require Minus. +Require Import Le. +Require Import Lt. +Require Import Gt. +Require Import Plus. +Require Import Mult. +Require Import Minus. (** [nat_of_P] is a morphism for addition *) -Lemma convert_add_un : - (x:positive)(m:nat) - (positive_to_nat (add_un x) m) = (plus m (positive_to_nat x m)). +Lemma Pmult_nat_succ_morphism : + forall (p:positive) (n:nat), Pmult_nat (Psucc p) n = n + Pmult_nat p n. Proof. -Intro x; NewInduction x as [p IHp|p IHp|]; Simpl; Auto; Intro m; Rewrite IHp; -Rewrite plus_assoc_l; Trivial. +intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m; + rewrite IHp; rewrite plus_assoc; trivial. Qed. -Lemma cvt_add_un : - (p:positive) (convert (add_un p)) = (S (convert p)). +Lemma nat_of_P_succ_morphism : + forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p). Proof. - Intro; Change (S (convert p)) with (plus (S O) (convert p)); - Unfold convert; Apply convert_add_un. + intro; change (S (nat_of_P p)) with (1 + nat_of_P p) in |- *; + unfold nat_of_P in |- *; apply Pmult_nat_succ_morphism. Qed. -Theorem convert_add_carry : - (x,y:positive)(m:nat) - (positive_to_nat (add_carry x y) m) = - (plus m (positive_to_nat (add x y) m)). +Theorem Pmult_nat_plus_carry_morphism : + forall (p q:positive) (n:nat), + Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n. Proof. -Intro x; NewInduction x as [p IHp|p IHp|]; - Intro y; NewDestruct y; Simpl; Auto with arith; Intro m; [ - Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith -| Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith -| Rewrite convert_add_un; Rewrite plus_assoc_l; Trivial with arith -| Rewrite convert_add_un; Apply plus_assoc_r ]. +intro x; induction x as [p IHp| p IHp| ]; intro y; + [ destruct y as [p0| p0| ] + | destruct y as [p0| p0| ] + | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; + intro m; + [ rewrite IHp; rewrite plus_assoc; trivial with arith + | rewrite IHp; rewrite plus_assoc; trivial with arith + | rewrite Pmult_nat_succ_morphism; rewrite plus_assoc; trivial with arith + | rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ]. Qed. -Theorem cvt_carry : - (x,y:positive)(convert (add_carry x y)) = (S (convert (add x y))). +Theorem nat_of_P_plus_carry_morphism : + forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)). Proof. -Intros;Unfold convert; Rewrite convert_add_carry; Simpl; Trivial with arith. +intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism; + simpl in |- *; trivial with arith. Qed. -Theorem add_verif : - (x,y:positive)(m:nat) - (positive_to_nat (add x y) m) = - (plus (positive_to_nat x m) (positive_to_nat y m)). +Theorem Pmult_nat_l_plus_morphism : + forall (p q:positive) (n:nat), + Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n. Proof. -Intro x; NewInduction x as [p IHp|p IHp|]; - Intro y; NewDestruct y;Simpl;Auto with arith; [ - Intros m;Rewrite convert_add_carry; Rewrite IHp; - Rewrite plus_assoc_r; Rewrite plus_assoc_r; - Rewrite (plus_permute m (positive_to_nat p (plus m m))); Trivial with arith -| Intros m; Rewrite IHp; Apply plus_assoc_l -| Intros m; Rewrite convert_add_un; - Rewrite (plus_sym (plus m (positive_to_nat p (plus m m)))); - Apply plus_assoc_r -| Intros m; Rewrite IHp; Apply plus_permute -| Intros m; Rewrite convert_add_un; Apply plus_assoc_r ]. +intro x; induction x as [p IHp| p IHp| ]; intro y; + [ destruct y as [p0| p0| ] + | destruct y as [p0| p0| ] + | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; + [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp; + rewrite plus_assoc_reverse; rewrite plus_assoc_reverse; + rewrite (plus_permute m (Pmult_nat p (m + m))); + trivial with arith + | intros m; rewrite IHp; apply plus_assoc + | intros m; rewrite Pmult_nat_succ_morphism; + rewrite (plus_comm (m + Pmult_nat p (m + m))); + apply plus_assoc_reverse + | intros m; rewrite IHp; apply plus_permute + | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ]. Qed. -Theorem convert_add: - (x,y:positive) (convert (add x y)) = (plus (convert x) (convert y)). +Theorem nat_of_P_plus_morphism : + forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q. Proof. -Intros x y; Exact (add_verif x y (S O)). +intros x y; exact (Pmult_nat_l_plus_morphism x y 1). Qed. (** [Pmult_nat] is a morphism for addition *) -Lemma ZL2: - (y:positive)(m:nat) - (positive_to_nat y (plus m m)) = - (plus (positive_to_nat y m) (positive_to_nat y m)). +Lemma Pmult_nat_r_plus_morphism : + forall (p:positive) (n:nat), + Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n. Proof. -Intro y; NewInduction y as [p H|p H|]; Intro m; [ - Simpl; Rewrite H; Rewrite plus_assoc_r; - Rewrite (plus_permute m (positive_to_nat p (plus m m))); - Rewrite plus_assoc_r; Auto with arith -| Simpl; Rewrite H; Auto with arith -| Simpl; Trivial with arith ]. +intro y; induction y as [p H| p H| ]; intro m; + [ simpl in |- *; rewrite H; rewrite plus_assoc_reverse; + rewrite (plus_permute m (Pmult_nat p (m + m))); + rewrite plus_assoc_reverse; auto with arith + | simpl in |- *; rewrite H; auto with arith + | simpl in |- *; trivial with arith ]. Qed. -Lemma ZL6: - (p:positive) (positive_to_nat p (S (S O))) = (plus (convert p) (convert p)). +Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p. Proof. -Intro p;Change (2) with (plus (S O) (S O)); Rewrite ZL2; Trivial. +intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism; + trivial. Qed. (** [nat_of_P] is a morphism for multiplication *) -Theorem times_convert : - (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)). -Proof. -Intros x y; NewInduction x as [ x' H | x' H | ]; [ - Change (times (xI x') y) with (add y (xO (times x' y))); Rewrite convert_add; - Unfold 2 3 convert; Simpl; Do 2 Rewrite ZL6; Rewrite H; - Rewrite -> mult_plus_distr; Reflexivity -| Unfold 1 2 convert; Simpl; Do 2 Rewrite ZL6; - Rewrite H; Rewrite mult_plus_distr; Reflexivity -| Simpl; Rewrite <- plus_n_O; Reflexivity ]. -Qed. -V7only [ - Comments "Compatibility with the old version of times and times_convert". - Syntactic Definition times1 := - [x:positive;_:positive->positive;y:positive](times x y). - Syntactic Definition times1_convert := - [x,y:positive;_:positive->positive](times_convert x y). -]. +Theorem nat_of_P_mult_morphism : + forall p q:positive, nat_of_P (p * q) = nat_of_P p * nat_of_P q. +Proof. +intros x y; induction x as [x' H| x' H| ]; + [ change (xI x' * y)%positive with (y + xO (x' * y))%positive in |- *; + rewrite nat_of_P_plus_morphism; unfold nat_of_P at 2 3 in |- *; + simpl in |- *; do 2 rewrite ZL6; rewrite H; rewrite mult_plus_distr_r; + reflexivity + | unfold nat_of_P at 1 2 in |- *; simpl in |- *; do 2 rewrite ZL6; rewrite H; + rewrite mult_plus_distr_r; reflexivity + | simpl in |- *; rewrite <- plus_n_O; reflexivity ]. +Qed. (** [nat_of_P] maps to the strictly positive subset of [nat] *) -Lemma ZL4: (y:positive) (EX h:nat |(convert y)=(S h)). +Lemma ZL4 : forall p:positive, exists h : nat | nat_of_P p = S h. Proof. -Intro y; NewInduction y as [p H|p H|]; [ - NewDestruct H as [x H1]; Exists (plus (S x) (S x)); - Unfold convert ;Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2; Unfold convert in H1; - Rewrite H1; Auto with arith -| NewDestruct H as [x H2]; Exists (plus x (S x)); Unfold convert; - Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith -| Exists O ;Auto with arith ]. +intro y; induction y as [p H| p H| ]; + [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *; + simpl in |- *; change 2 with (1 + 1) in |- *; + rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; + rewrite H1; auto with arith + | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *; + simpl in |- *; change 2 with (1 + 1) in |- *; + rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; + rewrite H2; auto with arith + | exists 0; auto with arith ]. Qed. (** Extra lemmas on [lt] on Peano natural numbers *) -Lemma ZL7: - (m,n:nat) (lt m n) -> (lt (plus m m) (plus n n)). +Lemma ZL7 : forall n m:nat, n < m -> n + n < m + m. Proof. -Intros m n H; Apply lt_trans with m:=(plus m n); [ - Apply lt_reg_l with 1:=H -| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. +intros m n H; apply lt_trans with (m := m + n); + [ apply plus_lt_compat_l with (1 := H) + | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. Qed. -Lemma ZL8: - (m,n:nat) (lt m n) -> (lt (S (plus m m)) (plus n n)). +Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m. Proof. -Intros m n H; Apply le_lt_trans with m:=(plus m n); [ - Change (lt (plus m m) (plus m n)) ; Apply lt_reg_l with 1:=H -| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. +intros m n H; apply le_lt_trans with (m := m + n); + [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H) + | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed @@ -162,29 +160,30 @@ Qed. Part 1: [lt] on [positive] is finer than [lt] on [nat] *) -Lemma compare_convert_INFERIEUR : - (x,y:positive) (compare x y EGAL) = INFERIEUR -> - (lt (convert x) (convert y)). -Proof. -Intro x; NewInduction x as [p H|p H|];Intro y; NewDestruct y as [q|q|]; - Intro H2; [ - Unfold convert ;Simpl; Apply lt_n_S; - Do 2 Rewrite ZL6; Apply ZL7; Apply H; Simpl in H2; Assumption -| Unfold convert ;Simpl; Do 2 Rewrite ZL6; - Apply ZL8; Apply H;Simpl in H2; Apply ZLSI;Assumption -| Simpl; Discriminate H2 -| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Elim (ZLII p q H2); [ - Intros H3;Apply lt_S;Apply ZL7; Apply H;Apply H3 - | Intros E;Rewrite E;Apply lt_n_Sn] -| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL7;Apply H;Assumption -| Simpl; Discriminate H2 -| Unfold convert ;Simpl; Apply lt_n_S; Rewrite ZL6; - Elim (ZL4 q);Intros h H3; Rewrite H3;Simpl; Apply lt_O_Sn -| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 q);Intros h H3; - Rewrite H3; Simpl; Rewrite <- plus_n_Sm; Apply lt_n_S; Apply lt_O_Sn -| Simpl; Discriminate H2 ]. +Lemma nat_of_P_lt_Lt_compare_morphism : + forall p q:positive, (p ?= q)%positive Eq = Lt -> nat_of_P p < nat_of_P q. +Proof. +intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ]; + intro H2; + [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6; + apply ZL7; apply H; simpl in H2; assumption + | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8; + apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption + | simpl in |- *; discriminate H2 + | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + elim (Pcompare_Lt_Lt p q H2); + [ intros H3; apply lt_S; apply ZL7; apply H; apply H3 + | intros E; rewrite E; apply lt_n_Sn ] + | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + apply ZL7; apply H; assumption + | simpl in |- *; discriminate H2 + | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6; + elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; + apply lt_O_Sn + | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q); + intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm; + apply lt_n_S; apply lt_O_Sn + | simpl in |- *; discriminate H2 ]. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed @@ -193,29 +192,30 @@ Qed. Part 1: [gt] on [positive] is finer than [gt] on [nat] *) -Lemma compare_convert_SUPERIEUR : - (x,y:positive) (compare x y EGAL)=SUPERIEUR -> (gt (convert x) (convert y)). -Proof. -Unfold gt; Intro x; NewInduction x as [p H|p H|]; - Intro y; NewDestruct y as [q|q|]; Intro H2; [ - Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply lt_n_S; Apply ZL7; Apply H;Assumption -| Simpl; Unfold convert ;Simpl; Do 2 Rewrite ZL6; - Elim (ZLSS p q H2); [ - Intros H3;Apply lt_S;Apply ZL7;Apply H;Assumption - | Intros E;Rewrite E;Apply lt_n_Sn] -| Unfold convert ;Simpl; Rewrite ZL6;Elim (ZL4 p); - Intros h H3;Rewrite H3;Simpl; Apply lt_n_S; Apply lt_O_Sn -| Simpl;Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL8; Apply H; Apply ZLIS; Assumption -| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL7;Apply H;Assumption -| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 p); - Intros h H3;Rewrite H3;Simpl; Rewrite <- plus_n_Sm;Apply lt_n_S; - Apply lt_O_Sn -| Simpl; Discriminate H2 -| Simpl; Discriminate H2 -| Simpl; Discriminate H2 ]. +Lemma nat_of_P_gt_Gt_compare_morphism : + forall p q:positive, (p ?= q)%positive Eq = Gt -> nat_of_P p > nat_of_P q. +Proof. +unfold gt in |- *; intro x; induction x as [p H| p H| ]; intro y; + destruct y as [q| q| ]; intro H2; + [ simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + apply lt_n_S; apply ZL7; apply H; assumption + | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + elim (Pcompare_Gt_Gt p q H2); + [ intros H3; apply lt_S; apply ZL7; apply H; assumption + | intros E; rewrite E; apply lt_n_Sn ] + | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p); + intros h H3; rewrite H3; simpl in |- *; apply lt_n_S; + apply lt_O_Sn + | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + apply ZL8; apply H; apply Pcompare_Lt_Gt; assumption + | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + apply ZL7; apply H; assumption + | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p); + intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm; + apply lt_n_S; apply lt_O_Sn + | simpl in |- *; discriminate H2 + | simpl in |- *; discriminate H2 + | simpl in |- *; discriminate H2 ]. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed @@ -224,18 +224,18 @@ Qed. Part 2: [lt] on [nat] is finer than [lt] on [positive] *) -Lemma convert_compare_INFERIEUR : - (x,y:positive)(lt (convert x) (convert y)) -> (compare x y EGAL) = INFERIEUR. +Lemma nat_of_P_lt_Lt_compare_complement_morphism : + forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q)%positive Eq = Lt. Proof. -Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ - Intros E; Rewrite (compare_convert_EGAL x y E); - Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] -| Intros H;Elim H; [ - Auto - | Intros H1 H2; Absurd (lt (convert x) (convert y)); [ - Apply lt_not_sym; Change (gt (convert x) (convert y)); - Apply compare_convert_SUPERIEUR; Assumption - | Assumption ]]]. +intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq)); + [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H; + absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ] + | intros H; elim H; + [ auto + | intros H1 H2; absurd (nat_of_P x < nat_of_P y); + [ apply lt_asym; change (nat_of_P x > nat_of_P y) in |- *; + apply nat_of_P_gt_Gt_compare_morphism; assumption + | assumption ] ] ]. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed @@ -244,78 +244,78 @@ Qed. Part 2: [gt] on [nat] is finer than [gt] on [positive] *) -Lemma convert_compare_SUPERIEUR : - (x,y:positive)(gt (convert x) (convert y)) -> (compare x y EGAL) = SUPERIEUR. +Lemma nat_of_P_gt_Gt_compare_complement_morphism : + forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q)%positive Eq = Gt. Proof. -Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ - Intros E; Rewrite (compare_convert_EGAL x y E); - Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] -| Intros H;Elim H; [ - Intros H1 H2; Absurd (lt (convert y) (convert x)); [ - Apply lt_not_sym; Apply compare_convert_INFERIEUR; Assumption - | Assumption ] - | Auto]]. +intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq)); + [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H; + absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ] + | intros H; elim H; + [ intros H1 H2; absurd (nat_of_P y < nat_of_P x); + [ apply lt_asym; apply nat_of_P_lt_Lt_compare_morphism; assumption + | assumption ] + | auto ] ]. Qed. (** [nat_of_P] is strictly positive *) -Lemma compare_positive_to_nat_O : - (p:positive)(m:nat)(le m (positive_to_nat p m)). -NewInduction p; Simpl; Auto with arith. -Intro m; Apply le_trans with (plus m m); Auto with arith. +Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n. +induction p; simpl in |- *; auto with arith. +intro m; apply le_trans with (m + m); auto with arith. Qed. -Lemma compare_convert_O : (p:positive)(lt O (convert p)). -Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith. -Apply compare_positive_to_nat_O. +Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p. +intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith. +apply le_Pmult_nat. Qed. (** Pmult_nat permutes with multiplication *) -Lemma positive_to_nat_mult : (p:positive) (n,m:nat) - (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)). +Lemma Pmult_nat_mult_permute : + forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n. Proof. - Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n). - Rewrite (H (plus n n) m). Reflexivity. - Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H. - Trivial. + simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n). + rewrite (H (n + n) m). reflexivity. + intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H. + trivial. Qed. -Lemma positive_to_nat_2 : (p:positive) - (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))). +Lemma Pmult_nat_2_mult_2_permute : + forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1. Proof. - Intros. Rewrite <- positive_to_nat_mult. Reflexivity. + intros. rewrite <- Pmult_nat_mult_permute. reflexivity. Qed. -Lemma positive_to_nat_4 : (p:positive) - (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))). +Lemma Pmult_nat_4_mult_2_permute : + forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2. Proof. - Intros. Rewrite <- positive_to_nat_mult. Reflexivity. + intros. rewrite <- Pmult_nat_mult_permute. reflexivity. Qed. (** Mapping of xH, xO and xI through [nat_of_P] *) -Lemma convert_xH : (convert xH)=(1). +Lemma nat_of_P_xH : nat_of_P 1 = 1. Proof. - Reflexivity. + reflexivity. Qed. -Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)). +Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p. Proof. - Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. - Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity. - Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4. - Rewrite H. Reflexivity. - Reflexivity. + simple induction p. unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. + rewrite Pmult_nat_4_mult_2_permute. rewrite H. simpl in |- *. rewrite <- plus_Snm_nSm. reflexivity. + unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute. + rewrite H. reflexivity. + reflexivity. Qed. -Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))). +Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p). Proof. - Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2. - Rewrite positive_to_nat_4; Injection H; Intro H1; Rewrite H1; Rewrite <- plus_Snm_nSm; Reflexivity. - Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4. - Injection H; Intro H1; Rewrite H1; Reflexivity. - Reflexivity. + simple induction p. unfold nat_of_P in |- *. simpl in |- *. intro p0. intro. rewrite Pmult_nat_2_mult_2_permute. + rewrite Pmult_nat_4_mult_2_permute; injection H; intro H1; rewrite H1; + rewrite <- plus_Snm_nSm; reflexivity. + unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute. + injection H; intro H1; rewrite H1; reflexivity. + reflexivity. Qed. (**********************************************************************) @@ -324,54 +324,61 @@ Qed. (** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *) -Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m). +Theorem nat_of_P_o_P_of_succ_nat_eq_succ : + forall n:nat, nat_of_P (P_of_succ_nat n) = S n. Proof. -Intro m; NewInduction m as [|n H]; [ - Reflexivity -| Simpl; Rewrite cvt_add_un; Rewrite H; Auto ]. +intro m; induction m as [| n H]; + [ reflexivity + | simpl in |- *; rewrite nat_of_P_succ_morphism; rewrite H; auto ]. Qed. (** Miscellaneous lemmas on [P_of_succ_nat] *) -Lemma ZL3: (x:nat) (add_un (anti_convert (plus x x))) = (xO (anti_convert x)). +Lemma ZL3 : + forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n). Proof. -Intro x; NewInduction x as [|n H]; [ - Simpl; Auto with arith -| Simpl; Rewrite plus_sym; Simpl; Rewrite H; Rewrite ZL1;Auto with arith]. +intro x; induction x as [| n H]; + [ simpl in |- *; auto with arith + | simpl in |- *; rewrite plus_comm; simpl in |- *; rewrite H; + rewrite xO_succ_permute; auto with arith ]. Qed. -Lemma ZL5: (x:nat) (anti_convert (plus (S x) (S x))) = (xI (anti_convert x)). +Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n). Proof. -Intro x; NewInduction x as [|n H];Simpl; [ - Auto with arith -| Rewrite <- plus_n_Sm; Simpl; Simpl in H; Rewrite H; Auto with arith]. +intro x; induction x as [| n H]; simpl in |- *; + [ auto with arith + | rewrite <- plus_n_Sm; simpl in |- *; simpl in H; rewrite H; + auto with arith ]. Qed. (** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *) -Theorem bij2 : (x:positive) (anti_convert (convert x)) = (add_un x). +Theorem P_of_succ_nat_o_nat_of_P_eq_succ : + forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p. Proof. -Intro x; NewInduction x as [p H|p H|]; [ - Simpl; Rewrite <- H; Change (2) with (plus (1) (1)); - Rewrite ZL2; Elim (ZL4 p); - Unfold convert; Intros n H1;Rewrite H1; Rewrite ZL3; Auto with arith -| Unfold convert ;Simpl; Change (2) with (plus (1) (1)); - Rewrite ZL2; - Rewrite <- (sub_add_one - (anti_convert - (plus (positive_to_nat p (S O)) (positive_to_nat p (S O))))); - Rewrite <- (sub_add_one (xI p)); - Simpl;Rewrite <- H;Elim (ZL4 p); Unfold convert ;Intros n H1;Rewrite H1; - Rewrite ZL5; Simpl; Trivial with arith -| Unfold convert; Simpl; Auto with arith ]. +intro x; induction x as [p H| p H| ]; + [ simpl in |- *; rewrite <- H; change 2 with (1 + 1) in |- *; + rewrite Pmult_nat_r_plus_morphism; elim (ZL4 p); + unfold nat_of_P in |- *; intros n H1; rewrite H1; + rewrite ZL3; auto with arith + | unfold nat_of_P in |- *; simpl in |- *; change 2 with (1 + 1) in |- *; + rewrite Pmult_nat_r_plus_morphism; + rewrite <- (Ppred_succ (P_of_succ_nat (Pmult_nat p 1 + Pmult_nat p 1))); + rewrite <- (Ppred_succ (xI p)); simpl in |- *; + rewrite <- H; elim (ZL4 p); unfold nat_of_P in |- *; + intros n H1; rewrite H1; rewrite ZL5; simpl in |- *; + trivial with arith + | unfold nat_of_P in |- *; simpl in |- *; auto with arith ]. Qed. (** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity on [positive] *) -Theorem bij3: (x:positive)(sub_un (anti_convert (convert x))) = x. +Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id : + forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p. Proof. -Intros x; Rewrite bij2; Rewrite sub_add_one; Trivial with arith. +intros x; rewrite P_of_succ_nat_o_nat_of_P_eq_succ; rewrite Ppred_succ; + trivial with arith. Qed. (**********************************************************************) @@ -380,93 +387,99 @@ Qed. (** [nat_of_P] is a morphism for subtraction on positive numbers *) -Theorem true_sub_convert: - (x,y:positive) (compare x y EGAL) = SUPERIEUR -> - (convert (true_sub x y)) = (minus (convert x) (convert y)). +Theorem nat_of_P_minus_morphism : + forall p q:positive, + (p ?= q)%positive Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q. Proof. -Intros x y H; Apply plus_reg_l with (convert y); -Rewrite le_plus_minus_r; [ - Rewrite <- convert_add; Rewrite sub_add; Auto with arith -| Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)]. +intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r; + [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith + | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ]. Qed. (** [nat_of_P] is injective *) -Lemma convert_intro : (x,y:positive)(convert x)=(convert y) -> x=y. +Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q. Proof. -Intros x y H;Rewrite <- (bij3 x);Rewrite <- (bij3 y); Rewrite H; Trivial with arith. +intros x y H; rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id x); + rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id y); + rewrite H; trivial with arith. Qed. -Lemma ZL16: (p,q:positive)(lt (minus (convert p) (convert q)) (convert p)). +Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p. Proof. -Intros p q; Elim (ZL4 p);Elim (ZL4 q); Intros h H1 i H2; -Rewrite H1;Rewrite H2; Simpl;Unfold lt; Apply le_n_S; Apply le_minus. +intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1; + rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; + apply le_minus. Qed. -Lemma ZL17: (p,q:positive)(lt (convert p) (convert (add p q))). +Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q). Proof. -Intros p q; Rewrite convert_add;Unfold lt;Elim (ZL4 q); Intros k H;Rewrite H; -Rewrite plus_sym;Simpl; Apply le_n_S; Apply le_plus_r. +intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q); + intros k H; rewrite H; rewrite plus_comm; simpl in |- *; + apply le_n_S; apply le_plus_r. Qed. (** Comparison and subtraction *) -Lemma compare_true_sub_right : - (p,q,z:positive) - (compare q p EGAL)=INFERIEUR-> - (compare z p EGAL)=SUPERIEUR-> - (compare z q EGAL)=SUPERIEUR-> - (compare (true_sub z p) (true_sub z q) EGAL)=INFERIEUR. -Proof. -Intros; Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Apply simpl_lt_plus_l with p:=(convert q); Rewrite le_plus_minus_r; [ - Rewrite plus_sym; Apply simpl_lt_plus_l with p:=(convert p); - Rewrite plus_assoc_l; Rewrite le_plus_minus_r; [ - Rewrite (plus_sym (convert p)); Apply lt_reg_l; - Apply compare_convert_INFERIEUR; Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR; - Apply ZC1; Assumption ] - | Apply lt_le_weak;Apply compare_convert_INFERIEUR; - Apply ZC1; Assumption ] - | Assumption ] - | Assumption ]. -Qed. - -Lemma compare_true_sub_left : - (p,q,z:positive) - (compare q p EGAL)=INFERIEUR-> - (compare p z EGAL)=SUPERIEUR-> - (compare q z EGAL)=SUPERIEUR-> - (compare (true_sub q z) (true_sub p z) EGAL)=INFERIEUR. -Proof. -Intros p q z; Intros; - Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Unfold gt; Apply simpl_lt_plus_l with p:=(convert z); - Rewrite le_plus_minus_r; [ - Rewrite le_plus_minus_r; [ - Apply compare_convert_INFERIEUR;Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1;Assumption] - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1; Assumption] - | Assumption] -| Assumption]. +Lemma Pcompare_minus_r : + forall p q r:positive, + (q ?= p)%positive Eq = Lt -> + (r ?= p)%positive Eq = Gt -> + (r ?= q)%positive Eq = Gt -> (r - p ?= r - q)%positive Eq = Lt. +Proof. +intros; apply nat_of_P_lt_Lt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; + [ rewrite nat_of_P_minus_morphism; + [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r; + [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p); + rewrite plus_assoc; rewrite le_plus_minus_r; + [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l; + apply nat_of_P_lt_Lt_compare_morphism; + assumption + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + apply ZC1; assumption ] + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; + assumption ] + | assumption ] + | assumption ]. +Qed. + +Lemma Pcompare_minus_l : + forall p q r:positive, + (q ?= p)%positive Eq = Lt -> + (p ?= r)%positive Eq = Gt -> + (q ?= r)%positive Eq = Gt -> (q - r ?= p - r)%positive Eq = Lt. +Proof. +intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; + [ rewrite nat_of_P_minus_morphism; + [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z); + rewrite le_plus_minus_r; + [ rewrite le_plus_minus_r; + [ apply nat_of_P_lt_Lt_compare_morphism; assumption + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + apply ZC1; assumption ] + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; + assumption ] + | assumption ] + | assumption ]. Qed. (** Distributivity of multiplication over subtraction *) -Theorem times_true_sub_distr: - (x,y,z:positive) (compare y z EGAL) = SUPERIEUR -> - (times x (true_sub y z)) = (true_sub (times x y) (times x z)). -Proof. -Intros x y z H; Apply convert_intro; -Rewrite times_convert; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Do 2 Rewrite times_convert; - Do 3 Rewrite (mult_sym (convert x));Apply mult_minus_distr - | Apply convert_compare_SUPERIEUR; Do 2 Rewrite times_convert; - Unfold gt; Elim (ZL4 x);Intros h H1;Rewrite H1; Apply lt_mult_left; - Exact (compare_convert_SUPERIEUR y z H) ] -| Assumption ]. +Theorem Pmult_minus_distr_l : + forall p q r:positive, + (q ?= r)%positive Eq = Gt -> + (p * (q - r))%positive = (p * q - p * r)%positive. +Proof. +intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism; + rewrite nat_of_P_minus_morphism; + [ rewrite nat_of_P_minus_morphism; + [ do 2 rewrite nat_of_P_mult_morphism; + do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r + | apply nat_of_P_gt_Gt_compare_complement_morphism; + do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; + elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l; + exact (nat_of_P_gt_Gt_compare_morphism y z H) ] + | assumption ]. Qed. - |