(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                Between.v                                 *)
(****************************************************************************)

Require Le.
Require Lt.

Section Between.
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)).

Hint bet_emp.

Lemma bet_eq : (k,l:nat)(l=k)->(between k l).
Proof.
Induction 1; Auto.
Qed.

Hint bet_S bet_eq bet_emp.

Lemma between_le : (k,l:nat)(between k l)->(le k l).
Proof.
Induction 1; Auto.
Qed.
Immediate between_le.

Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l).
Proof.
Induction 1.
Intros; Absurd (le (S k) k); Auto.
Induction 1; Auto.
Qed.
Hint between_Sk_l.

Lemma between_restr : (k,l,m:nat)(le k l)->(le l m)->(between k m)->(between l m).
Proof.
Induction 1; Auto.
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)).

Hint exists_S exists_le.

Lemma exists_le_S : (k,l:nat)(exists k l)->(le (S k) l).
Proof.
Induction 1; Auto.
Qed.
Immediate exists_le_S.

Lemma exists_lt : (k,l:nat)(exists k l)->(lt k l).
Proof exists_le_S.
Immediate exists_lt.


Lemma exists_S_le : (k,l:nat)(exists k (S l))->(le k l).
Proof.
Intros; Apply le_S_n; Auto.
Qed.
Immediate exists_S_le.

Definition in_int [p,q,r:nat](le p r)/\(lt r q).

Lemma in_int_intro : (p,q,r:nat)(le p r)->(lt r q)->(in_int p q r).
Proof.
Red; Auto.
Qed.
Hint in_int_intro.

Lemma in_int_lt : (p,q,r:nat)(in_int p q r)->(lt p q).
Proof.
Induction 1; Intros.
Apply le_lt_trans with r; Auto.
Qed.

Lemma in_int_p_Sq : (p,q,r:nat)(in_int p (S q) r)->((in_int p q r)\/<nat>r=q).
Proof.
Induction 1; Intros.
Elim (le_lt_or_eq r q); Auto.
Qed.

Lemma in_int_S : (p,q,r:nat)(in_int p q r)->(in_int p (S q) r).
Proof.
Induction 1;Auto.
Qed.
Hint in_int_S.

Lemma in_int_Sp_q : (p,q,r:nat)(in_int (S p) q r)->(in_int p q r).
Proof.
Induction 1; Auto.
Qed.
Immediate in_int_Sp_q.

Lemma between_in_int : (k,l:nat)(between k l)->(r:nat)(in_int k l r)->(P r).
Proof.
Induction 1; Intros.
Absurd (lt k k); Auto.
Apply in_int_lt with r; Auto.
Elim (in_int_p_Sq k l0 r); Intros; Auto.
Rewrite H4; Trivial.
Qed.

Lemma in_int_between : (k,l:nat)(le k l)->((r:nat)(in_int k l r)->(P r))->(between k l).
Proof.
Induction 1; Auto.
Qed.

Lemma exists_in_int : (k,l:nat)(exists k l)->(EX m:nat | (in_int k l m) & (Q m)).
Proof.
Induction 1.
Induction 2; Intros p inp Qp; Exists p; Auto.
Intros; Exists l0; Auto.
Qed.

Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l).
Proof.
Induction 1; Intros.
Elim H1; Auto.
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)).
Proof.
Induction 1; Intros; Auto.
Elim H1; Intro; Auto.
Elim (H2 m); Auto.
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).
Proof.
Induction 1; Red; Intros.
Absurd (lt k k); Auto.
Absurd (Q l0); Auto.
Elim (exists_in_int k (S l0)); Auto; Intros l' inl' Ql'.
Replace l0 with l'; Auto.
Elim inl'; Intros.
Elim (le_lt_or_eq l' l0); Auto; Intros.
Absurd (exists k l0); Auto.
Apply in_int_exists with l'; Auto.
Qed.

Inductive nth [init:nat] : nat->nat->Prop
  := nth_O : (nth init init O)
  | nth_S : (k,l:nat)(n:nat)(nth init k n)->(between (S k) l)
                        ->(Q l)->(nth init l (S n)).

Lemma nth_le : (init,l,n:nat)(nth init l n)->(le init l).
Proof.
Induction 1; Intros; Auto.
Apply le_trans with (S k); Auto.
Qed.

Definition eventually [n:nat](EX k:nat | (le k n) & (Q k)).

Lemma event_O : (eventually O)->(Q O).
Proof.
Induction 1; Intros.
Replace O with x; Auto.
Qed.

End Between.

Hint nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le in_int_S 
     in_int_intro. 
Immediate in_int_Sp_q exists_le_S exists_S_le.


(* $Id: Between.v,v 1.6 1998/04/30 16:45:43 mohring Exp $ *)
