diff options
Diffstat (limited to 'theories/Arith')
| -rwxr-xr-x | theories/Arith/Arith.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Between.v | 204 | ||||
| -rw-r--r-- | theories/Arith/Bool_nat.v | 36 | ||||
| -rwxr-xr-x | theories/Arith/Compare.v | 43 | ||||
| -rwxr-xr-x | theories/Arith/Compare_dec.v | 104 | ||||
| -rw-r--r-- | theories/Arith/Div2.v | 185 | ||||
| -rwxr-xr-x | theories/Arith/EqNat.v | 91 | ||||
| -rw-r--r-- | theories/Arith/Euclid.v | 93 | ||||
| -rw-r--r-- | theories/Arith/Even.v | 433 | ||||
| -rw-r--r-- | theories/Arith/Factorial.v | 53 | ||||
| -rwxr-xr-x | theories/Arith/Gt.v | 123 | ||||
| -rwxr-xr-x | theories/Arith/Le.v | 106 | ||||
| -rwxr-xr-x | theories/Arith/Lt.v | 145 | ||||
| -rwxr-xr-x | theories/Arith/Max.v | 70 | ||||
| -rwxr-xr-x | theories/Arith/Min.v | 71 | ||||
| -rwxr-xr-x | theories/Arith/Minus.v | 121 | ||||
| -rwxr-xr-x | theories/Arith/Mult.v | 223 | ||||
| -rwxr-xr-x | theories/Arith/Peano_dec.v | 26 | ||||
| -rwxr-xr-x | theories/Arith/Plus.v | 187 | ||||
| -rwxr-xr-x | theories/Arith/Wf_nat.v | 222 |
20 files changed, 1257 insertions, 1281 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 832ea7a427..dbbb3403e2 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -18,4 +18,4 @@ Require Export Between. Require Export Minus. Require Export Peano_dec. Require Export Compare_dec. -Require Export Factorial. +Require Export Factorial.
\ No newline at end of file diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 14b2453358..665f96c684 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -8,178 +8,182 @@ (*i $Id$ i*) -Require Le. -Require Lt. +Require Import Le. +Require Import Lt. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type k,l,p,q,r:nat. +Implicit Types k l p q r : nat. Section Between. -Variables P,Q : nat -> Prop. +Variables P Q : nat -> Prop. -Inductive between [k:nat] : nat -> Prop - := bet_emp : (between k k) - | bet_S : (l:nat)(between k l)->(P l)->(between k (S l)). +Inductive between k : nat -> Prop := + | bet_emp : between k k + | bet_S : forall l, between k l -> P l -> between k (S l). -Hint constr_between : arith v62 := Constructors between. +Hint Constructors between: arith v62. -Lemma bet_eq : (k,l:nat)(l=k)->(between k l). +Lemma bet_eq : forall k l, l = k -> between k l. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Hints Resolve bet_eq : arith v62. +Hint Resolve bet_eq: arith v62. -Lemma between_le : (k,l:nat)(between k l)->(le k l). +Lemma between_le : forall k l, between k l -> k <= l. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Hints Immediate between_le : arith v62. +Hint Immediate between_le: arith v62. -Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l). +Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. Proof. -NewInduction 1. -Intros; Absurd (le (S k) k); Auto with arith. -NewDestruct H; Auto with arith. +induction 1. +intros; absurd (S k <= k); auto with arith. +destruct H; auto with arith. Qed. -Hints Resolve between_Sk_l : arith v62. +Hint Resolve between_Sk_l: arith v62. -Lemma between_restr : - (k,l,m:nat)(le k l)->(le l m)->(between k m)->(between l m). +Lemma between_restr : + forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Inductive exists [k:nat] : nat -> Prop - := exists_S : (l:nat)(exists k l)->(exists k (S l)) - | exists_le: (l:nat)(le k l)->(Q l)->(exists k (S l)). +Inductive exists_between k : nat -> Prop := + | exists_S : forall l, exists_between k l -> exists_between k (S l) + | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). -Hint constr_exists : arith v62 := Constructors exists. +Hint Constructors exists_between: arith v62. -Lemma exists_le_S : (k,l:nat)(exists k l)->(le (S k) l). +Lemma exists_le_S : forall k l, exists_between k l -> S k <= l. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Lemma exists_lt : (k,l:nat)(exists k l)->(lt k l). +Lemma exists_lt : forall k l, exists_between k l -> k < l. Proof exists_le_S. -Hints Immediate exists_le_S exists_lt : arith v62. +Hint Immediate exists_le_S exists_lt: arith v62. -Lemma exists_S_le : (k,l:nat)(exists k (S l))->(le k l). +Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l. Proof. -Intros; Apply le_S_n; Auto with arith. +intros; apply le_S_n; auto with arith. Qed. -Hints Immediate exists_S_le : arith v62. +Hint Immediate exists_S_le: arith v62. -Definition in_int := [p,q,r:nat](le p r)/\(lt r q). +Definition in_int p q r := p <= r /\ r < q. -Lemma in_int_intro : (p,q,r:nat)(le p r)->(lt r q)->(in_int p q r). +Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r. Proof. -Red; Auto with arith. +red in |- *; auto with arith. Qed. -Hints Resolve in_int_intro : arith v62. +Hint Resolve in_int_intro: arith v62. -Lemma in_int_lt : (p,q,r:nat)(in_int p q r)->(lt p q). +Lemma in_int_lt : forall p q r, in_int p q r -> p < q. Proof. -NewInduction 1; Intros. -Apply le_lt_trans with r; Auto with arith. +induction 1; intros. +apply le_lt_trans with r; auto with arith. Qed. -Lemma in_int_p_Sq : - (p,q,r:nat)(in_int p (S q) r)->((in_int p q r) \/ <nat>r=q). +Lemma in_int_p_Sq : + forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat. Proof. -NewInduction 1; Intros. -Elim (le_lt_or_eq r q); Auto with arith. +induction 1; intros. +elim (le_lt_or_eq r q); auto with arith. Qed. -Lemma in_int_S : (p,q,r:nat)(in_int p q r)->(in_int p (S q) r). +Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r. Proof. -NewInduction 1;Auto with arith. +induction 1; auto with arith. Qed. -Hints Resolve in_int_S : arith v62. +Hint Resolve in_int_S: arith v62. -Lemma in_int_Sp_q : (p,q,r:nat)(in_int (S p) q r)->(in_int p q r). +Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Hints Immediate in_int_Sp_q : arith v62. +Hint Immediate in_int_Sp_q: arith v62. -Lemma between_in_int : (k,l:nat)(between k l)->(r:nat)(in_int k l r)->(P r). +Lemma between_in_int : + forall k l, between k l -> forall r, in_int k l r -> P r. Proof. -NewInduction 1; Intros. -Absurd (lt k k); Auto with arith. -Apply in_int_lt with r; Auto with arith. -Elim (in_int_p_Sq k l r); Intros; Auto with arith. -Rewrite H2; Trivial with arith. +induction 1; intros. +absurd (k < k); auto with arith. +apply in_int_lt with r; auto with arith. +elim (in_int_p_Sq k l r); intros; auto with arith. +rewrite H2; trivial with arith. Qed. -Lemma in_int_between : - (k,l:nat)(le k l)->((r:nat)(in_int k l r)->(P r))->(between k l). +Lemma in_int_between : + forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Lemma exists_in_int : - (k,l:nat)(exists k l)->(EX m:nat | (in_int k l m) & (Q m)). +Lemma exists_in_int : + forall k l, exists_between k l -> exists2 m : nat | in_int k l m & Q m. Proof. -NewInduction 1. -Case IHexists; Intros p inp Qp; Exists p; Auto with arith. -Exists l; Auto with arith. +induction 1. +case IHexists_between; intros p inp Qp; exists p; auto with arith. +exists l; auto with arith. Qed. -Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l). +Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l. Proof. -NewDestruct 1; Intros. -Elim H0; Auto with arith. +destruct 1; intros. +elim H0; auto with arith. Qed. -Lemma between_or_exists : - (k,l:nat)(le k l)->((n:nat)(in_int k l n)->((P n)\/(Q n))) - ->((between k l)\/(exists k l)). +Lemma between_or_exists : + forall k l, + k <= l -> + (forall n:nat, in_int k l n -> P n \/ Q n) -> + between k l \/ exists_between k l. Proof. -NewInduction 1; Intros; Auto with arith. -Elim IHle; Intro; Auto with arith. -Elim (H0 m); Auto with arith. +induction 1; intros; auto with arith. +elim IHle; intro; auto with arith. +elim (H0 m); auto with arith. Qed. -Lemma between_not_exists : (k,l:nat)(between k l)-> - ((n:nat)(in_int k l n) -> (P n) -> ~(Q n)) - -> ~(exists k l). +Lemma between_not_exists : + forall k l, + between k l -> + (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. Proof. -NewInduction 1; Red; Intros. -Absurd (lt k k); Auto with arith. -Absurd (Q l); Auto with arith. -Elim (exists_in_int k (S l)); Auto with arith; Intros l' inl' Ql'. -Replace l with l'; Auto with arith. -Elim inl'; Intros. -Elim (le_lt_or_eq l' l); Auto with arith; Intros. -Absurd (exists k l); Auto with arith. -Apply in_int_exists with l'; Auto with arith. +induction 1; red in |- *; intros. +absurd (k < k); auto with arith. +absurd (Q l); auto with arith. +elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'. +replace l with l'; auto with arith. +elim inl'; intros. +elim (le_lt_or_eq l' l); auto with arith; intros. +absurd (exists_between k l); auto with arith. +apply in_int_exists with l'; auto with arith. Qed. -Inductive P_nth [init:nat] : nat->nat->Prop - := nth_O : (P_nth init init O) - | nth_S : (k,l:nat)(n:nat)(P_nth init k n)->(between (S k) l) - ->(Q l)->(P_nth init l (S n)). +Inductive P_nth (init:nat) : nat -> nat -> Prop := + | nth_O : P_nth init init 0 + | nth_S : + forall k l (n:nat), + P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n). -Lemma nth_le : (init,l,n:nat)(P_nth init l n)->(le init l). +Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l. Proof. -NewInduction 1; Intros; Auto with arith. -Apply le_trans with (S k); Auto with arith. +induction 1; intros; auto with arith. +apply le_trans with (S k); auto with arith. Qed. -Definition eventually := [n:nat](EX k:nat | (le k n) & (Q k)). +Definition eventually (n:nat) := exists2 k : nat | k <= n & Q k. -Lemma event_O : (eventually O)->(Q O). +Lemma event_O : eventually 0 -> Q 0. Proof. -NewInduction 1; Intros. -Replace O with x; Auto with arith. +induction 1; intros. +replace 0 with x; auto with arith. Qed. End Between. -Hints Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le - in_int_S in_int_intro : arith v62. -Hints Immediate in_int_Sp_q exists_le_S exists_S_le : arith v62. +Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le + in_int_S in_int_intro: arith v62. +Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
\ No newline at end of file diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index f9f6eeb19b..8b1b3a8c20 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -10,34 +10,30 @@ Require Export Compare_dec. Require Export Peano_dec. -Require Sumbool. +Require Import Sumbool. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,x,y:nat. +Implicit Types m n x y : nat. (** The decidability of equality and order relations over type [nat] give some boolean functions with the adequate specification. *) -Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)). -Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} := - [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)). +Definition notzerop n := sumbool_not _ _ (zerop n). +Definition lt_ge_dec : forall x y, {x < y} + {x >= y} := + fun n m => sumbool_not _ _ (le_lt_dec m n). -Definition nat_lt_ge_bool := - [x,y:nat](bool_of_sumbool (lt_ge_dec x y)). -Definition nat_ge_lt_bool := - [x,y:nat](bool_of_sumbool (sumbool_not ? ? (lt_ge_dec x y))). +Definition nat_lt_ge_bool x y := bool_of_sumbool (lt_ge_dec x y). +Definition nat_ge_lt_bool x y := + bool_of_sumbool (sumbool_not _ _ (lt_ge_dec x y)). -Definition nat_le_gt_bool := - [x,y:nat](bool_of_sumbool (le_gt_dec x y)). -Definition nat_gt_le_bool := - [x,y:nat](bool_of_sumbool (sumbool_not ? ? (le_gt_dec x y))). +Definition nat_le_gt_bool x y := bool_of_sumbool (le_gt_dec x y). +Definition nat_gt_le_bool x y := + bool_of_sumbool (sumbool_not _ _ (le_gt_dec x y)). -Definition nat_eq_bool := - [x,y:nat](bool_of_sumbool (eq_nat_dec x y)). -Definition nat_noteq_bool := - [x,y:nat](bool_of_sumbool (sumbool_not ? ? (eq_nat_dec x y))). +Definition nat_eq_bool x y := bool_of_sumbool (eq_nat_dec x y). +Definition nat_noteq_bool x y := + bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)). -Definition zerop_bool := [x:nat](bool_of_sumbool (zerop x)). -Definition notzerop_bool := [x:nat](bool_of_sumbool (notzerop x)). +Definition zerop_bool x := bool_of_sumbool (zerop x). +Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 88055f11e9..b5afebd94a 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -9,7 +9,6 @@ (*i $Id$ i*) (** Equality is decidable on [nat] *) -V7only [Import nat_scope.]. Open Local Scope nat_scope. (* @@ -19,42 +18,42 @@ Hints Immediate not_eq_sym : arith. *) Notation not_eq_sym := sym_not_eq. -Implicit Variables Type m,n,p,q:nat. +Implicit Types m n p q : nat. -Require Arith. -Require Peano_dec. -Require Compare_dec. +Require Import Arith. +Require Import Peano_dec. +Require Import Compare_dec. Definition le_or_le_S := le_le_S_dec. -Definition compare := gt_eq_gt_dec. +Definition Pcompare := gt_eq_gt_dec. -Lemma le_dec : (n,m:nat) {le n m} + {le m n}. +Lemma le_dec : forall n m, {n <= m} + {m <= n}. Proof le_ge_dec. -Definition lt_or_eq := [n,m:nat]{(gt m n)}+{n=m}. +Definition lt_or_eq n m := {m > n} + {n = m}. -Lemma le_decide : (n,m:nat)(le n m)->(lt_or_eq n m). +Lemma le_decide : forall n m, n <= m -> lt_or_eq n m. Proof le_lt_eq_dec. -Lemma le_le_S_eq : (p,q:nat)(le p q)->((le (S p) q)\/(p=q)). +Lemma le_le_S_eq : forall n m, n <= m -> S n <= m \/ n = m. Proof le_lt_or_eq. (* By special request of G. Kahn - Used in Group Theory *) -Lemma discrete_nat : (m, n: nat) (lt m n) -> - (S m) = n \/ (EX r: nat | n = (S (S (plus m r)))). +Lemma discrete_nat : + forall n m, n < m -> S n = m \/ ( exists r : nat | m = S (S (n + r))). Proof. -Intros m n H. -LApply (lt_le_S m n); Auto with arith. -Intro H'; LApply (le_lt_or_eq (S m) n); Auto with arith. -NewInduction 1; Auto with arith. -Right; Exists (minus n (S (S m))); Simpl. -Rewrite (plus_sym m (minus n (S (S m)))). -Rewrite (plus_n_Sm (minus n (S (S m))) m). -Rewrite (plus_n_Sm (minus n (S (S m))) (S m)). -Rewrite (plus_sym (minus n (S (S m))) (S (S m))); Auto with arith. +intros m n H. +lapply (lt_le_S m n); auto with arith. +intro H'; lapply (le_lt_or_eq (S m) n); auto with arith. +induction 1; auto with arith. +right; exists (n - S (S m)); simpl in |- *. +rewrite (plus_comm m (n - S (S m))). +rewrite (plus_n_Sm (n - S (S m)) m). +rewrite (plus_n_Sm (n - S (S m)) (S m)). +rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith. Qed. Require Export Wf_nat. -Require Export Min. +Require Export Min.
\ No newline at end of file diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index a7cb9bd92c..d88d6f29b9 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -8,102 +8,100 @@ (*i $Id$ i*) -Require Le. -Require Lt. -Require Gt. -Require Decidable. +Require Import Le. +Require Import Lt. +Require Import Gt. +Require Import Decidable. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,x,y:nat. +Implicit Types m n x y : nat. -Definition zerop : (n:nat){n=O}+{lt O n}. -NewDestruct n; Auto with arith. +Definition zerop : forall n, {n = 0} + {0 < n}. +destruct n; auto with arith. Defined. -Definition lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}. +Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}. Proof. -NewInduction n; Destruct m; Auto with arith. -Intros m0; Elim (IHn m0); Auto with arith. -NewInduction 1; Auto with arith. +induction n; simple destruct m; auto with arith. +intros m0; elim (IHn m0); auto with arith. +induction 1; auto with arith. Defined. -Lemma gt_eq_gt_dec : (n,m:nat)({(gt m n)}+{n=m})+{(gt n m)}. +Lemma gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}. Proof lt_eq_lt_dec. -Lemma le_lt_dec : (n,m:nat) {le n m} + {lt m n}. +Lemma le_lt_dec : forall n m, {n <= m} + {m < n}. Proof. -NewInduction n. -Auto with arith. -NewInduction m. -Auto with arith. -Elim (IHn m); Auto with arith. +induction n. +auto with arith. +induction m. +auto with arith. +elim (IHn m); auto with arith. Defined. -Definition le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}. +Definition le_le_S_dec : forall n m, {n <= m} + {S m <= n}. Proof. -Exact le_lt_dec. +exact le_lt_dec. Defined. -Definition le_ge_dec : (n,m:nat) {le n m} + {ge n m}. +Definition le_ge_dec : forall n m, {n <= m} + {n >= m}. Proof. -Intros; Elim (le_lt_dec n m); Auto with arith. +intros; elim (le_lt_dec n m); auto with arith. Defined. -Definition le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}. +Definition le_gt_dec : forall n m, {n <= m} + {n > m}. Proof. -Exact le_lt_dec. +exact le_lt_dec. Defined. -Definition le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}). +Definition le_lt_eq_dec : forall n m, n <= m -> {n < m} + {n = m}. Proof. -Intros; Elim (lt_eq_lt_dec n m); Auto with arith. -Intros; Absurd (lt m n); Auto with arith. +intros; elim (lt_eq_lt_dec n m); auto with arith. +intros; absurd (m < n); auto with arith. Defined. (** Proofs of decidability *) -Theorem dec_le:(x,y:nat)(decidable (le x y)). -Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [ - Auto with arith -| Intro; Right; Apply gt_not_le; Assumption]. +Theorem dec_le : forall n m, decidable (n <= m). +intros x y; unfold decidable in |- *; elim (le_gt_dec x y); + [ auto with arith | intro; right; apply gt_not_le; assumption ]. Qed. -Theorem dec_lt:(x,y:nat)(decidable (lt x y)). -Intros x y; Unfold lt; Apply dec_le. +Theorem dec_lt : forall n m, decidable (n < m). +intros x y; unfold lt in |- *; apply dec_le. Qed. -Theorem dec_gt:(x,y:nat)(decidable (gt x y)). -Intros x y; Unfold gt; Apply dec_lt. +Theorem dec_gt : forall n m, decidable (n > m). +intros x y; unfold gt in |- *; apply dec_lt. Qed. -Theorem dec_ge:(x,y:nat)(decidable (ge x y)). -Intros x y; Unfold ge; Apply dec_le. +Theorem dec_ge : forall n m, decidable (n >= m). +intros x y; unfold ge in |- *; apply dec_le. Qed. -Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x). -Intros x y H; Elim (lt_eq_lt_dec x y); [ - Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption] -| Auto with arith]. +Theorem not_eq : forall n m, n <> m -> n < m \/ m < n. +intros x y H; elim (lt_eq_lt_dec x y); + [ intros H1; elim H1; + [ auto with arith | intros H2; absurd (x = y); assumption ] + | auto with arith ]. Qed. -Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y). -Intros x y H; Elim (le_gt_dec x y); - [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ]. +Theorem not_le : forall n m, ~ n <= m -> n > m. +intros x y H; elim (le_gt_dec x y); + [ intros H1; absurd (x <= y); assumption | trivial with arith ]. Qed. -Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y). -Intros x y H; Elim (le_gt_dec x y); - [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption]. +Theorem not_gt : forall n m, ~ n > m -> n <= m. +intros x y H; elim (le_gt_dec x y); + [ trivial with arith | intros H1; absurd (x > y); assumption ]. Qed. -Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y). -Intros x y H; Exact (not_le y x H). +Theorem not_ge : forall n m, ~ n >= m -> n < m. +intros x y H; exact (not_le y x H). Qed. -Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y). -Intros x y H; Exact (not_gt y x H). +Theorem not_lt : forall n m, ~ n < m -> n >= m. +intros x y H; exact (not_gt y x H). Qed. - diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 9ab8fc820e..911b0b3861 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -8,153 +8,155 @@ (*i $Id$ i*) -Require Lt. -Require Plus. -Require Compare_dec. -Require Even. +Require Import Lt. +Require Import Plus. +Require Import Compare_dec. +Require Import Even. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type n:nat. +Implicit Type n : nat. (** Here we define [n/2] and prove some of its properties *) -Fixpoint div2 [n:nat] : nat := - Cases n of - O => O - | (S O) => O - | (S (S n')) => (S (div2 n')) +Fixpoint div2 n : nat := + match n with + | O => 0 + | S O => 0 + | S (S n') => S (div2 n') end. (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is useful to prove the corresponding induction principle *) -Lemma ind_0_1_SS : (P:nat->Prop) - (P O) -> (P (S O)) -> ((n:nat)(P n)->(P (S (S n)))) -> (n:nat)(P n). +Lemma ind_0_1_SS : + forall P:nat -> Prop, + P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. Proof. -Intros. -Cut (n:nat)(P n)/\(P (S n)). -Intros. Elim (H2 n). Auto with arith. +intros. +cut (forall n, P n /\ P (S n)). +intros. elim (H2 n). auto with arith. -NewInduction n0. Auto with arith. -Intros. Elim IHn0; Auto with arith. +induction n0. auto with arith. +intros. elim IHn0; auto with arith. Qed. (** [0 <n => n/2 < n] *) -Lemma lt_div2 : (n:nat) (lt O n) -> (lt (div2 n) n). +Lemma lt_div2 : forall n, 0 < n -> div2 n < n. Proof. -Intro n. Pattern n. Apply ind_0_1_SS. -Intro. Inversion H. -Auto with arith. -Intros. Simpl. -Case (zerop n0). -Intro. Rewrite e. Auto with arith. -Auto with arith. +intro n. pattern n in |- *. apply ind_0_1_SS. +intro. inversion H. +auto with arith. +intros. simpl in |- *. +case (zerop n0). +intro. rewrite e. auto with arith. +auto with arith. Qed. -Hints Resolve lt_div2 : arith. +Hint Resolve lt_div2: arith. (** Properties related to the parity *) -Lemma even_odd_div2 : (n:nat) - ((even n)<->(div2 n)=(div2 (S n))) /\ ((odd n)<->(S (div2 n))=(div2 (S n))). +Lemma even_odd_div2 : + forall n, + (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)). Proof. -Intro n. Pattern n. Apply ind_0_1_SS. +intro n. pattern n in |- *. apply ind_0_1_SS. (* n = 0 *) -Split. Split; Auto with arith. -Split. Intro H. Inversion H. -Intro H. Absurd (S (div2 O))=(div2 (S O)); Auto with arith. +split. split; auto with arith. +split. intro H. inversion H. +intro H. absurd (S (div2 0) = div2 1); auto with arith. (* n = 1 *) -Split. Split. Intro. Inversion H. Inversion H1. -Intro H. Absurd (div2 (S O))=(div2 (S (S O))). -Simpl. Discriminate. Assumption. -Split; Auto with arith. +split. split. intro. inversion H. inversion H1. +intro H. absurd (div2 1 = div2 2). +simpl in |- *. discriminate. assumption. +split; auto with arith. (* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H0 H1. -Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. -Split; Split; Auto with arith. -Intro H. Inversion H. Inversion H1. -Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith. -Intro H. Inversion H. Inversion H1. -Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith. +intros. decompose [and] H. unfold iff in H0, H1. +decompose [and] H0. decompose [and] H1. clear H H0 H1. +split; split; auto with arith. +intro H. inversion H. inversion H1. +change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith. +intro H. inversion H. inversion H1. +change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith. Qed. (** Specializations *) -Lemma even_div2 : (n:nat) (even n) -> (div2 n)=(div2 (S n)). -Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_div2 n))). +Lemma even_div2 : forall n, even n -> div2 n = div2 (S n). +Proof fun n => proj1 (proj1 (even_odd_div2 n)). -Lemma div2_even : (n:nat) (div2 n)=(div2 (S n)) -> (even n). -Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_div2 n))). +Lemma div2_even : forall n, div2 n = div2 (S n) -> even n. +Proof fun n => proj2 (proj1 (even_odd_div2 n)). -Lemma odd_div2 : (n:nat) (odd n) -> (S (div2 n))=(div2 (S n)). -Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_div2 n))). +Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n). +Proof fun n => proj1 (proj2 (even_odd_div2 n)). -Lemma div2_odd : (n:nat) (S (div2 n))=(div2 (S n)) -> (odd n). -Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_div2 n))). +Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n. +Proof fun n => proj2 (proj2 (even_odd_div2 n)). -Hints Resolve even_div2 div2_even odd_div2 div2_odd : arith. +Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. (** Properties related to the double ([2n]) *) -Definition double := [n:nat](plus n n). +Definition double n := n + n. -Hints Unfold double : arith. +Hint Unfold double: arith. -Lemma double_S : (n:nat) (double (S n))=(S (S (double n))). +Lemma double_S : forall n, double (S n) = S (S (double n)). Proof. -Intro. Unfold double. Simpl. Auto with arith. +intro. unfold double in |- *. simpl in |- *. auto with arith. Qed. -Lemma double_plus : (m,n:nat) (double (plus m n))=(plus (double m) (double n)). +Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m. Proof. -Intros m n. Unfold double. -Do 2 Rewrite -> plus_assoc_r. Rewrite -> (plus_permute n). -Reflexivity. +intros m n. unfold double in |- *. +do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n). +reflexivity. Qed. -Hints Resolve double_S : arith. +Hint Resolve double_S: arith. -Lemma even_odd_double : (n:nat) - ((even n)<->n=(double (div2 n))) /\ ((odd n)<->n=(S (double (div2 n)))). +Lemma even_odd_double : + forall n, + (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). Proof. -Intro n. Pattern n. Apply ind_0_1_SS. +intro n. pattern n in |- *. apply ind_0_1_SS. (* n = 0 *) -Split; Split; Auto with arith. -Intro H. Inversion H. +split; split; auto with arith. +intro H. inversion H. (* n = 1 *) -Split; Split; Auto with arith. -Intro H. Inversion H. Inversion H1. +split; split; auto with arith. +intro H. inversion H. inversion H1. (* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H0 H1. -Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. -Split; Split. -Intro H. Inversion H. Inversion H1. -Simpl. Rewrite (double_S (div2 n0)). Auto with arith. -Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith. -Intro H. Inversion H. Inversion H1. -Simpl. Rewrite (double_S (div2 n0)). Auto with arith. -Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith. +intros. decompose [and] H. unfold iff in H0, H1. +decompose [and] H0. decompose [and] H1. clear H H0 H1. +split; split. +intro H. inversion H. inversion H1. +simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. +simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. +intro H. inversion H. inversion H1. +simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. +simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. Qed. (** Specializations *) -Lemma even_double : (n:nat) (even n) -> n=(double (div2 n)). -Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_double n))). +Lemma even_double : forall n, even n -> n = double (div2 n). +Proof fun n => proj1 (proj1 (even_odd_double n)). -Lemma double_even : (n:nat) n=(double (div2 n)) -> (even n). -Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_double n))). +Lemma double_even : forall n, n = double (div2 n) -> even n. +Proof fun n => proj2 (proj1 (even_odd_double n)). -Lemma odd_double : (n:nat) (odd n) -> n=(S (double (div2 n))). -Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_double n))). +Lemma odd_double : forall n, odd n -> n = S (double (div2 n)). +Proof fun n => proj1 (proj2 (even_odd_double n)). -Lemma double_odd : (n:nat) n=(S (double (div2 n))) -> (odd n). -Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_double n))). +Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n. +Proof fun n => proj2 (proj2 (even_odd_double n)). -Hints Resolve even_double double_even odd_double double_odd : arith. +Hint Resolve even_double double_even odd_double double_odd: arith. (** Application: - if [n] is even then there is a [p] such that [n = 2p] @@ -162,13 +164,12 @@ Hints Resolve even_double double_even odd_double double_odd : arith. (Immediate: it is [n/2]) *) -Lemma even_2n : (n:nat) (even n) -> { p:nat | n=(double p) }. +Lemma even_2n : forall n, even n -> {p : nat | n = double p}. Proof. -Intros n H. Exists (div2 n). Auto with arith. +intros n H. exists (div2 n). auto with arith. Qed. -Lemma odd_S2n : (n:nat) (odd n) -> { p:nat | n=(S (double p)) }. +Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}. Proof. -Intros n H. Exists (div2 n). Auto with arith. +intros n H. exists (div2 n). auto with arith. Qed. - diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index a0ba5127da..f1246ceaf3 100755 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -10,69 +10,68 @@ (** Equality on natural numbers *) -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,x,y:nat. +Implicit Types m n x y : nat. -Fixpoint eq_nat [n:nat] : nat -> Prop := - [m:nat]Cases n m of - O O => True - | O (S _) => False - | (S _) O => False - | (S n1) (S m1) => (eq_nat n1 m1) - end. +Fixpoint eq_nat n m {struct n} : Prop := + match n, m with + | O, O => True + | O, S _ => False + | S _, O => False + | S n1, S m1 => eq_nat n1 m1 + end. -Theorem eq_nat_refl : (n:nat)(eq_nat n n). -NewInduction n; Simpl; Auto. +Theorem eq_nat_refl : forall n, eq_nat n n. +induction n; simpl in |- *; auto. Qed. -Hints Resolve eq_nat_refl : arith v62. +Hint Resolve eq_nat_refl: arith v62. -Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m). -NewInduction 1; Trivial with arith. +Theorem eq_eq_nat : forall n m, n = m -> eq_nat n m. +induction 1; trivial with arith. Qed. -Hints Immediate eq_eq_nat : arith v62. +Hint Immediate eq_eq_nat: arith v62. -Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m). -NewInduction n; NewInduction m; Simpl; Contradiction Orelse Auto with arith. +Theorem eq_nat_eq : forall n m, eq_nat n m -> n = m. +induction n; induction m; simpl in |- *; contradiction || auto with arith. Qed. -Hints Immediate eq_nat_eq : arith v62. +Hint Immediate eq_nat_eq: arith v62. -Theorem eq_nat_elim : (n:nat)(P:nat->Prop)(P n)->(m:nat)(eq_nat n m)->(P m). -Intros; Replace m with n; Auto with arith. +Theorem eq_nat_elim : + forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. +intros; replace m with n; auto with arith. Qed. -Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}. -NewInduction n. -NewDestruct m. -Auto with arith. -Intros; Right; Red; Trivial with arith. -NewDestruct m. -Right; Red; Auto with arith. -Intros. -Simpl. -Apply IHn. +Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. +induction n. +destruct m as [| n]. +auto with arith. +intros; right; red in |- *; trivial with arith. +destruct m as [| n0]. +right; red in |- *; auto with arith. +intros. +simpl in |- *. +apply IHn. Defined. -Fixpoint beq_nat [n:nat] : nat -> bool := - [m:nat]Cases n m of - O O => true - | O (S _) => false - | (S _) O => false - | (S n1) (S m1) => (beq_nat n1 m1) - end. +Fixpoint beq_nat n m {struct n} : bool := + match n, m with + | O, O => true + | O, S _ => false + | S _, O => false + | S n1, S m1 => beq_nat n1 m1 + end. -Lemma beq_nat_refl : (x:nat)true=(beq_nat x x). +Lemma beq_nat_refl : forall n, true = beq_nat n n. Proof. - Intro x; NewInduction x; Simpl; Auto. + intro x; induction x; simpl in |- *; auto. Qed. -Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y. +Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y. Proof. - Double Induction x y; Simpl. - Reflexivity. - Intros; Discriminate H0. - Intros; Discriminate H0. - Intros; Case (H0 ? H1); Reflexivity. + double induction x y; simpl in |- *. + reflexivity. + intros; discriminate H0. + intros; discriminate H0. + intros; case (H0 _ H1); reflexivity. Defined. - diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index f64d932e76..02c48f028b 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -8,58 +8,61 @@ (*i $Id$ i*) -Require Mult. -Require Compare_dec. -Require Wf_nat. +Require Import Mult. +Require Import Compare_dec. +Require Import Wf_nat. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type a,b,n,q,r:nat. +Implicit Types a b n q r : nat. -Inductive diveucl [a,b:nat] : Set - := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b). +Inductive diveucl a b : Set := + divex : forall q r, b > r -> a = q * b + r -> diveucl a b. -Lemma eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b). -Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. -Elim (le_gt_dec b n). -Intro lebn. -Elim (H0 (minus n b)); Auto with arith. -Intros q r g e. -Apply divex with (S q) r; Simpl; Auto with arith. -Elim plus_assoc_l. -Elim e; Auto with arith. -Intros gtbn. -Apply divex with O n; Simpl; Auto with arith. +Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n. +intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. +elim (le_gt_dec b n). +intro lebn. +elim (H0 (n - b)); auto with arith. +intros q r g e. +apply divex with (S q) r; simpl in |- *; auto with arith. +elim plus_assoc. +elim e; auto with arith. +intros gtbn. +apply divex with 0 n; simpl in |- *; auto with arith. Qed. -Lemma quotient : (b:nat)(gt b O)-> - (a:nat){q:nat|(EX r:nat | (a=(plus (mult q b) r))/\(gt b r))}. -Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. -Elim (le_gt_dec b n). -Intro lebn. -Elim (H0 (minus n b)); Auto with arith. -Intros q Hq; Exists (S q). -Elim Hq; Intros r Hr. -Exists r; Simpl; Elim Hr; Intros. -Elim plus_assoc_l. -Elim H1; Auto with arith. -Intros gtbn. -Exists O; Exists n; Simpl; Auto with arith. +Lemma quotient : + forall n, + n > 0 -> + forall m:nat, {q : nat | exists r : nat | m = q * n + r /\ n > r}. +intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. +elim (le_gt_dec b n). +intro lebn. +elim (H0 (n - b)); auto with arith. +intros q Hq; exists (S q). +elim Hq; intros r Hr. +exists r; simpl in |- *; elim Hr; intros. +elim plus_assoc. +elim H1; auto with arith. +intros gtbn. +exists 0; exists n; simpl in |- *; auto with arith. Qed. -Lemma modulo : (b:nat)(gt b O)-> - (a:nat){r:nat|(EX q:nat | (a=(plus (mult q b) r))/\(gt b r))}. -Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. -Elim (le_gt_dec b n). -Intro lebn. -Elim (H0 (minus n b)); Auto with arith. -Intros r Hr; Exists r. -Elim Hr; Intros q Hq. -Elim Hq; Intros; Exists (S q); Simpl. -Elim plus_assoc_l. -Elim H1; Auto with arith. -Intros gtbn. -Exists n; Exists O; Simpl; Auto with arith. -Qed. +Lemma modulo : + forall n, + n > 0 -> + forall m:nat, {r : nat | exists q : nat | m = q * n + r /\ n > r}. +intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. +elim (le_gt_dec b n). +intro lebn. +elim (H0 (n - b)); auto with arith. +intros r Hr; exists r. +elim Hr; intros q Hq. +elim Hq; intros; exists (S q); simpl in |- *. +elim plus_assoc. +elim H1; auto with arith. +intros gtbn. +exists n; exists 0; simpl in |- *; auto with arith. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 88ad1851bc..0017a464b0 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -12,299 +12,294 @@ and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2. *) -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n:nat. +Implicit Types m n : nat. -Inductive even : nat->Prop := - even_O : (even O) - | even_S : (n:nat)(odd n)->(even (S n)) -with odd : nat->Prop := - odd_S : (n:nat)(even n)->(odd (S n)). +Inductive even : nat -> Prop := + | even_O : even 0 + | even_S : forall n, odd n -> even (S n) +with odd : nat -> Prop := + odd_S : forall n, even n -> odd (S n). -Hint constr_even : arith := Constructors even. -Hint constr_odd : arith := Constructors odd. +Hint Constructors even: arith. +Hint Constructors odd: arith. -Lemma even_or_odd : (n:nat) (even n)\/(odd n). +Lemma even_or_odd : forall n, even n \/ odd n. Proof. -NewInduction n. -Auto with arith. -Elim IHn; Auto with arith. +induction n. +auto with arith. +elim IHn; auto with arith. Qed. -Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }. +Lemma even_odd_dec : forall n, {even n} + {odd n}. Proof. -NewInduction n. -Auto with arith. -Elim IHn; Auto with arith. +induction n. +auto with arith. +elim IHn; auto with arith. Qed. -Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False. +Lemma not_even_and_odd : forall n, even n -> odd n -> False. Proof. -NewInduction n. -Intros. Inversion H0. -Intros. Inversion H. Inversion H0. Auto with arith. +induction n. +intros. inversion H0. +intros. inversion H. inversion H0. auto with arith. Qed. -Lemma even_plus_aux: - (n,m:nat) - (iff (odd (plus n m)) (odd n) /\ (even m) \/ (even n) /\ (odd m)) /\ - (iff (even (plus n m)) (even n) /\ (even m) \/ (odd n) /\ (odd m)). +Lemma even_plus_aux : + forall n m, + (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\ + (even (n + m) <-> even n /\ even m \/ odd n /\ odd m). Proof. -Intros n; Elim n; Simpl; Auto with arith. -Intros m; Split; Auto. -Split. -Intros H; Right; Split; Auto with arith. -Intros H'; Case H'; Auto with arith. -Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1. -Intros H; Elim H; Auto. -Split; Auto with arith. -Intros H'; Elim H'; Auto with arith. -Intros H; Elim H; Auto. -Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1. -Intros n0 H' m; Elim (H' m); Intros H'1 H'2; Elim H'1; Intros E1 E2; Elim H'2; - Intros E3 E4; Clear H'1 H'2. -Split; Split. -Intros H'0; Case E3. -Inversion H'0; Auto. -Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith. -Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith. -Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2. -Apply odd_S. -Apply E4; Left; Split; Auto with arith. -Inversion C1; Auto. -Apply odd_S. -Apply E4; Right; Split; Auto with arith. -Inversion C1; Auto. -Intros H'0. -Case E1. -Inversion H'0; Auto. -Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith. -Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith. -Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2. -Apply even_S. -Apply E2; Left; Split; Auto with arith. -Inversion C1; Auto. -Apply even_S. -Apply E2; Right; Split; Auto with arith. -Inversion C1; Auto. +intros n; elim n; simpl in |- *; auto with arith. +intros m; split; auto. +split. +intros H; right; split; auto with arith. +intros H'; case H'; auto with arith. +intros H'0; elim H'0; intros H'1 H'2; inversion H'1. +intros H; elim H; auto. +split; auto with arith. +intros H'; elim H'; auto with arith. +intros H; elim H; auto. +intros H'0; elim H'0; intros H'1 H'2; inversion H'1. +intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2; + intros E3 E4; clear H'1 H'2. +split; split. +intros H'0; case E3. +inversion H'0; auto. +intros H; elim H; intros H0 H1; clear H; auto with arith. +intros H; elim H; intros H0 H1; clear H; auto with arith. +intros H'0; case H'0; intros C0; case C0; intros C1 C2. +apply odd_S. +apply E4; left; split; auto with arith. +inversion C1; auto. +apply odd_S. +apply E4; right; split; auto with arith. +inversion C1; auto. +intros H'0. +case E1. +inversion H'0; auto. +intros H; elim H; intros H0 H1; clear H; auto with arith. +intros H; elim H; intros H0 H1; clear H; auto with arith. +intros H'0; case H'0; intros C0; case C0; intros C1 C2. +apply even_S. +apply E2; left; split; auto with arith. +inversion C1; auto. +apply even_S. +apply E2; right; split; auto with arith. +inversion C1; auto. Qed. -Lemma even_even_plus : (n,m:nat) (even n) -> (even m) -> (even (plus n m)). +Lemma even_even_plus : forall n m, even n -> even m -> even (n + m). Proof. -Intros n m; Case (even_plus_aux n m). -Intros H H0; Case H0; Auto. +intros n m; case (even_plus_aux n m). +intros H H0; case H0; auto. Qed. -Lemma odd_even_plus : (n,m:nat) (odd n) -> (odd m) -> (even (plus n m)). +Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m). Proof. -Intros n m; Case (even_plus_aux n m). -Intros H H0; Case H0; Auto. +intros n m; case (even_plus_aux n m). +intros H H0; case H0; auto. Qed. -Lemma even_plus_even_inv_r : - (n,m:nat) (even (plus n m)) -> (even n) -> (even m). +Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'0. -Intros H'1; Case H'1; Auto. -Intros H0; Elim H0; Auto. -Intros H0 H1 H2; Case (not_even_and_odd n); Auto. -Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'0. +intros H'1; case H'1; auto. +intros H0; elim H0; auto. +intros H0 H1 H2; case (not_even_and_odd n); auto. +case H0; auto. Qed. -Lemma even_plus_even_inv_l : - (n,m:nat) (even (plus n m)) -> (even m) -> (even n). +Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'0. -Intros H'1; Case H'1; Auto. -Intros H0; Elim H0; Auto. -Intros H0 H1 H2; Case (not_even_and_odd m); Auto. -Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'0. +intros H'1; case H'1; auto. +intros H0; elim H0; auto. +intros H0 H1 H2; case (not_even_and_odd m); auto. +case H0; auto. Qed. -Lemma even_plus_odd_inv_r : (n,m:nat) (even (plus n m)) -> (odd n) -> (odd m). +Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'0. -Intros H'1; Case H'1; Auto. -Intros H0 H1 H2; Case (not_even_and_odd n); Auto. -Case H0; Auto. -Intros H0; Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'0. +intros H'1; case H'1; auto. +intros H0 H1 H2; case (not_even_and_odd n); auto. +case H0; auto. +intros H0; case H0; auto. Qed. -Lemma even_plus_odd_inv_l : (n,m:nat) (even (plus n m)) -> (odd m) -> (odd n). +Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'0. -Intros H'1; Case H'1; Auto. -Intros H0 H1 H2; Case (not_even_and_odd m); Auto. -Case H0; Auto. -Intros H0; Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'0. +intros H'1; case H'1; auto. +intros H0 H1 H2; case (not_even_and_odd m); auto. +case H0; auto. +intros H0; case H0; auto. Qed. -Hints Resolve even_even_plus odd_even_plus :arith. +Hint Resolve even_even_plus odd_even_plus: arith. -Lemma odd_plus_l : (n,m:nat) (odd n) -> (even m) -> (odd (plus n m)). +Lemma odd_plus_l : forall n m, odd n -> even m -> odd (n + m). Proof. -Intros n m; Case (even_plus_aux n m). -Intros H; Case H; Auto. +intros n m; case (even_plus_aux n m). +intros H; case H; auto. Qed. -Lemma odd_plus_r : (n,m:nat) (even n) -> (odd m) -> (odd (plus n m)). +Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m). Proof. -Intros n m; Case (even_plus_aux n m). -Intros H; Case H; Auto. +intros n m; case (even_plus_aux n m). +intros H; case H; auto. Qed. -Lemma odd_plus_even_inv_l : (n,m:nat) (odd (plus n m)) -> (odd m) -> (even n). +Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'. -Intros H'1; Case H'1; Auto. -Intros H0 H1 H2; Case (not_even_and_odd m); Auto. -Case H0; Auto. -Intros H0; Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'. +intros H'1; case H'1; auto. +intros H0 H1 H2; case (not_even_and_odd m); auto. +case H0; auto. +intros H0; case H0; auto. Qed. -Lemma odd_plus_even_inv_r : (n,m:nat) (odd (plus n m)) -> (odd n) -> (even m). +Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'. -Intros H'1; Case H'1; Auto. -Intros H0; Case H0; Auto. -Intros H0 H1 H2; Case (not_even_and_odd n); Auto. -Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'. +intros H'1; case H'1; auto. +intros H0; case H0; auto. +intros H0 H1 H2; case (not_even_and_odd n); auto. +case H0; auto. Qed. -Lemma odd_plus_odd_inv_l : (n,m:nat) (odd (plus n m)) -> (even m) -> (odd n). +Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'. -Intros H'1; Case H'1; Auto. -Intros H0; Case H0; Auto. -Intros H0 H1 H2; Case (not_even_and_odd m); Auto. -Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'. +intros H'1; case H'1; auto. +intros H0; case H0; auto. +intros H0 H1 H2; case (not_even_and_odd m); auto. +case H0; auto. Qed. -Lemma odd_plus_odd_inv_r : (n,m:nat) (odd (plus n m)) -> (even n) -> (odd m). +Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m. Proof. -Intros n m H; Case (even_plus_aux n m). -Intros H' H'0; Elim H'. -Intros H'1; Case H'1; Auto. -Intros H0 H1 H2; Case (not_even_and_odd n); Auto. -Case H0; Auto. -Intros H0; Case H0; Auto. +intros n m H; case (even_plus_aux n m). +intros H' H'0; elim H'. +intros H'1; case H'1; auto. +intros H0 H1 H2; case (not_even_and_odd n); auto. +case H0; auto. +intros H0; case H0; auto. Qed. -Hints Resolve odd_plus_l odd_plus_r :arith. +Hint Resolve odd_plus_l odd_plus_r: arith. Lemma even_mult_aux : - (n,m:nat) - (iff (odd (mult n m)) (odd n) /\ (odd m)) /\ - (iff (even (mult n m)) (even n) \/ (even m)). + forall n m, + (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). Proof. -Intros n; Elim n; Simpl; Auto with arith. -Intros m; Split; Split; Auto with arith. -Intros H'; Inversion H'. -Intros H'; Elim H'; Auto. -Intros n0 H' m; Split; Split; Auto with arith. -Intros H'0. -Elim (even_plus_aux m (mult n0 m)); Intros H'3 H'4; Case H'3; Intros H'1 H'2; - Case H'1; Auto. -Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith. -Split; Auto with arith. -Case (H' m). -Intros H'8 H'9; Case H'9. -Intros H'10; Case H'10; Auto with arith. -Intros H'11 H'12; Case (not_even_and_odd m); Auto with arith. -Intros H'5; Elim H'5; Intros H'6 H'7; Case (not_even_and_odd (mult n0 m)); Auto. -Case (H' m). -Intros H'8 H'9; Case H'9; Auto. -Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0. -Elim (even_plus_aux m (mult n0 m)); Auto. -Intros H'0 H'3. -Elim H'0. -Intros H'4 H'5; Apply H'5; Auto. -Left; Split; Auto with arith. -Case (H' m). -Intros H'6 H'7; Elim H'7. -Intros H'8 H'9; Apply H'9. -Left. -Inversion H'1; Auto. -Intros H'0. -Elim (even_plus_aux m (mult n0 m)); Intros H'3 H'4; Case H'4. -Intros H'1 H'2. -Elim H'1; Auto. -Intros H; Case H; Auto. -Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith. -Left. -Case (H' m). -Intros H'8; Elim H'8. -Intros H'9; Elim H'9; Auto with arith. -Intros H'0; Elim H'0; Intros H'1. -Case (even_or_odd m); Intros H'2. -Apply even_even_plus; Auto. -Case (H' m). -Intros H H0; Case H0; Auto. -Apply odd_even_plus; Auto. -Inversion H'1; Case (H' m); Auto. -Intros H1; Case H1; Auto. -Apply even_even_plus; Auto. -Case (H' m). -Intros H H0; Case H0; Auto. +intros n; elim n; simpl in |- *; auto with arith. +intros m; split; split; auto with arith. +intros H'; inversion H'. +intros H'; elim H'; auto. +intros n0 H' m; split; split; auto with arith. +intros H'0. +elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2; + case H'1; auto. +intros H'5; elim H'5; intros H'6 H'7; auto with arith. +split; auto with arith. +case (H' m). +intros H'8 H'9; case H'9. +intros H'10; case H'10; auto with arith. +intros H'11 H'12; case (not_even_and_odd m); auto with arith. +intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto. +case (H' m). +intros H'8 H'9; case H'9; auto. +intros H'0; elim H'0; intros H'1 H'2; clear H'0. +elim (even_plus_aux m (n0 * m)); auto. +intros H'0 H'3. +elim H'0. +intros H'4 H'5; apply H'5; auto. +left; split; auto with arith. +case (H' m). +intros H'6 H'7; elim H'7. +intros H'8 H'9; apply H'9. +left. +inversion H'1; auto. +intros H'0. +elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4. +intros H'1 H'2. +elim H'1; auto. +intros H; case H; auto. +intros H'5; elim H'5; intros H'6 H'7; auto with arith. +left. +case (H' m). +intros H'8; elim H'8. +intros H'9; elim H'9; auto with arith. +intros H'0; elim H'0; intros H'1. +case (even_or_odd m); intros H'2. +apply even_even_plus; auto. +case (H' m). +intros H H0; case H0; auto. +apply odd_even_plus; auto. +inversion H'1; case (H' m); auto. +intros H1; case H1; auto. +apply even_even_plus; auto. +case (H' m). +intros H H0; case H0; auto. Qed. -Lemma even_mult_l : (n,m:nat) (even n) -> (even (mult n m)). +Lemma even_mult_l : forall n m, even n -> even (n * m). Proof. -Intros n m; Case (even_mult_aux n m); Auto. -Intros H H0; Case H0; Auto. +intros n m; case (even_mult_aux n m); auto. +intros H H0; case H0; auto. Qed. -Lemma even_mult_r: (n,m:nat) (even m) -> (even (mult n m)). +Lemma even_mult_r : forall n m, even m -> even (n * m). Proof. -Intros n m; Case (even_mult_aux n m); Auto. -Intros H H0; Case H0; Auto. +intros n m; case (even_mult_aux n m); auto. +intros H H0; case H0; auto. Qed. -Hints Resolve even_mult_l even_mult_r :arith. +Hint Resolve even_mult_l even_mult_r: arith. -Lemma even_mult_inv_r: (n,m:nat) (even (mult n m)) -> (odd n) -> (even m). +Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m. Proof. -Intros n m H' H'0. -Case (even_mult_aux n m). -Intros H'1 H'2; Elim H'2. -Intros H'3; Elim H'3; Auto. -Intros H; Case (not_even_and_odd n); Auto. +intros n m H' H'0. +case (even_mult_aux n m). +intros H'1 H'2; elim H'2. +intros H'3; elim H'3; auto. +intros H; case (not_even_and_odd n); auto. Qed. -Lemma even_mult_inv_l : (n,m:nat) (even (mult n m)) -> (odd m) -> (even n). +Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n. Proof. -Intros n m H' H'0. -Case (even_mult_aux n m). -Intros H'1 H'2; Elim H'2. -Intros H'3; Elim H'3; Auto. -Intros H; Case (not_even_and_odd m); Auto. +intros n m H' H'0. +case (even_mult_aux n m). +intros H'1 H'2; elim H'2. +intros H'3; elim H'3; auto. +intros H; case (not_even_and_odd m); auto. Qed. -Lemma odd_mult : (n,m:nat) (odd n) -> (odd m) -> (odd (mult n m)). +Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m). Proof. -Intros n m; Case (even_mult_aux n m); Intros H; Case H; Auto. +intros n m; case (even_mult_aux n m); intros H; case H; auto. Qed. -Hints Resolve even_mult_l even_mult_r odd_mult :arith. +Hint Resolve even_mult_l even_mult_r odd_mult: arith. -Lemma odd_mult_inv_l : (n,m:nat) (odd (mult n m)) -> (odd n). +Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n. Proof. -Intros n m H'. -Case (even_mult_aux n m). -Intros H'1 H'2; Elim H'1. -Intros H'3; Elim H'3; Auto. +intros n m H'. +case (even_mult_aux n m). +intros H'1 H'2; elim H'1. +intros H'3; elim H'3; auto. Qed. -Lemma odd_mult_inv_r : (n,m:nat) (odd (mult n m)) -> (odd m). +Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m. Proof. -Intros n m H'. -Case (even_mult_aux n m). -Intros H'1 H'2; Elim H'1. -Intros H'3; Elim H'3; Auto. +intros n m H'. +case (even_mult_aux n m). +intros H'1 H'2; elim H'1. +intros H'3; elim H'3; auto. Qed. - diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 1d1ee00af6..69b55e0094 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -8,44 +8,43 @@ (*i $Id$ i*) -Require Plus. -Require Mult. -Require Lt. -V7only [Import nat_scope.]. +Require Import Plus. +Require Import Mult. +Require Import Lt. Open Local Scope nat_scope. (** Factorial *) -Fixpoint fact [n:nat]:nat:= - Cases n of - O => (S O) - |(S n) => (mult (S n) (fact n)) +Fixpoint fact (n:nat) : nat := + match n with + | O => 1 + | S n => S n * fact n end. -Arguments Scope fact [ nat_scope ]. +Arguments Scope fact [nat_scope]. -Lemma lt_O_fact : (n:nat)(lt O (fact n)). +Lemma lt_O_fact : forall n:nat, 0 < fact n. Proof. -Induction n; Unfold lt; Simpl; Auto with arith. +simple induction n; unfold lt in |- *; simpl in |- *; auto with arith. Qed. -Lemma fact_neq_0:(n:nat)~(fact n)=O. +Lemma fact_neq_0 : forall n:nat, fact n <> 0. Proof. -Intro. -Apply sym_not_eq. -Apply lt_O_neq. -Apply lt_O_fact. +intro. +apply sym_not_eq. +apply lt_O_neq. +apply lt_O_fact. Qed. -Lemma fact_growing : (n,m:nat) (le n m) -> (le (fact n) (fact m)). +Lemma fact_le : forall n m:nat, n <= m -> fact n <= fact m. Proof. -NewInduction 1. -Apply le_n. -Assert (le (mult (S O) (fact n)) (mult (S m) (fact m))). -Apply le_mult_mult. -Apply lt_le_S; Apply lt_O_Sn. -Assumption. -Simpl (mult (S O) (fact n)) in H0. -Rewrite <- plus_n_O in H0. -Assumption. -Qed. +induction 1. +apply le_n. +assert (1 * fact n <= S m * fact m). +apply mult_le_compat. +apply lt_le_S; apply lt_O_Sn. +assumption. +simpl (1 * fact n) in H0. +rewrite <- plus_n_O in H0. +assumption. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index ce4661df66..c0afdb0ae8 100755 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -8,142 +8,141 @@ (*i $Id$ i*) -Require Le. -Require Lt. -Require Plus. -V7only [Import nat_scope.]. +Require Import Le. +Require Import Lt. +Require Import Plus. Open Local Scope nat_scope. -Implicit Variables Type m,n,p:nat. +Implicit Types m n p : nat. (** Order and successor *) -Theorem gt_Sn_O : (n:nat)(gt (S n) O). +Theorem gt_Sn_O : forall n, S n > 0. Proof. - Auto with arith. + auto with arith. Qed. -Hints Resolve gt_Sn_O : arith v62. +Hint Resolve gt_Sn_O: arith v62. -Theorem gt_Sn_n : (n:nat)(gt (S n) n). +Theorem gt_Sn_n : forall n, S n > n. Proof. - Auto with arith. + auto with arith. Qed. -Hints Resolve gt_Sn_n : arith v62. +Hint Resolve gt_Sn_n: arith v62. -Theorem gt_n_S : (n,m:nat)(gt n m)->(gt (S n) (S m)). +Theorem gt_n_S : forall n m, n > m -> S n > S m. Proof. - Auto with arith. + auto with arith. Qed. -Hints Resolve gt_n_S : arith v62. +Hint Resolve gt_n_S: arith v62. -Lemma gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n). +Lemma gt_S_n : forall n m, S m > S n -> m > n. Proof. - Auto with arith. + auto with arith. Qed. -Hints Immediate gt_S_n : arith v62. +Hint Immediate gt_S_n: arith v62. -Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(m=n)). +Theorem gt_S : forall n m, S n > m -> n > m \/ m = n. Proof. - Intros n m H; Unfold gt; Apply le_lt_or_eq; Auto with arith. + intros n m H; unfold gt in |- *; apply le_lt_or_eq; auto with arith. Qed. -Lemma gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n). +Lemma gt_pred : forall n m, m > S n -> pred m > n. Proof. - Auto with arith. + auto with arith. Qed. -Hints Immediate gt_pred : arith v62. +Hint Immediate gt_pred: arith v62. (** Irreflexivity *) -Lemma gt_antirefl : (n:nat)~(gt n n). -Proof lt_n_n. -Hints Resolve gt_antirefl : arith v62. +Lemma gt_irrefl : forall n, ~ n > n. +Proof lt_irrefl. +Hint Resolve gt_irrefl: arith v62. (** Asymmetry *) -Lemma gt_not_sym : (n,m:nat)(gt n m) -> ~(gt m n). -Proof [n,m:nat](lt_not_sym m n). +Lemma gt_asym : forall n m, n > m -> ~ m > n. +Proof fun n m => lt_asym m n. -Hints Resolve gt_not_sym : arith v62. +Hint Resolve gt_asym: arith v62. (** Relating strict and large orders *) -Lemma le_not_gt : (n,m:nat)(le n m) -> ~(gt n m). +Lemma le_not_gt : forall n m, n <= m -> ~ n > m. Proof le_not_lt. -Hints Resolve le_not_gt : arith v62. +Hint Resolve le_not_gt: arith v62. -Lemma gt_not_le : (n,m:nat)(gt n m) -> ~(le n m). +Lemma gt_not_le : forall n m, n > m -> ~ n <= m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Resolve gt_not_le : arith v62. +Hint Resolve gt_not_le: arith v62. -Theorem le_S_gt : (n,m:nat)(le (S n) m)->(gt m n). +Theorem le_S_gt : forall n m, S n <= m -> m > n. Proof. - Auto with arith. + auto with arith. Qed. -Hints Immediate le_S_gt : arith v62. +Hint Immediate le_S_gt: arith v62. -Lemma gt_S_le : (n,p:nat)(gt (S p) n)->(le n p). +Lemma gt_S_le : forall n m, S m > n -> n <= m. Proof. - Intros n p; Exact (lt_n_Sm_le n p). + intros n p; exact (lt_n_Sm_le n p). Qed. -Hints Immediate gt_S_le : arith v62. +Hint Immediate gt_S_le: arith v62. -Lemma gt_le_S : (n,p:nat)(gt p n)->(le (S n) p). +Lemma gt_le_S : forall n m, m > n -> S n <= m. Proof. - Auto with arith. + auto with arith. Qed. -Hints Resolve gt_le_S : arith v62. +Hint Resolve gt_le_S: arith v62. -Lemma le_gt_S : (n,p:nat)(le n p)->(gt (S p) n). +Lemma le_gt_S : forall n m, n <= m -> S m > n. Proof. - Auto with arith. + auto with arith. Qed. -Hints Resolve le_gt_S : arith v62. +Hint Resolve le_gt_S: arith v62. (** Transitivity *) -Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p). +Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p. Proof. - Red; Intros; Apply lt_le_trans with m; Auto with arith. + red in |- *; intros; apply lt_le_trans with m; auto with arith. Qed. -Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p). +Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p. Proof. - Red; Intros; Apply le_lt_trans with m; Auto with arith. + red in |- *; intros; apply le_lt_trans with m; auto with arith. Qed. -Lemma gt_trans : (n,m,p:nat)(gt n m)->(gt m p)->(gt n p). +Lemma gt_trans : forall n m p, n > m -> m > p -> n > p. Proof. - Red; Intros n m p H1 H2. - Apply lt_trans with m; Auto with arith. + red in |- *; intros n m p H1 H2. + apply lt_trans with m; auto with arith. Qed. -Theorem gt_trans_S : (n,m,p:nat)(gt (S n) m)->(gt m p)->(gt n p). +Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p. Proof. - Red; Intros; Apply lt_le_trans with m; Auto with arith. + red in |- *; intros; apply lt_le_trans with m; auto with arith. Qed. -Hints Resolve gt_trans_S le_gt_trans gt_le_trans : arith v62. +Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. (** Comparison to 0 *) -Theorem gt_O_eq : (n:nat)((gt n O)\/(O=n)). +Theorem gt_O_eq : forall n, n > 0 \/ 0 = n. Proof. - Intro n ; Apply gt_S ; Auto with arith. + intro n; apply gt_S; auto with arith. Qed. (** Simplification and compatibility *) -Lemma simpl_gt_plus_l : (n,m,p:nat)(gt (plus p n) (plus p m))->(gt n m). +Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m. Proof. - Red; Intros n m p H; Apply simpl_lt_plus_l with p; Auto with arith. + red in |- *; intros n m p H; apply plus_lt_reg_l with p; auto with arith. Qed. -Lemma gt_reg_l : (n,m,p:nat)(gt n m)->(gt (plus p n) (plus p m)). +Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m. Proof. - Auto with arith. + auto with arith. Qed. -Hints Resolve gt_reg_l : arith v62. +Hint Resolve plus_gt_compat_l: arith v62.
\ No newline at end of file diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index c80689836e..d311046650 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -9,114 +9,114 @@ (*i $Id$ i*) (** Order on natural numbers *) -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,p:nat. +Implicit Types m n p : nat. (** Reflexivity *) -Theorem le_refl : (n:nat)(le n n). +Theorem le_refl : forall n, n <= n. Proof. -Exact le_n. +exact le_n. Qed. (** Transitivity *) -Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p). +Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. Proof. - NewInduction 2; Auto. + induction 2; auto. Qed. -Hints Resolve le_trans : arith v62. +Hint Resolve le_trans: arith v62. (** Order, successor and predecessor *) -Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)). +Theorem le_n_S : forall n m, n <= m -> S n <= S m. Proof. - NewInduction 1; Auto. + induction 1; auto. Qed. -Theorem le_n_Sn : (n:nat)(le n (S n)). +Theorem le_n_Sn : forall n, n <= S n. Proof. - Auto. + auto. Qed. -Theorem le_O_n : (n:nat)(le O n). +Theorem le_O_n : forall n, 0 <= n. Proof. - NewInduction n ; Auto. + induction n; auto. Qed. -Hints Resolve le_n_S le_n_Sn le_O_n le_n_S : arith v62. +Hint Resolve le_n_S le_n_Sn le_O_n le_n_S: arith v62. -Theorem le_pred_n : (n:nat)(le (pred n) n). +Theorem le_pred_n : forall n, pred n <= n. Proof. -NewInduction n ; Auto with arith. +induction n; auto with arith. Qed. -Hints Resolve le_pred_n : arith v62. +Hint Resolve le_pred_n: arith v62. -Theorem le_trans_S : (n,m:nat)(le (S n) m)->(le n m). +Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof. -Intros n m H ; Apply le_trans with (S n); Auto with arith. +intros n m H; apply le_trans with (S n); auto with arith. Qed. -Hints Immediate le_trans_S : arith v62. +Hint Immediate le_Sn_le: arith v62. -Theorem le_S_n : (n,m:nat)(le (S n) (S m))->(le n m). +Theorem le_S_n : forall n m, S n <= S m -> n <= m. Proof. -Intros n m H ; Change (le (pred (S n)) (pred (S m))). -Elim H ; Simpl ; Auto with arith. +intros n m H; change (pred (S n) <= pred (S m)) in |- *. +elim H; simpl in |- *; auto with arith. Qed. -Hints Immediate le_S_n : arith v62. +Hint Immediate le_S_n: arith v62. -Theorem le_pred : (n,m:nat)(le n m)->(le (pred n) (pred m)). +Theorem le_pred : forall n m, n <= m -> pred n <= pred m. Proof. -NewInduction n as [|n IHn]. Simpl. Auto with arith. -NewDestruct m as [|m]. Simpl. Intro H. Inversion H. -Simpl. Auto with arith. +induction n as [| n IHn]. simpl in |- *. auto with arith. +destruct m as [| m]. simpl in |- *. intro H. inversion H. +simpl in |- *. auto with arith. Qed. (** Comparison to 0 *) -Theorem le_Sn_O : (n:nat)~(le (S n) O). +Theorem le_Sn_O : forall n, ~ S n <= 0. Proof. -Red ; Intros n H. -Change (IsSucc O) ; Elim H ; Simpl ; Auto with arith. +red in |- *; intros n H. +change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith. Qed. -Hints Resolve le_Sn_O : arith v62. +Hint Resolve le_Sn_O: arith v62. -Theorem le_n_O_eq : (n:nat)(le n O)->(O=n). +Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n. Proof. -NewInduction n; Auto with arith. -Intro; Contradiction le_Sn_O with n. +induction n; auto with arith. +intro; contradiction le_Sn_O with n. Qed. -Hints Immediate le_n_O_eq : arith v62. +Hint Immediate le_n_O_eq: arith v62. (** Negative properties *) -Theorem le_Sn_n : (n:nat)~(le (S n) n). +Theorem le_Sn_n : forall n, ~ S n <= n. Proof. -NewInduction n; Auto with arith. +induction n; auto with arith. Qed. -Hints Resolve le_Sn_n : arith v62. +Hint Resolve le_Sn_n: arith v62. (** Antisymmetry *) -Theorem le_antisym : (n,m:nat)(le n m)->(le m n)->(n=m). +Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m. Proof. -Intros n m h ; NewDestruct h as [|m0]; Auto with arith. -Intros H1. -Absurd (le (S m0) m0) ; Auto with arith. -Apply le_trans with n ; Auto with arith. +intros n m h; destruct h as [| m0 H]; auto with arith. +intros H1. +absurd (S m0 <= m0); auto with arith. +apply le_trans with n; auto with arith. Qed. -Hints Immediate le_antisym : arith v62. +Hint Immediate le_antisym: arith v62. (** A different elimination principle for the order on natural numbers *) -Lemma le_elim_rel : (P:nat->nat->Prop) - ((p:nat)(P O p))-> - ((p,q:nat)(le p q)->(P p q)->(P (S p) (S q)))-> - (n,m:nat)(le n m)->(P n m). +Lemma le_elim_rel : + forall P:nat -> nat -> Prop, + (forall p, P 0 p) -> + (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> + forall n m, n <= m -> P n m. Proof. -NewInduction n; Auto with arith. -Intros m Le. -Elim Le; Auto with arith. -Qed. +induction n; auto with arith. +intros m Le. +elim Le; auto with arith. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 8c80e64c25..425087ea56 100755 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -8,169 +8,168 @@ (*i $Id$ i*) -Require Le. -V7only [Import nat_scope.]. +Require Import Le. Open Local Scope nat_scope. -Implicit Variables Type m,n,p:nat. +Implicit Types m n p : nat. (** Irreflexivity *) -Theorem lt_n_n : (n:nat)~(lt n n). +Theorem lt_irrefl : forall n, ~ n < n. Proof le_Sn_n. -Hints Resolve lt_n_n : arith v62. +Hint Resolve lt_irrefl: arith v62. (** Relationship between [le] and [lt] *) -Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p). +Theorem lt_le_S : forall n m, n < m -> S n <= m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Immediate lt_le_S : arith v62. +Hint Immediate lt_le_S: arith v62. -Theorem lt_n_Sm_le : (n,m:nat)(lt n (S m))->(le n m). +Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Immediate lt_n_Sm_le : arith v62. +Hint Immediate lt_n_Sm_le: arith v62. -Theorem le_lt_n_Sm : (n,m:nat)(le n m)->(lt n (S m)). +Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Immediate le_lt_n_Sm : arith v62. +Hint Immediate le_lt_n_Sm: arith v62. -Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n). +Theorem le_not_lt : forall n m, n <= m -> ~ m < n. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n). +Theorem lt_not_le : forall n m, n < m -> ~ m <= n. Proof. -Red; Intros n m Lt Le; Exact (le_not_lt m n Le Lt). +red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt). Qed. -Hints Immediate le_not_lt lt_not_le : arith v62. +Hint Immediate le_not_lt lt_not_le: arith v62. (** Asymmetry *) -Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n). +Theorem lt_asym : forall n m, n < m -> ~ m < n. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. (** Order and successor *) -Theorem lt_n_Sn : (n:nat)(lt n (S n)). +Theorem lt_n_Sn : forall n, n < S n. Proof. -Auto with arith. +auto with arith. Qed. -Hints Resolve lt_n_Sn : arith v62. +Hint Resolve lt_n_Sn: arith v62. -Theorem lt_S : (n,m:nat)(lt n m)->(lt n (S m)). +Theorem lt_S : forall n m, n < m -> n < S m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Resolve lt_S : arith v62. +Hint Resolve lt_S: arith v62. -Theorem lt_n_S : (n,m:nat)(lt n m)->(lt (S n) (S m)). +Theorem lt_n_S : forall n m, n < m -> S n < S m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Resolve lt_n_S : arith v62. +Hint Resolve lt_n_S: arith v62. -Theorem lt_S_n : (n,m:nat)(lt (S n) (S m))->(lt n m). +Theorem lt_S_n : forall n m, S n < S m -> n < m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Immediate lt_S_n : arith v62. +Hint Immediate lt_S_n: arith v62. -Theorem lt_O_Sn : (n:nat)(lt O (S n)). +Theorem lt_O_Sn : forall n, 0 < S n. Proof. -Auto with arith. +auto with arith. Qed. -Hints Resolve lt_O_Sn : arith v62. +Hint Resolve lt_O_Sn: arith v62. -Theorem lt_n_O : (n:nat)~(lt n O). +Theorem lt_n_O : forall n, ~ n < 0. Proof le_Sn_O. -Hints Resolve lt_n_O : arith v62. +Hint Resolve lt_n_O: arith v62. (** Predecessor *) -Lemma S_pred : (n,m:nat)(lt m n)->n=(S (pred n)). +Lemma S_pred : forall n m, m < n -> n = S (pred n). Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Lemma lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)). +Lemma lt_pred : forall n m, S n < m -> n < pred m. Proof. -NewInduction 1; Simpl; Auto with arith. +induction 1; simpl in |- *; auto with arith. Qed. -Hints Immediate lt_pred : arith v62. +Hint Immediate lt_pred: arith v62. -Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n). -NewDestruct 1; Simpl; Auto with arith. +Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n. +destruct 1; simpl in |- *; auto with arith. Qed. -Hints Resolve lt_pred_n_n : arith v62. +Hint Resolve lt_pred_n_n: arith v62. (** Transitivity properties *) -Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p). +Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. Proof. -NewInduction 2; Auto with arith. +induction 2; auto with arith. Qed. -Theorem lt_le_trans : (n,m,p:nat)(lt n m)->(le m p)->(lt n p). +Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. Proof. -NewInduction 2; Auto with arith. +induction 2; auto with arith. Qed. -Theorem le_lt_trans : (n,m,p:nat)(le n m)->(lt m p)->(lt n p). +Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. Proof. -NewInduction 2; Auto with arith. +induction 2; auto with arith. Qed. -Hints Resolve lt_trans lt_le_trans le_lt_trans : arith v62. +Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62. (** Large = strict or equal *) -Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m). +Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m). +Theorem lt_le_weak : forall n m, n < m -> n <= m. Proof. -Auto with arith. +auto with arith. Qed. -Hints Immediate lt_le_weak : arith v62. +Hint Immediate lt_le_weak: arith v62. (** Dichotomy *) -Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)). +Theorem le_or_lt : forall n m, n <= m \/ m < n. Proof. -Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith. -NewInduction 1; Auto with arith. +intros n m; pattern n, m in |- *; apply nat_double_ind; auto with arith. +induction 1; auto with arith. Qed. -Theorem nat_total_order: (m,n: nat) ~ m = n -> (lt m n) \/ (lt n m). +Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n. Proof. -Intros m n diff. -Elim (le_or_lt n m); [Intro H'0 | Auto with arith]. -Elim (le_lt_or_eq n m); Auto with arith. -Intro H'; Elim diff; Auto with arith. +intros m n diff. +elim (le_or_lt n m); [ intro H'0 | auto with arith ]. +elim (le_lt_or_eq n m); auto with arith. +intro H'; elim diff; auto with arith. Qed. (** Comparison to 0 *) -Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n). +Theorem neq_O_lt : forall n, 0 <> n -> 0 < n. Proof. -NewInduction n; Auto with arith. -Intros; Absurd O=O; Trivial with arith. +induction n; auto with arith. +intros; absurd (0 = 0); trivial with arith. Qed. -Hints Immediate neq_O_lt : arith v62. +Hint Immediate neq_O_lt: arith v62. -Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n). +Theorem lt_O_neq : forall n, 0 < n -> 0 <> n. Proof. -NewInduction 1; Auto with arith. +induction 1; auto with arith. Qed. -Hints Immediate lt_O_neq : arith v62. +Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index ac8ff97a19..c915c06909 100755 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,80 +8,78 @@ (*i $Id$ i*) -Require Arith. +Require Import Arith. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n:nat. +Implicit Types m n : nat. (** maximum of two natural numbers *) -Fixpoint max [n:nat] : nat -> nat := -[m:nat]Cases n m of - O _ => m - | (S n') O => n - | (S n') (S m') => (S (max n' m')) - end. +Fixpoint max n m {struct n} : nat := + match n, m with + | O, _ => m + | S n', O => n + | S n', S m' => S (max n' m') + end. (** Simplifications of [max] *) -Lemma max_SS : (n,m:nat)((S (max n m))=(max (S n) (S m))). +Lemma max_SS : forall n m, S (max n m) = max (S n) (S m). Proof. -Auto with arith. +auto with arith. Qed. -Lemma max_sym : (n,m:nat)(max n m)=(max m n). +Lemma max_comm : forall n m, max n m = max m n. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. +induction n; induction m; simpl in |- *; auto with arith. Qed. (** [max] and [le] *) -Lemma max_l : (n,m:nat)(le m n)->(max n m)=n. +Lemma max_l : forall n m, m <= n -> max n m = n. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. +induction n; induction m; simpl in |- *; auto with arith. Qed. -Lemma max_r : (n,m:nat)(le n m)->(max n m)=m. +Lemma max_r : forall n m, n <= m -> max n m = m. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. +induction n; induction m; simpl in |- *; auto with arith. Qed. -Lemma le_max_l : (n,m:nat)(le n (max n m)). +Lemma le_max_l : forall n m, n <= max n m. Proof. -NewInduction n; Intros; Simpl; Auto with arith. -Elim m; Intros; Simpl; Auto with arith. +induction n; intros; simpl in |- *; auto with arith. +elim m; intros; simpl in |- *; auto with arith. Qed. -Lemma le_max_r : (n,m:nat)(le m (max n m)). +Lemma le_max_r : forall n m, m <= max n m. Proof. -NewInduction n; Simpl; Auto with arith. -NewInduction m; Simpl; Auto with arith. +induction n; simpl in |- *; auto with arith. +induction m; simpl in |- *; auto with arith. Qed. -Hints Resolve max_r max_l le_max_l le_max_r: arith v62. +Hint Resolve max_r max_l le_max_l le_max_r: arith v62. (** [max n m] is equal to [n] or [m] *) -Lemma max_dec : (n,m:nat){(max n m)=n}+{(max n m)=m}. +Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. -Elim (IHn m);Intro H;Elim H;Auto. +induction n; induction m; simpl in |- *; auto with arith. +elim (IHn m); intro H; elim H; auto. Qed. -Lemma max_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (max n m)). +Lemma max_case : forall n m (P:nat -> Set), P n -> P m -> P (max n m). Proof. -NewInduction n; Simpl; Auto with arith. -NewInduction m; Intros; Simpl; Auto with arith. -Pattern (max n m); Apply IHn ; Auto with arith. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (max n m) in |- *; apply IHn; auto with arith. Qed. -Lemma max_case2 : (n,m:nat)(P:nat->Prop)(P n)->(P m)->(P (max n m)). +Lemma max_case2 : forall n m (P:nat -> Prop), P n -> P m -> P (max n m). Proof. -NewInduction n; Simpl; Auto with arith. -NewInduction m; Intros; Simpl; Auto with arith. -Pattern (max n m); Apply IHn ; Auto with arith. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (max n m) in |- *; apply IHn; auto with arith. Qed. - diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 81559526bd..18fba26a22 100755 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -8,77 +8,76 @@ (*i $Id$ i*) -Require Arith. +Require Import Arith. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n:nat. +Implicit Types m n : nat. (** minimum of two natural numbers *) -Fixpoint min [n:nat] : nat -> nat := -[m:nat]Cases n m of - O _ => O - | (S n') O => O - | (S n') (S m') => (S (min n' m')) - end. +Fixpoint min n m {struct n} : nat := + match n, m with + | O, _ => 0 + | S n', O => 0 + | S n', S m' => S (min n' m') + end. (** Simplifications of [min] *) -Lemma min_SS : (n,m:nat)((S (min n m))=(min (S n) (S m))). +Lemma min_SS : forall n m, S (min n m) = min (S n) (S m). Proof. -Auto with arith. +auto with arith. Qed. -Lemma min_sym : (n,m:nat)(min n m)=(min m n). +Lemma min_comm : forall n m, min n m = min m n. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. +induction n; induction m; simpl in |- *; auto with arith. Qed. (** [min] and [le] *) -Lemma min_l : (n,m:nat)(le n m)->(min n m)=n. +Lemma min_l : forall n m, n <= m -> min n m = n. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. +induction n; induction m; simpl in |- *; auto with arith. Qed. -Lemma min_r : (n,m:nat)(le m n)->(min n m)=m. +Lemma min_r : forall n m, m <= n -> min n m = m. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. +induction n; induction m; simpl in |- *; auto with arith. Qed. -Lemma le_min_l : (n,m:nat)(le (min n m) n). +Lemma le_min_l : forall n m, min n m <= n. Proof. -NewInduction n; Intros; Simpl; Auto with arith. -Elim m; Intros; Simpl; Auto with arith. +induction n; intros; simpl in |- *; auto with arith. +elim m; intros; simpl in |- *; auto with arith. Qed. -Lemma le_min_r : (n,m:nat)(le (min n m) m). +Lemma le_min_r : forall n m, min n m <= m. Proof. -NewInduction n; Simpl; Auto with arith. -NewInduction m; Simpl; Auto with arith. +induction n; simpl in |- *; auto with arith. +induction m; simpl in |- *; auto with arith. Qed. -Hints Resolve min_l min_r le_min_l le_min_r : arith v62. +Hint Resolve min_l min_r le_min_l le_min_r: arith v62. (** [min n m] is equal to [n] or [m] *) -Lemma min_dec : (n,m:nat){(min n m)=n}+{(min n m)=m}. +Lemma min_dec : forall n m, {min n m = n} + {min n m = m}. Proof. -NewInduction n;NewInduction m;Simpl;Auto with arith. -Elim (IHn m);Intro H;Elim H;Auto. +induction n; induction m; simpl in |- *; auto with arith. +elim (IHn m); intro H; elim H; auto. Qed. -Lemma min_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (min n m)). +Lemma min_case : forall n m (P:nat -> Set), P n -> P m -> P (min n m). Proof. -NewInduction n; Simpl; Auto with arith. -NewInduction m; Intros; Simpl; Auto with arith. -Pattern (min n m); Apply IHn ; Auto with arith. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (min n m) in |- *; apply IHn; auto with arith. Qed. -Lemma min_case2 : (n,m:nat)(P:nat->Prop)(P n)->(P m)->(P (min n m)). +Lemma min_case2 : forall n m (P:nat -> Prop), P n -> P m -> P (min n m). Proof. -NewInduction n; Simpl; Auto with arith. -NewInduction m; Intros; Simpl; Auto with arith. -Pattern (min n m); Apply IHn ; Auto with arith. -Qed. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (min n m) in |- *; apply IHn; auto with arith. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 658c25194e..783c494a2b 100755 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -10,111 +10,114 @@ (** Subtraction (difference between two natural numbers) *) -Require Lt. -Require Le. +Require Import Lt. +Require Import Le. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,p:nat. +Implicit Types m n p : nat. (** 0 is right neutral *) -Lemma minus_n_O : (n:nat)(n=(minus n O)). +Lemma minus_n_O : forall n, n = n - 0. Proof. -NewInduction n; Simpl; Auto with arith. +induction n; simpl in |- *; auto with arith. Qed. -Hints Resolve minus_n_O : arith v62. +Hint Resolve minus_n_O: arith v62. (** Permutation with successor *) -Lemma minus_Sn_m : (n,m:nat)(le m n)->((S (minus n m))=(minus (S n) m)). +Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m. Proof. -Intros n m Le; Pattern m n; Apply le_elim_rel; Simpl; Auto with arith. +intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *; + auto with arith. Qed. -Hints Resolve minus_Sn_m : arith v62. +Hint Resolve minus_Sn_m: arith v62. -Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)). -Intro x; NewInduction x; Simpl; Auto with arith. +Theorem pred_of_minus : forall n, pred n = n - 1. +intro x; induction x; simpl in |- *; auto with arith. Qed. (** Diagonal *) -Lemma minus_n_n : (n:nat)(O=(minus n n)). +Lemma minus_n_n : forall n, 0 = n - n. Proof. -NewInduction n; Simpl; Auto with arith. +induction n; simpl in |- *; auto with arith. Qed. -Hints Resolve minus_n_n : arith v62. +Hint Resolve minus_n_n: arith v62. (** Simplification *) -Lemma minus_plus_simpl : - (n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))). +Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). Proof. - NewInduction p; Simpl; Auto with arith. + induction p; simpl in |- *; auto with arith. Qed. -Hints Resolve minus_plus_simpl : arith v62. +Hint Resolve minus_plus_simpl_l_reverse: arith v62. (** Relation with plus *) -Lemma plus_minus : (n,m,p:nat)(n=(plus m p))->(p=(minus n m)). +Lemma plus_minus : forall n m p, n = m + p -> p = n - m. Proof. -Intros n m p; Pattern m n; Apply nat_double_ind; Simpl; Intros. -Replace (minus n0 O) with n0; Auto with arith. -Absurd O=(S (plus n0 p)); Auto with arith. -Auto with arith. +intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *; + intros. +replace (n0 - 0) with n0; auto with arith. +absurd (0 = S (n0 + p)); auto with arith. +auto with arith. Qed. -Hints Immediate plus_minus : arith v62. +Hint Immediate plus_minus: arith v62. -Lemma minus_plus : (n,m:nat)(minus (plus n m) n)=m. -Symmetry; Auto with arith. +Lemma minus_plus : forall n m, n + m - n = m. +symmetry in |- *; auto with arith. Qed. -Hints Resolve minus_plus : arith v62. +Hint Resolve minus_plus: arith v62. -Lemma le_plus_minus : (n,m:nat)(le n m)->(m=(plus n (minus m n))). +Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n). Proof. -Intros n m Le; Pattern n m; Apply le_elim_rel; Simpl; Auto with arith. +intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *; + auto with arith. Qed. -Hints Resolve le_plus_minus : arith v62. +Hint Resolve le_plus_minus: arith v62. -Lemma le_plus_minus_r : (n,m:nat)(le n m)->(plus n (minus m n))=m. +Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m. Proof. -Symmetry; Auto with arith. +symmetry in |- *; auto with arith. Qed. -Hints Resolve le_plus_minus_r : arith v62. +Hint Resolve le_plus_minus_r: arith v62. (** Relation with order *) -Theorem le_minus: (i,h:nat) (le (minus i h) i). +Theorem le_minus : forall n m, n - m <= n. Proof. -Intros i h;Pattern i h; Apply nat_double_ind; [ - Auto -| Auto -| Intros m n H; Simpl; Apply le_trans with m:=m; Auto ]. +intros i h; pattern i, h in |- *; apply nat_double_ind; + [ auto + | auto + | intros m n H; simpl in |- *; apply le_trans with (m := m); auto ]. Qed. -Lemma lt_minus : (n,m:nat)(le m n)->(lt O m)->(lt (minus n m) n). +Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n. Proof. -Intros n m Le; Pattern m n; Apply le_elim_rel; Simpl; Auto with arith. -Intros; Absurd (lt O O); Auto with arith. -Intros p q lepq Hp gtp. -Elim (le_lt_or_eq O p); Auto with arith. -Auto with arith. -NewInduction 1; Elim minus_n_O; Auto with arith. +intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *; + auto with arith. +intros; absurd (0 < 0); auto with arith. +intros p q lepq Hp gtp. +elim (le_lt_or_eq 0 p); auto with arith. +auto with arith. +induction 1; elim minus_n_O; auto with arith. Qed. -Hints Resolve lt_minus : arith v62. +Hint Resolve lt_minus: arith v62. -Lemma lt_O_minus_lt : (n,m:nat)(lt O (minus n m))->(lt m n). +Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n. Proof. -Intros n m; Pattern n m; Apply nat_double_ind; Simpl; Auto with arith. -Intros; Absurd (lt O O); Trivial with arith. -Qed. -Hints Immediate lt_O_minus_lt : arith v62. - -Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O. -Intros y x; Pattern y x ; Apply nat_double_ind; [ - Simpl; Trivial with arith -| Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n] -| Simpl; Intros n m H1 H2; Apply H1; - Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption]. +intros n m; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; + auto with arith. +intros; absurd (0 < 0); trivial with arith. Qed. +Hint Immediate lt_O_minus_lt: arith v62. + +Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0. +intros y x; pattern y, x in |- *; apply nat_double_ind; + [ simpl in |- *; trivial with arith + | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ] + | simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3; + apply H2; apply le_n_S; assumption ]. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index eb36ffa24d..49fcb06e0c 100755 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -13,178 +13,166 @@ Require Export Minus. Require Export Lt. Require Export Le. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,p:nat. +Implicit Types m n p : nat. (** Zero property *) -Lemma mult_0_r : (n:nat) (mult n O)=O. +Lemma mult_0_r : forall n, n * 0 = 0. Proof. -Intro; Symmetry; Apply mult_n_O. +intro; symmetry in |- *; apply mult_n_O. Qed. -Lemma mult_0_l : (n:nat) (mult O n)=O. +Lemma mult_0_l : forall n, 0 * n = 0. Proof. -Reflexivity. +reflexivity. Qed. (** Distributivity *) -Lemma mult_plus_distr : - (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))). +Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. Proof. -Intros; Elim n; Simpl; Intros; Auto with arith. -Elim plus_assoc_l; Elim H; Auto with arith. +intros; elim n; simpl in |- *; intros; auto with arith. +elim plus_assoc; elim H; auto with arith. Qed. -Hints Resolve mult_plus_distr : arith v62. +Hint Resolve mult_plus_distr_r: arith v62. -Lemma mult_plus_distr_r : (n,m,p:nat) (mult n (plus m p))=(plus (mult n m) (mult n p)). +Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. Proof. - NewInduction n. Trivial. - Intros. Simpl. Rewrite (IHn m p). Apply sym_eq. Apply plus_permute_2_in_4. + induction n. trivial. + intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4. Qed. -Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))). +Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. Proof. -Intros; Pattern n m; Apply nat_double_ind; Simpl; Intros; Auto with arith. -Elim minus_plus_simpl; Auto with arith. +intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros; + auto with arith. +elim minus_plus_simpl_l_reverse; auto with arith. Qed. -Hints Resolve mult_minus_distr : arith v62. +Hint Resolve mult_minus_distr_r: arith v62. (** Associativity *) -Lemma mult_assoc_r : (n,m,p:nat)((mult (mult n m) p) = (mult n (mult m p))). +Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). Proof. -Intros; Elim n; Intros; Simpl; Auto with arith. -Rewrite mult_plus_distr. -Elim H; Auto with arith. +intros; elim n; intros; simpl in |- *; auto with arith. +rewrite mult_plus_distr_r. +elim H; auto with arith. Qed. -Hints Resolve mult_assoc_r : arith v62. +Hint Resolve mult_assoc_reverse: arith v62. -Lemma mult_assoc_l : (n,m,p:nat)(mult n (mult m p)) = (mult (mult n m) p). +Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. Proof. -Auto with arith. +auto with arith. Qed. -Hints Resolve mult_assoc_l : arith v62. +Hint Resolve mult_assoc: arith v62. (** Commutativity *) -Lemma mult_sym : (n,m:nat)(mult n m)=(mult m n). +Lemma mult_comm : forall n m, n * m = m * n. Proof. -Intros; Elim n; Intros; Simpl; Auto with arith. -Elim mult_n_Sm. -Elim H; Apply plus_sym. +intros; elim n; intros; simpl in |- *; auto with arith. +elim mult_n_Sm. +elim H; apply plus_comm. Qed. -Hints Resolve mult_sym : arith v62. +Hint Resolve mult_comm: arith v62. (** 1 is neutral *) -Lemma mult_1_n : (n:nat)(mult (S O) n)=n. +Lemma mult_1_l : forall n, 1 * n = n. Proof. -Simpl; Auto with arith. +simpl in |- *; auto with arith. Qed. -Hints Resolve mult_1_n : arith v62. +Hint Resolve mult_1_l: arith v62. -Lemma mult_n_1 : (n:nat)(mult n (S O))=n. +Lemma mult_1_r : forall n, n * 1 = n. Proof. -Intro; Elim mult_sym; Auto with arith. +intro; elim mult_comm; auto with arith. Qed. -Hints Resolve mult_n_1 : arith v62. +Hint Resolve mult_1_r: arith v62. (** Compatibility with orders *) -Lemma mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)). +Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. Proof. -NewInduction m; Simpl; Auto with arith. +induction m; simpl in |- *; auto with arith. Qed. -Hints Resolve mult_O_le : arith v62. +Hint Resolve mult_O_le: arith v62. -Lemma mult_le_compat_l : (n,m,p:nat) (le n m) -> (le (mult p n) (mult p m)). +Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m. Proof. - NewInduction p as [|p IHp]. Intros. Simpl. Apply le_n. - Intros. Simpl. Apply le_plus_plus. Assumption. - Apply IHp. Assumption. + induction p as [| p IHp]. intros. simpl in |- *. apply le_n. + intros. simpl in |- *. apply plus_le_compat. assumption. + apply IHp. assumption. Qed. -Hints Resolve mult_le_compat_l : arith. -V7only [ -Notation mult_le := [m,n,p:nat](mult_le_compat_l p n m). -]. +Hint Resolve mult_le_compat_l: arith. -Lemma le_mult_right : (m,n,p:nat)(le m n)->(le (mult m p) (mult n p)). -Intros m n p H. -Rewrite mult_sym. Rewrite (mult_sym n). -Auto with arith. +Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p. +intros m n p H. +rewrite mult_comm. rewrite (mult_comm n). +auto with arith. Qed. -Lemma le_mult_mult : - (m,n,p,q:nat)(le m n)->(le p q)->(le (mult m p) (mult n q)). +Lemma mult_le_compat : + forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q. Proof. -Intros m n p q Hmn Hpq; NewInduction Hmn. -NewInduction Hpq. +intros m n p q Hmn Hpq; induction Hmn. +induction Hpq. (* m*p<=m*p *) -Apply le_n. +apply le_n. (* m*p<=m*m0 -> m*p<=m*(S m0) *) -Rewrite <- mult_n_Sm; Apply le_trans with (mult m m0). -Assumption. -Apply le_plus_l. +rewrite <- mult_n_Sm; apply le_trans with (m * m0). +assumption. +apply le_plus_l. (* m*p<=m0*q -> m*p<=(S m0)*q *) -Simpl; Apply le_trans with (mult m0 q). -Assumption. -Apply le_plus_r. +simpl in |- *; apply le_trans with (m0 * q). +assumption. +apply le_plus_r. Qed. -Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)). +Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. Proof. - Intro m; NewInduction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption. - Intros. Exact (lt_plus_plus ? ? ? ? H (IHm ? ? H)). + intro m; induction m. intros. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption. + intros. exact (plus_lt_compat _ _ _ _ H (IHm _ _ H)). Qed. -Hints Resolve mult_lt : arith. -V7only [ -Notation lt_mult_left := mult_lt. -(* Theorem lt_mult_left : - (x,y,z:nat) (lt x y) -> (lt (mult (S z) x) (mult (S z) y)). -*) -]. +Hint Resolve mult_S_lt_compat_l: arith. -Lemma lt_mult_right : - (m,n,p:nat) (lt m n) -> (lt (0) p) -> (lt (mult m p) (mult n p)). -Intros m n p H H0. -NewInduction p. -Elim (lt_n_n ? H0). -Rewrite mult_sym. -Replace (mult n (S p)) with (mult (S p) n); Auto with arith. +Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. +intros m n p H H0. +induction p. +elim (lt_irrefl _ H0). +rewrite mult_comm. +replace (n * S p) with (S p * n); auto with arith. Qed. -Lemma mult_le_conv_1 : (m,n,p:nat) (le (mult (S m) n) (mult (S m) p)) -> (le n p). +Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. Proof. - Intros m n p H. Elim (le_or_lt n p). Trivial. - Intro H0. Cut (lt (mult (S m) n) (mult (S m) n)). Intro. Elim (lt_n_n ? H1). - Apply le_lt_trans with m:=(mult (S m) p). Assumption. - Apply mult_lt. Assumption. + intros m n p H. elim (le_or_lt n p). trivial. + intro H0. cut (S m * n < S m * n). intro. elim (lt_irrefl _ H1). + apply le_lt_trans with (m := S m * p). assumption. + apply mult_S_lt_compat_l. assumption. Qed. (** n|->2*n and n|->2n+1 have disjoint image *) -V7only [ (* From Zdivides *) ]. -Theorem odd_even_lem: - (p, q : ?) ~ (plus (mult (2) p) (1)) = (mult (2) q). -Intros p; Elim p; Auto. -Intros q; Case q; Simpl. -Red; Intros; Discriminate. -Intros q'; Rewrite [x, y : ?] (plus_sym x (S y)); Simpl; Red; Intros; - Discriminate. -Intros p' H q; Case q. -Simpl; Red; Intros; Discriminate. -Intros q'; Red; Intros H0; Case (H q'). -Replace (mult (S (S O)) q') with (minus (mult (S (S O)) (S q')) (2)). -Rewrite <- H0; Simpl; Auto. -Repeat Rewrite [x, y : ?] (plus_sym x (S y)); Simpl; Auto. -Simpl; Repeat Rewrite [x, y : ?] (plus_sym x (S y)); Simpl; Auto. -Case q'; Simpl; Auto. +Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q. +intros p; elim p; auto. +intros q; case q; simpl in |- *. +red in |- *; intros; discriminate. +intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *; + intros; discriminate. +intros p' H q; case q. +simpl in |- *; red in |- *; intros; discriminate. +intros q'; red in |- *; intros H0; case (H q'). +replace (2 * q') with (2 * S q' - 2). +rewrite <- H0; simpl in |- *; auto. +repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto. +simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; + auto. +case q'; simpl in |- *; auto. Qed. @@ -194,31 +182,30 @@ Qed. tail-recursive, whereas [mult] is not. This can be useful when extracting programs. *) -Fixpoint mult_acc [s,m,n:nat] : nat := - Cases n of - O => s - | (S p) => (mult_acc (tail_plus m s) m p) - end. +Fixpoint mult_acc (s:nat) m n {struct n} : nat := + match n with + | O => s + | S p => mult_acc (tail_plus m s) m p + end. -Lemma mult_acc_aux : (n,s,m:nat)(plus s (mult n m))= (mult_acc s m n). +Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. -NewInduction n as [|p IHp]; Simpl;Auto. -Intros s m; Rewrite <- plus_tail_plus; Rewrite <- IHp. -Rewrite <- plus_assoc_r; Apply (f_equal2 nat nat);Auto. -Rewrite plus_sym;Auto. +induction n as [| p IHp]; simpl in |- *; auto. +intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. +rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto. +rewrite plus_comm; auto. Qed. -Definition tail_mult := [n,m:nat](mult_acc O m n). +Definition tail_mult n m := mult_acc 0 m n. -Lemma mult_tail_mult : (n,m:nat)(mult n m)=(tail_mult n m). +Lemma mult_tail_mult : forall n m, n * m = tail_mult n m. Proof. -Intros; Unfold tail_mult; Rewrite <- mult_acc_aux;Auto. +intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto. Qed. (** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] and [mult] and simplify *) -Tactic Definition TailSimpl := - Repeat Rewrite <- plus_tail_plus; - Repeat Rewrite <- mult_tail_mult; - Simpl. +Ltac tail_simpl := + repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult; + simpl in |- *.
\ No newline at end of file diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 96a8523f9f..4d657d0602 100755 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -8,29 +8,27 @@ (*i $Id$ i*) -Require Decidable. +Require Import Decidable. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,x,y:nat. +Implicit Types m n x y : nat. -Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}. +Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}. Proof. -NewInduction n. -Auto. -Left; Exists n; Auto. +induction n. +auto. +left; exists n; auto. Defined. -Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}. +Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}. Proof. -NewInduction n; NewInduction m; Auto. -Elim (IHn m); Auto. +induction n; induction m; auto. +elim (IHn m); auto. Defined. -Hints Resolve O_or_S eq_nat_dec : arith. +Hint Resolve O_or_S eq_nat_dec: arith. -Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)). -Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith. +Theorem dec_eq_nat : forall n m, decidable (n = m). +intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith. Defined. - diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index ffa94fcd05..496ac33303 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -10,183 +10,176 @@ (** Properties of addition *) -Require Le. -Require Lt. +Require Import Le. +Require Import Lt. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,p,q:nat. +Implicit Types m n p q : nat. (** Zero is neutral *) -Lemma plus_0_l : (n:nat) (O+n)=n. +Lemma plus_0_l : forall n, 0 + n = n. Proof. -Reflexivity. +reflexivity. Qed. -Lemma plus_0_r : (n:nat) (n+O)=n. +Lemma plus_0_r : forall n, n + 0 = n. Proof. -Intro; Symmetry; Apply plus_n_O. +intro; symmetry in |- *; apply plus_n_O. Qed. (** Commutativity *) -Lemma plus_sym : (n,m:nat)(n+m)=(m+n). +Lemma plus_comm : forall n m, n + m = m + n. Proof. -Intros n m ; Elim n ; Simpl ; Auto with arith. -Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith. +intros n m; elim n; simpl in |- *; auto with arith. +intros y H; elim (plus_n_Sm m y); auto with arith. Qed. -Hints Immediate plus_sym : arith v62. +Hint Immediate plus_comm: arith v62. (** Associativity *) -Lemma plus_Snm_nSm : (n,m:nat)((S n)+m)=(n+(S m)). -Intros. -Simpl. -Rewrite -> (plus_sym n m). -Rewrite -> (plus_sym n (S m)). -Trivial with arith. +Lemma plus_Snm_nSm : forall n m, S n + m = n + S m. +intros. +simpl in |- *. +rewrite (plus_comm n m). +rewrite (plus_comm n (S m)). +trivial with arith. Qed. -Lemma plus_assoc_l : (n,m,p:nat)((n+(m+p))=((n+m)+p)). +Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. Proof. -Intros n m p; Elim n; Simpl; Auto with arith. +intros n m p; elim n; simpl in |- *; auto with arith. Qed. -Hints Resolve plus_assoc_l : arith v62. +Hint Resolve plus_assoc: arith v62. -Lemma plus_permute : (n,m,p:nat) ((n+(m+p))=(m+(n+p))). +Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p). Proof. -Intros; Rewrite (plus_assoc_l m n p); Rewrite (plus_sym m n); Auto with arith. +intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith. Qed. -Lemma plus_assoc_r : (n,m,p:nat)(((n+m)+p)=(n+(m+p))). +Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p). Proof. -Auto with arith. +auto with arith. Qed. -Hints Resolve plus_assoc_r : arith v62. +Hint Resolve plus_assoc_reverse: arith v62. (** Simplification *) -Lemma plus_reg_l : (n,m,p:nat)((p+n)=(p+m))->(n=m). +Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m. Proof. -Intros m p n; NewInduction n ; Simpl ; Auto with arith. +intros m p n; induction n; simpl in |- *; auto with arith. Qed. -V7only [ -Notation simpl_plus_l := [n,m,p:nat](plus_reg_l m p n). -]. -Lemma plus_le_reg_l : (n,m,p:nat) (p+n)<=(p+m) -> n<=m. +Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m. Proof. -NewInduction p; Simpl; Auto with arith. +induction p; simpl in |- *; auto with arith. Qed. -V7only [ -Notation simpl_le_plus_l := [p,n,m:nat](plus_le_reg_l n m p). -]. -Lemma simpl_lt_plus_l : (n,m,p:nat) (p+n)<(p+m) -> n<m. +Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m. Proof. -NewInduction p; Simpl; Auto with arith. +induction p; simpl in |- *; auto with arith. Qed. (** Compatibility with order *) -Lemma le_reg_l : (n,m,p:nat) n<=m -> (p+n)<=(p+m). +Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m. Proof. -NewInduction p; Simpl; Auto with arith. +induction p; simpl in |- *; auto with arith. Qed. -Hints Resolve le_reg_l : arith v62. +Hint Resolve plus_le_compat_l: arith v62. -Lemma le_reg_r : (a,b,c:nat) a<=b -> (a+c)<=(b+c). +Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p. Proof. -NewInduction 1 ; Simpl; Auto with arith. +induction 1; simpl in |- *; auto with arith. Qed. -Hints Resolve le_reg_r : arith v62. +Hint Resolve plus_le_compat_r: arith v62. -Lemma le_plus_l : (n,m:nat) n<=(n+m). +Lemma le_plus_l : forall n m, n <= n + m. Proof. -NewInduction n; Simpl; Auto with arith. +induction n; simpl in |- *; auto with arith. Qed. -Hints Resolve le_plus_l : arith v62. +Hint Resolve le_plus_l: arith v62. -Lemma le_plus_r : (n,m:nat) m<=(n+m). +Lemma le_plus_r : forall n m, m <= n + m. Proof. -Intros n m; Elim n; Simpl; Auto with arith. +intros n m; elim n; simpl in |- *; auto with arith. Qed. -Hints Resolve le_plus_r : arith v62. +Hint Resolve le_plus_r: arith v62. -Theorem le_plus_trans : (n,m,p:nat) n<=m -> n<=(m+p). +Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p. Proof. -Intros; Apply le_trans with m:=m; Auto with arith. +intros; apply le_trans with (m := m); auto with arith. Qed. -Hints Resolve le_plus_trans : arith v62. +Hint Resolve le_plus_trans: arith v62. -Theorem lt_plus_trans : (n,m,p:nat) n<m -> n<(m+p). +Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. Proof. -Intros; Apply lt_le_trans with m:=m; Auto with arith. +intros; apply lt_le_trans with (m := m); auto with arith. Qed. -Hints Immediate lt_plus_trans : arith v62. +Hint Immediate lt_plus_trans: arith v62. -Lemma lt_reg_l : (n,m,p:nat) n<m -> (p+n)<(p+m). +Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. Proof. -NewInduction p; Simpl; Auto with arith. +induction p; simpl in |- *; auto with arith. Qed. -Hints Resolve lt_reg_l : arith v62. +Hint Resolve plus_lt_compat_l: arith v62. -Lemma lt_reg_r : (n,m,p:nat) n<m -> (n+p)<(m+p). +Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. Proof. -Intros n m p H ; Rewrite (plus_sym n p) ; Rewrite (plus_sym m p). -Elim p; Auto with arith. +intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p). +elim p; auto with arith. Qed. -Hints Resolve lt_reg_r : arith v62. +Hint Resolve plus_lt_compat_r: arith v62. -Lemma le_plus_plus : (n,m,p,q:nat) n<=m -> p<=q -> (n+p)<=(m+q). +Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. Proof. -Intros n m p q H H0. -Elim H; Simpl; Auto with arith. +intros n m p q H H0. +elim H; simpl in |- *; auto with arith. Qed. -Lemma le_lt_plus_plus : (n,m,p,q:nat) n<=m -> p<q -> (n+p)<(m+q). +Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. Proof. - Unfold lt. Intros. Change ((S n)+p)<=(m+q). Rewrite plus_Snm_nSm. - Apply le_plus_plus; Assumption. + unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. rewrite plus_Snm_nSm. + apply plus_le_compat; assumption. Qed. -Lemma lt_le_plus_plus : (n,m,p,q:nat) n<m -> p<=q -> (n+p)<(m+q). +Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. Proof. - Unfold lt. Intros. Change ((S n)+p)<=(m+q). Apply le_plus_plus; Assumption. + unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. apply plus_le_compat; assumption. Qed. -Lemma lt_plus_plus : (n,m,p,q:nat) n<m -> p<q -> (n+p)<(m+q). +Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. Proof. - Intros. Apply lt_le_plus_plus. Assumption. - Apply lt_le_weak. Assumption. + intros. apply plus_lt_le_compat. assumption. + apply lt_le_weak. assumption. Qed. (** Inversion lemmas *) -Lemma plus_is_O : (m,n:nat) (m+n)=O -> m=O /\ n=O. +Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0. Proof. - Intro m; NewDestruct m; Auto. - Intros. Discriminate H. + intro m; destruct m as [| n]; auto. + intros. discriminate H. Qed. -Definition plus_is_one : - (m,n:nat) (m+n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}. +Definition plus_is_one : + forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}. Proof. - Intro m; NewDestruct m; Auto. - NewDestruct n; Auto. - Intros. - Simpl in H. Discriminate H. + intro m; destruct m as [| n]; auto. + destruct n; auto. + intros. + simpl in H. discriminate H. Defined. (** Derived properties *) -Lemma plus_permute_2_in_4 : (m,n,p,q:nat) ((m+n)+(p+q))=((m+p)+(n+q)). +Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q). Proof. - Intros m n p q. - Rewrite <- (plus_assoc_l m n (p+q)). Rewrite (plus_assoc_l n p q). - Rewrite (plus_sym n p). Rewrite <- (plus_assoc_l p n q). Apply plus_assoc_l. + intros m n p q. + rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q). + rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc. Qed. (** Tail-recursive plus *) @@ -195,15 +188,15 @@ Qed. tail-recursive, whereas [plus] is not. This can be useful when extracting programs. *) -Fixpoint plus_acc [q,n:nat] : nat := - Cases n of - O => q - | (S p) => (plus_acc (S q) p) - end. +Fixpoint plus_acc q n {struct n} : nat := + match n with + | O => q + | S p => plus_acc (S q) p + end. -Definition tail_plus := [n,m:nat](plus_acc m n). +Definition tail_plus n m := plus_acc m n. -Lemma plus_tail_plus : (n,m:nat)(n+m)=(tail_plus n m). -Unfold tail_plus; NewInduction n as [|n IHn]; Simpl; Auto. -Intro m; Rewrite <- IHn; Simpl; Auto. -Qed. +Lemma plus_tail_plus : forall n m, n + m = tail_plus n m. +unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto. +intro m; rewrite <- IHn; simpl in |- *; auto. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 51df19b294..a7a50795e6 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -10,36 +10,35 @@ (** Well-founded relations and natural numbers *) -Require Lt. +Require Import Lt. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,p:nat. +Implicit Types m n p : nat. -Chapter Well_founded_Nat. +Section Well_founded_Nat. Variable A : Set. Variable f : A -> nat. -Definition ltof := [a,b:A](lt (f a) (f b)). -Definition gtof := [a,b:A](gt (f b) (f a)). +Definition ltof (a b:A) := f a < f b. +Definition gtof (a b:A) := f b > f a. -Theorem well_founded_ltof : (well_founded A ltof). +Theorem well_founded_ltof : well_founded ltof. Proof. -Red. -Cut (n:nat)(a:A)(lt (f a) n)->(Acc A ltof a). -Intros H a; Apply (H (S (f a))); Auto with arith. -NewInduction n. -Intros; Absurd (lt (f a) O); Auto with arith. -Intros a ltSma. -Apply Acc_intro. -Unfold ltof; Intros b ltfafb. -Apply IHn. -Apply lt_le_trans with (f a); Auto with arith. +red in |- *. +cut (forall n (a:A), f a < n -> Acc ltof a). +intros H a; apply (H (S (f a))); auto with arith. +induction n. +intros; absurd (f a < 0); auto with arith. +intros a ltSma. +apply Acc_intro. +unfold ltof in |- *; intros b ltfafb. +apply IHn. +apply lt_le_trans with (f a); auto with arith. Qed. -Theorem well_founded_gtof : (well_founded A gtof). +Theorem well_founded_gtof : well_founded gtof. Proof well_founded_ltof. (** It is possible to directly prove the induction principle going @@ -59,142 +58,149 @@ the ML-like program for [induction_ltof2] is : [[ where rec indrec a = F a indrec;; ]] *) -Theorem induction_ltof1 - : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a). +Theorem induction_ltof1 : + forall P:A -> Set, + (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. Proof. -Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a). -Intros H a; Apply (H (S (f a))); Auto with arith. -NewInduction n. -Intros; Absurd (lt (f a) O); Auto with arith. -Intros a ltSma. -Apply F. -Unfold ltof; Intros b ltfafb. -Apply IHn. -Apply lt_le_trans with (f a); Auto with arith. +intros P F; cut (forall n (a:A), f a < n -> P a). +intros H a; apply (H (S (f a))); auto with arith. +induction n. +intros; absurd (f a < 0); auto with arith. +intros a ltSma. +apply F. +unfold ltof in |- *; intros b ltfafb. +apply IHn. +apply lt_le_trans with (f a); auto with arith. Defined. -Theorem induction_gtof1 - : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a). +Theorem induction_gtof1 : + forall P:A -> Set, + (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. Proof. -Exact induction_ltof1. +exact induction_ltof1. Defined. -Theorem induction_ltof2 - : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a). +Theorem induction_ltof2 : + forall P:A -> Set, + (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. Proof. -Exact (well_founded_induction A ltof well_founded_ltof). +exact (well_founded_induction well_founded_ltof). Defined. -Theorem induction_gtof2 - : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a). +Theorem induction_gtof2 : + forall P:A -> Set, + (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. Proof. -Exact induction_ltof2. +exact induction_ltof2. Defined. (** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)] then [R] is well-founded. *) -Variable R : A->A->Prop. +Variable R : A -> A -> Prop. -Hypothesis H_compat : (x,y:A) (R x y) -> (lt (f x) (f y)). +Hypothesis H_compat : forall x y:A, R x y -> f x < f y. -Theorem well_founded_lt_compat : (well_founded A R). +Theorem well_founded_lt_compat : well_founded R. Proof. -Red. -Cut (n:nat)(a:A)(lt (f a) n)->(Acc A R a). -Intros H a; Apply (H (S (f a))); Auto with arith. -NewInduction n. -Intros; Absurd (lt (f a) O); Auto with arith. -Intros a ltSma. -Apply Acc_intro. -Intros b ltfafb. -Apply IHn. -Apply lt_le_trans with (f a); Auto with arith. +red in |- *. +cut (forall n (a:A), f a < n -> Acc R a). +intros H a; apply (H (S (f a))); auto with arith. +induction n. +intros; absurd (f a < 0); auto with arith. +intros a ltSma. +apply Acc_intro. +intros b ltfafb. +apply IHn. +apply lt_le_trans with (f a); auto with arith. Qed. End Well_founded_Nat. -Lemma lt_wf : (well_founded nat lt). -Proof (well_founded_ltof nat [m:nat]m). +Lemma lt_wf : well_founded lt. +Proof well_founded_ltof nat (fun m => m). -Lemma lt_wf_rec1 : (p:nat)(P:nat->Set) - ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p). +Lemma lt_wf_rec1 : + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. Proof. -Exact [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)] - (induction_ltof1 nat [m:nat]m P F p). +exact + (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) => + induction_ltof1 nat (fun m => m) P F p). Defined. -Lemma lt_wf_rec : (p:nat)(P:nat->Set) - ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p). +Lemma lt_wf_rec : + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. Proof. -Exact [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)] - (induction_ltof2 nat [m:nat]m P F p). +exact + (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) => + induction_ltof2 nat (fun m => m) P F p). Defined. -Lemma lt_wf_ind : (p:nat)(P:nat->Prop) - ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p). -Intro p; Intros; Elim (lt_wf p); Auto with arith. +Lemma lt_wf_ind : + forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n. +intro p; intros; elim (lt_wf p); auto with arith. Qed. -Lemma gt_wf_rec : (p:nat)(P:nat->Set) - ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p). +Lemma gt_wf_rec : + forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n. Proof. -Exact lt_wf_rec. +exact lt_wf_rec. Defined. -Lemma gt_wf_ind : (p:nat)(P:nat->Prop) - ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p). +Lemma gt_wf_ind : + forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n. Proof lt_wf_ind. -Lemma lt_wf_double_rec : - (P:nat->nat->Set) - ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m)) - -> (p,q:nat)(P p q). -Intros P Hrec p; Pattern p; Apply lt_wf_rec. -Intros n H q; Pattern q; Apply lt_wf_rec; Auto with arith. +Lemma lt_wf_double_rec : + forall P:nat -> nat -> Set, + (forall n m, + (forall p (q:nat), p < n -> P p q) -> + (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. +intros P Hrec p; pattern p in |- *; apply lt_wf_rec. +intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith. Defined. -Lemma lt_wf_double_ind : - (P:nat->nat->Prop) - ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m)) - -> (p,q:nat)(P p q). -Intros P Hrec p; Pattern p; Apply lt_wf_ind. -Intros n H q; Pattern q; Apply lt_wf_ind; Auto with arith. +Lemma lt_wf_double_ind : + forall P:nat -> nat -> Prop, + (forall n m, + (forall p (q:nat), p < n -> P p q) -> + (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. +intros P Hrec p; pattern p in |- *; apply lt_wf_ind. +intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith. Qed. -Hints Resolve lt_wf : arith. -Hints Resolve well_founded_lt_compat : arith. +Hint Resolve lt_wf: arith. +Hint Resolve well_founded_lt_compat: arith. Section LT_WF_REL. -Variable A :Set. -Variable R:A->A->Prop. +Variable A : Set. +Variable R : A -> A -> Prop. (* Relational form of inversion *) Variable F : A -> nat -> Prop. -Definition inv_lt_rel - [x,y]:=(EX n | (F x n) & (m:nat)(F y m)->(lt n m)). - -Hypothesis F_compat : (x,y:A) (R x y) -> (inv_lt_rel x y). -Remark acc_lt_rel : - (x:A)(EX n | (F x n))->(Acc A R x). -Intros x (n,fxn); Generalize x fxn; Clear x fxn. -Pattern n; Apply lt_wf_ind; Intros. -Constructor; Intros. -Case (F_compat y x); Trivial; Intros. -Apply (H x0); Auto. -Save. - -Theorem well_founded_inv_lt_rel_compat : (well_founded A R). -Constructor; Intros. -Case (F_compat y a); Trivial; Intros. -Apply acc_lt_rel; Trivial. -Exists x; Trivial. -Save. +Definition inv_lt_rel x y := + exists2 n : _ | F x n & (forall m, F y m -> n < m). + +Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y. +Remark acc_lt_rel : forall x:A, ( exists n : _ | F x n) -> Acc R x. +intros x [n fxn]; generalize x fxn; clear x fxn. +pattern n in |- *; apply lt_wf_ind; intros. +constructor; intros. +case (F_compat y x); trivial; intros. +apply (H x0); auto. +Qed. + +Theorem well_founded_inv_lt_rel_compat : well_founded R. +constructor; intros. +case (F_compat y a); trivial; intros. +apply acc_lt_rel; trivial. +exists x; trivial. +Qed. End LT_WF_REL. -Lemma well_founded_inv_rel_inv_lt_rel - : (A:Set)(F:A->nat->Prop)(well_founded A (inv_lt_rel A F)). -Intros; Apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); Trivial. -Save. +Lemma well_founded_inv_rel_inv_lt_rel : + forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). +intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. +Qed.
\ No newline at end of file |