Between.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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 ∀ 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).

  Hint Constructors between: arith.

  Lemma bet_eq : forall k l, l = k -> between k l.P, Q:nat -> Prop
forall k l : nat, l = k -> between k l
  Proof.P, Q:nat -> Prop
forall k l : nat, l = k -> between k l
    intros * ->; auto with arith.
  Qed.

  Hint Resolve bet_eq: arith.

  Lemma between_le : forall k l, between k l -> k <= l.P, Q:nat -> Prop
forall k l : nat, between k l -> k <= l
  Proof.P, Q:nat -> Prop
forall k l : nat, between k l -> k <= l
    induction 1; auto with arith.
  Qed.
  Hint Immediate between_le: arith.

  Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.P, Q:nat -> Prop
forall k l : nat,
between k l -> S k <= l -> between (S k) l
  Proof.P, Q:nat -> Prop
forall k l : nat,
between k l -> S k <= l -> between (S k) l
    induction 1 as [|* [|]]; auto with arith.
  Qed.
  Hint Resolve between_Sk_l: arith.

  Lemma between_restr :
    forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.P, Q:nat -> Prop
forall k l m : nat,
k <= l -> l <= m -> between k m -> between l m
  Proof.P, Q:nat -> Prop
forall k l m : nat,
k <= l -> l <= m -> between k m -> between l m
    induction 1; auto with arith.
  Qed.

The exists_between type expresses the concept ∃ 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.P, Q:nat -> Prop
forall k l : nat, exists_between k l -> S k <= l
  Proof.P, Q:nat -> Prop
forall k l : nat, exists_between k l -> S k <= l
    induction 1; auto with arith.
  Qed.

  Lemma exists_lt : forall k l, exists_between k l -> k < l.P, Q:nat -> Prop
forall k l : nat, exists_between k l -> k < l
  Proof exists_le_S.
  Hint Immediate exists_le_S exists_lt: arith.

  Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.P, Q:nat -> Prop
forall k l : nat, exists_between k (S l) -> k <= l
  Proof.P, Q:nat -> Prop
forall k l : nat, exists_between k (S l) -> k <= l
    intros; apply le_S_n; auto with arith.
  Qed.
  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.P, Q:nat -> Prop
forall p q r : nat, p <= r -> r < q -> in_int p q r
  Proof.P, Q:nat -> Prop
forall p q r : nat, p <= r -> r < q -> in_int p q r
    split; assumption.
  Qed.
  Hint Resolve in_int_intro: arith.

  Lemma in_int_lt : forall p q r, in_int p q r -> p < q.P, Q:nat -> Prop
forall p q r : nat, in_int p q r -> p < q
  Proof.P, Q:nat -> Prop
forall p q r : nat, in_int p q r -> p < q
    intros * [].P, Q:nat -> Prop
p, q, r:nat
H:p <= r
H0:r < q
p < q
    eapply le_lt_trans; eassumption.
  Qed.

  Lemma in_int_p_Sq :
    forall p q r, in_int p (S q) r -> in_int p q r \/ r = q.P, Q:nat -> Prop
forall p q r : nat,
in_int p (S q) r -> in_int p q r \/ r = q
  Proof.P, Q:nat -> Prop
forall p q r : nat,
in_int p (S q) r -> in_int p q r \/ r = q
    intros p q r [].P, Q:nat -> Prop
