Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 163 insertions, 163 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 7680997d..2e9472c4 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Between.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Between.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Le.
 Require Import Lt.
@@ -16,174 +16,174 @@ Open Local Scope nat_scope.
 Implicit Types k l p q r : nat.
 
 Section Between.
-Variables P Q : nat -> Prop.
-
-Inductive between k : nat -> Prop :=
-  | bet_emp : between k k
-  | bet_S : forall l, between k l -> P l -> between k (S l).
-
-Hint Constructors between: arith v62.
-
-Lemma bet_eq : forall k l, l = k -> between k l.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-Hint Resolve bet_eq: arith v62.
-
-Lemma between_le : forall k l, between k l -> k <= l.
-Proof.
-induction 1; auto with arith.
-Qed.
-Hint Immediate between_le: arith v62.
-
-Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
-Proof.
-induction 1.
-intros; absurd (S k <= k); auto with arith.
-destruct H; auto with arith.
-Qed.
-Hint Resolve between_Sk_l: arith v62.
-
-Lemma between_restr :
- forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-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 Constructors exists_between: arith v62.
-
-Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-Lemma exists_lt : forall k l, exists_between k l -> k < l.
-Proof exists_le_S.
-Hint Immediate exists_le_S exists_lt: arith v62.
-
-Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
-Proof.
-intros; apply le_S_n; auto with arith.
-Qed.
-Hint Immediate exists_S_le: arith v62.
-
-Definition in_int p q r := p <= r /\ r < q.
-
-Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
-Proof.
-red in |- *; auto with arith.
-Qed.
-Hint Resolve in_int_intro: arith v62.
-
-Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
-Proof.
-induction 1; intros.
-apply le_lt_trans with r; auto with arith.
-Qed.
-
-Lemma in_int_p_Sq :
- forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat.
-Proof.
-induction 1; intros.
-elim (le_lt_or_eq r q); auto with arith.
-Qed.
-
-Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r.
-Proof.
-induction 1; auto with arith.
-Qed.
-Hint Resolve in_int_S: arith v62.
-
-Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
-Proof.
-induction 1; auto with arith.
-Qed.
-Hint Immediate in_int_Sp_q: arith v62.
-
-Lemma between_in_int :
- forall k l, between k l -> forall r, in_int k l r -> P r.
-Proof.
-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 :
- forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-Lemma exists_in_int :
- forall k l, exists_between k l ->  exists2 m : nat, in_int k l m & Q m.
-Proof.
-induction 1.
-case IHexists_between; intros p inp Qp; exists p; auto with arith.
-exists l; auto with arith.
-Qed.
-
-Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l.
-Proof.
-destruct 1; intros.
-elim H0; auto with arith.
-Qed.
-
-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.
-induction 1; intros; auto with arith.
-elim IHle; intro; auto with arith.
-elim (H0 m); auto with arith.
-Qed.
-
-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.
-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 0
-  | nth_S :
+  Variables P Q : nat -> Prop.
+  
+  Inductive between k : nat -> Prop :=
+    | bet_emp : between k k
+    | bet_S : forall l, between k l -> P l -> between k (S l).
+  
+  Hint Constructors between: arith v62.
+
+  Lemma bet_eq : forall k l, l = k -> between k l.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  Hint Resolve bet_eq: arith v62.
+
+  Lemma between_le : forall k l, between k l -> k <= l.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+  Hint Immediate between_le: arith v62.
+
+  Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
+  Proof.
+    intros k l H; induction H as [|l H].
+    intros; absurd (S k <= k); auto with arith.
+    destruct H; auto with arith.
+  Qed.
+  Hint Resolve between_Sk_l: arith v62.
+
+  Lemma between_restr :
+    forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  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 Constructors exists_between: arith v62.
+
+  Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  Lemma exists_lt : forall k l, exists_between k l -> k < l.
+  Proof exists_le_S.
+  Hint Immediate exists_le_S exists_lt: arith v62.
+
+  Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
+  Proof.
+    intros; apply le_S_n; auto with arith.
+  Qed.
+  Hint Immediate exists_S_le: arith v62.
+
+  Definition in_int p q r := p <= r /\ r < q.
+
+  Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
+  Proof.
+    red in |- *; auto with arith.
+  Qed.
+  Hint Resolve in_int_intro: arith v62.
+
+  Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
+  Proof.
+    induction 1; intros.
+    apply le_lt_trans with r; auto with arith.
+  Qed.
+
+  Lemma in_int_p_Sq :
+    forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat.
+  Proof.
+    induction 1; intros.
+    elim (le_lt_or_eq r q); auto with arith.
+  Qed.
+
+  Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+  Hint Resolve in_int_S: arith v62.
+
+  Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+  Hint Immediate in_int_Sp_q: arith v62.
+
+  Lemma between_in_int :
+    forall k l, between k l -> forall r, in_int k l r -> P r.
+  Proof.
+    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 :
+    forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  Lemma exists_in_int :
+    forall k l, exists_between k l ->  exists2 m : nat, in_int k l m & Q m.
+  Proof.
+    induction 1.
+    case IHexists_between; intros p inp Qp; exists p; auto with arith.
+    exists l; auto with arith.
+  Qed.
+
+  Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l.
+  Proof.
+    destruct 1; intros.
+    elim H0; auto with arith.
+  Qed.
+
+  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.
+    induction 1; intros; auto with arith.
+    elim IHle; intro; auto with arith.
+    elim (H0 m); auto with arith.
+  Qed.
+
+  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.
+    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 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).
+	P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n).
 
-Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
-Proof.
-induction 1; intros; auto with arith.
-apply le_trans with (S k); auto with arith.
-Qed.
+  Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
+  Proof.
+    induction 1; intros; auto with arith.
+    apply le_trans with (S k); auto with arith.
+  Qed.
 
-Definition eventually (n:nat) :=  exists2 k : nat, k <= n & Q k.
+  Definition eventually (n:nat) :=  exists2 k : nat, k <= n & Q k.
 
-Lemma event_O : eventually 0 -> Q 0.
-Proof.
-induction 1; intros.
-replace 0 with x; auto with arith.
-Qed.
+  Lemma event_O : eventually 0 -> Q 0.
+  Proof.
+    induction 1; intros.
+    replace 0 with x; auto with arith.
+  Qed.
 
 End Between.
 
 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
+Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.