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..
Inductive between k : nat -> Prop :=
| bet_emp : between k k
| bet_S : forall l, between k l -> P l -> between k (S l).
#[local]
Hint Constructors between: arith.
Lemma bet_eq : forall k l, l = k -> between k l.
#[local]
Hint Resolve bet_eq: arith.
Lemma between_le : forall k l, between k l -> k <= l.
#[local]
Hint Immediate between_le: arith.
Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
#[local]
Hint Resolve between_Sk_l: arith.
Lemma between_restr :
forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
| bet_emp : between k k
| bet_S : forall l, between k l -> P l -> between k (S l).
#[local]
Hint Constructors between: arith.
Lemma bet_eq : forall k l, l = k -> between k l.
#[local]
Hint Resolve bet_eq: arith.
Lemma between_le : forall k l, between k l -> k <= l.
#[local]
Hint Immediate between_le: arith.
Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
#[local]
Hint Resolve between_Sk_l: arith.
Lemma between_restr :
forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
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).
#[local]
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.
#[local]
Hint Immediate exists_le_S exists_lt: arith.
Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
#[local]
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.
#[local]
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.
#[local]
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.
#[local]
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.
#[global]
Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
in_int_S in_int_intro: arith.
#[global]
Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.
| 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).
#[local]
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.
#[local]
Hint Immediate exists_le_S exists_lt: arith.
Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
#[local]
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.
#[local]
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.
#[local]
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.
#[local]
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.
#[global]
Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
in_int_S in_int_intro: arith.
#[global]
Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.