p, q, r:nat
H:p <= r
H0:r < S q
in_int p q r \/ r = q
    destruct (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.P, Q:nat -> Prop
forall p q r : nat, in_int p q r -> in_int p (S q) r
  Proof.P, Q:nat -> Prop
forall p q r : nat, in_int p q r -> in_int p (S q) r
    intros * []; auto with arith.
  Qed.
  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.P, Q:nat -> Prop
forall p q r : nat, in_int (S p) q r -> in_int p q r
  Proof.P, Q:nat -> Prop
forall p q r : nat, in_int (S p) q r -> in_int p q r
    intros * []; auto with arith.
  Qed.
  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.P, Q:nat -> Prop
forall k l : nat,
between k l -> forall r : nat, in_int k l r -> P r
  Proof.P, Q:nat -> Prop
forall k l : nat,
between k l -> forall r : nat, in_int k l r -> P r
    induction 1; intros.P, Q:nat -> Prop
k, r:nat
H:in_int k k r
P r
P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:forall r0 : nat, in_int k l r0 -> P r0
r:nat
H1:in_int k (S l) r
P r
    -P, Q:nat -> Prop
k, r:nat
H:in_int k k r
P r absurd (k < k).P, Q:nat -> Prop
k, r:nat
H:in_int k k r
~ k < k
P, Q:nat -> Prop
k, r:nat
H:in_int k k r
k < k {P, Q:nat -> Prop
k, r:nat
H:in_int k k r
~ k < k auto with arith. }P, Q:nat -> Prop
k, r:nat
H:in_int k k r
k < k
      eapply in_int_lt; eassumption.
    -P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:forall r0 : nat, in_int k l r0 -> P r0
r:nat
H1:in_int k (S l) r
P r destruct (in_int_p_Sq k l r) as [| ->]; auto with arith.
  Qed.

  Lemma in_int_between :
    forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l.P, Q:nat -> Prop
forall k l : nat,
k <= l ->
(forall r : nat, in_int k l r -> P r) -> between k l
  Proof.P, Q:nat -> Prop
forall k l : nat,
k <= l ->
(forall r : nat, in_int k l r -> P r) -> between k l
    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.P, Q:nat -> Prop
forall k l : nat,
exists_between k l ->
exists2 m : nat, in_int k l m & Q m
  Proof.P, Q:nat -> Prop
forall k l : nat,
exists_between k l ->
exists2 m : nat, in_int k l m & Q m
    induction 1 as [* ? (p, ?, ?)|].P, Q:nat -> Prop
k, l:nat
H:exists_between k l
p:nat
H0:in_int k l p
H1:Q p
exists2 m : nat, in_int k (S l) m & Q m
P, Q:nat -> Prop
k, l:nat
H:k <= l
H0:Q l
exists2 m : nat, in_int k (S l) m & Q m
    -P, Q:nat -> Prop
k, l:nat
H:exists_between k l
p:nat
H0:in_int k l p
H1:Q p
exists2 m : nat, in_int k (S l) m & Q m exists p; auto with arith.
    -P, Q:nat -> Prop
k, l:nat
H:k <= l
H0:Q l
exists2 m : nat, in_int k (S l) m & Q m 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.P, Q:nat -> Prop
forall k l r : nat,
in_int k l r -> Q r -> exists_between k l
  Proof.P, Q:nat -> Prop
forall k l r : nat,
in_int k l r -> Q r -> exists_between k l
    intros * (?, lt_r_l) ?.P, Q:nat -> Prop
k, l, r:nat
H:k <= r
lt_r_l:r < l
H0:Q r
exists_between k l
    induction lt_r_l; 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.P, Q:nat -> Prop
forall k l : nat,
k <= l ->
(forall n : nat, in_int k l n -> P n \/ Q n) ->
between k l \/ exists_between k l
  Proof.P, Q:nat -> Prop
forall k l : nat,
k <= l ->
(forall n : nat, in_int k l n -> P n \/ Q n) ->
between k l \/ exists_between k l
    induction 1 as [|m ? IHle].P, Q:nat -> Prop
k:nat
(forall n : nat, in_int k k n -> P n \/ Q n) ->
between k k \/ exists_between k k
P, Q:nat -> Prop
k, m:nat
H:k <= m
IHle:(forall n : nat, in_int k m n -> P n \/ Q n) ->
between k m \/ exists_between k m
(forall n : nat, in_int k (S m) n -> P n \/ Q n) ->
between k (S m) \/ exists_between k (S m)
    -P, Q:nat -> Prop
k:nat
(forall n : nat, in_int k k n -> P n \/ Q n) ->
between k k \/ exists_between k k auto with arith.
    -P, Q:nat -> Prop
k, m:nat
H:k <= m
IHle:(forall n : nat, in_int k m n -> P n \/ Q n) ->
between k m \/ exists_between k m
(forall n : nat, in_int k (S m) n -> P n \/ Q n) ->
between k (S m) \/ exists_between k (S m) intros P_or_Q.P, Q:nat -> Prop
k, m:nat
H:k <= m
IHle:(forall n : nat, in_int k m n -> P n \/ Q n) ->
between k m \/ exists_between k m
P_or_Q:forall n : nat,
in_int k (S m) n -> P n \/ Q n
between k (S m) \/ exists_between k (S m)
      destruct IHle; auto with arith.P, Q:nat -> Prop
k, m:nat
H:k <= m
P_or_Q:forall n : nat,
in_int k (S m) n -> P n \/ Q n
H0:between k m
between k (S m) \/ exists_between k (S m)
      destruct (P_or_Q 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.P, Q:nat -> Prop
forall k l : nat,
between k l ->
(forall n : nat, in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
  Proof.P, Q:nat -> Prop
forall k l : nat,
between k l ->
(forall n : nat, in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
    induction 1; red; intros.P, Q:nat -> Prop
k:nat
H:forall n : nat, in_int k k n -> P n -> ~ Q n
H0:exists_between k k
False
P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
False
    -P, Q:nat -> Prop
k:nat
H:forall n : nat, in_int k k n -> P n -> ~ Q n
H0:exists_between k k
False absurd (k < k); auto with arith.
    -P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
False absurd (Q l).P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
~ Q l
P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
Q l {P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
~ Q l auto with arith. }P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
Q l
      destruct (exists_in_int k (S l)) as (l',[],?).P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
exists_between k (S l)
P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
Q l
      +P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
exists_between k (S l) auto with arith.
      +P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
Q l replace l with l'.P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
Q l'
P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
l' = l {P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
Q l' trivial. }P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
l' = l
        destruct (le_lt_or_eq l' l); auto with arith.P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
H6:l' < l
l' = l
        absurd (exists_between k l).P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
H6:l' < l
~ exists_between k l
P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
H6:l' < l
exists_between k l {P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
H6:l' < l
~ exists_between k l auto with arith. }P, Q:nat -> Prop
k, l:nat
H:between k l
H0:P l
IHbetween:(forall n : nat,
 in_int k l n -> P n -> ~ Q n) ->
~ exists_between k l
H1:forall n : nat, in_int k (S l) n -> P n -> ~ Q n
H2:exists_between k (S l)
l':nat
H3:k <= l'
H4:l' < S l
H5:Q l'
H6:l' < l
exists_between k l
        eapply in_int_exists; eauto 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).

  Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.P, Q:nat -> Prop
forall init l n : nat, P_nth init l n -> init <= l
  Proof.P, Q:nat -> Prop
forall init l n : nat, P_nth init l n -> init <= l
    induction 1.P, Q:nat -> Prop
init:nat
init <= init
P, Q:nat -> Prop
init, k, l, n:nat
H:P_nth init k n
H0:between (S k) l
H1:Q l
IHP_nth:init <= k
init <= l
    -P, Q:nat -> Prop
init:nat
init <= init auto with arith.
    -P, Q:nat -> Prop
init, k, l, n:nat
H:P_nth init k n
H0:between (S k) l
H1:Q l
IHP_nth:init <= k
init <= l eapply le_trans; eauto with arith.
  Qed.

  Definition eventually (n:nat) :=  exists2 k : nat, k <= n & Q k.

  Lemma event_O : eventually 0 -> Q 0.P, Q:nat -> Prop
eventually 0 -> Q 0
  Proof.P, Q:nat -> Prop
eventually 0 -> Q 0
    intros (x, ?, ?).P, Q:nat -> Prop
x:nat
H:x <= 0
H0:Q x
Q 0
    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.
Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.