Library Coq.Arith.Between
Require Import Le.
Require Import Lt.
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.
Hint Resolve bet_eq:
arith v62.
Lemma between_le :
forall k l,
between k l ->
k <=
l.
Hint Immediate between_le:
arith v62.
Lemma between_Sk_l :
forall k l,
between k l ->
S k <=
l ->
between (
S k)
l.
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.
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.
Lemma exists_lt :
forall k l,
exists_between k l ->
k <
l.
Hint Immediate exists_le_S exists_lt:
arith v62.
Lemma exists_S_le :
forall k l,
exists_between k (
S l) ->
k <=
l.
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.
Hint Resolve in_int_intro:
arith v62.
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 :>nat.
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 v62.
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 v62.
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 v62.
Hint Immediate in_int_Sp_q exists_le_S exists_S_le:
arith v62.