Library Coq.Arith.Between
Require Import Le.
Require Import Lt.
Local Open Scope nat_scope.
Implicit Types k l p q r :
nat.
Section Between.
Variables P Q :
nat -> Prop.
The between type expresses the concept
forall i: nat, k <= i < l -> P i..
The exists_between type expresses the concept
exists i: nat, k <= i < l /\ Q i.
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.
Lemma exists_le_S :
forall k l,
exists_between k l -> S k <= l.
Lemma exists_lt :
forall k l,
exists_between k l -> k < l.
Hint Immediate exists_le_S exists_lt:
arith.
Lemma exists_S_le :
forall k l,
exists_between k (
S l)
-> k <= l.
Hint Immediate exists_S_le:
arith.
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.
Hint Resolve in_int_intro:
arith.
Lemma in_int_lt :
forall p q r,
in_int p q r -> p < q.
Lemma in_int_p_Sq :
forall p q r,
in_int p (
S q)
r -> in_int p q r \/ r = q.
Lemma in_int_S :
forall p q r,
in_int p q r -> in_int p (
S q)
r.
Hint Resolve in_int_S:
arith.
Lemma in_int_Sp_q :
forall p q r,
in_int (
S p)
q r -> in_int p q r.
Hint Immediate in_int_Sp_q:
arith.
Lemma between_in_int :
forall k l,
between k l -> forall r,
in_int k l r -> P r.
Lemma in_int_between :
forall k l,
k <= l -> (forall r,
in_int k l r -> P r) -> between k l.
Lemma exists_in_int :
forall k l,
exists_between k l -> exists2 m : nat, in_int k l m & Q m.
Lemma in_int_exists :
forall k l r,
in_int k l r -> Q r -> exists_between 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.
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.
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 :
forall (
init:
nat)
l (
n:
nat),
P_nth init l n -> init <= l.
Definition eventually (
n:
nat) :=
exists2 k : nat, k <= n & Q k.
Lemma event_O :
eventually 0
-> Q 0.
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.
Hint Immediate in_int_Sp_q exists_le_S exists_S_le:
arith.