Require Import Coq.Arith.PeanoNat.
Require Import Coq.Logic.EqdepFacts.

Inductive OrderedNums : nat -> list nat -> Prop :=
  | FoundAll : forall (l : list nat), OrderedNums 0 (cons 0 l)
  | FoundNext : forall (n : nat) (l : list nat),
      OrderedNums n l -> OrderedNums (S n) (cons (S n) l)
  | Skip : forall (n x : nat) (l : list nat),
      OrderedNums n l -> OrderedNums n (cons x l).

Fact orderedThree : OrderedNums 3 (cons 3 (cons 2 (cons 2 (cons 1 (cons 0 nil))))).
Proof. 
  apply FoundNext.
  apply FoundNext.
  apply Skip.
  apply FoundNext.
  apply FoundAll.
Qed.

Fixpoint check_numbers (k : nat) (v : list nat) : bool :=
  match v with
  | nil => false
  | cons n v =>
      if Nat.eq_dec k n
      then
        match k with
        | 0 => true
        | (S k') => check_numbers k' v
        end
      else check_numbers k v
  end.

Theorem check_numbers_one : forall (k : nat) (l : list nat),
  check_numbers k l = true -> OrderedNums k l.
Proof.
  intros k l Heq.
  generalize dependent k.
  (* Go by induction on l. *)
  induction l; intros k Heq; simpl in Heq.
  - (* List is empty, algorithm couldn't have returned true. *)
    discriminate Heq.
  - (* List is not empty; what we do next depends on whether k is equal or not. *)
    destruct (Nat.eq_dec k a) eqn:Heqk.
    + (* k is equal, so we either recurse (if it' not zero), or we're done (if it's zero). *)
      destruct k; subst.
      * (* k is zero, so we've found all the numbers *)
        apply FoundAll.
      * (* k is not zero, we go on looking, which is correct by the induction hypothesis. *)
        apply FoundNext. auto.
    + (* k didn't match. We go on looking, and it's correct by the induction hypothesis. *)
      apply Skip. auto.
Qed.

Require Import Coq.Program.Equality.

Lemma check_numbers_suc : forall (k : nat) (v : list nat),
  OrderedNums (S k) v -> OrderedNums k v.
Proof.
  intros k v Hsk.
  dependent induction Hsk.
  - apply Skip. auto.
  - apply Skip. apply IHHsk. auto.
Qed.

Lemma check_numbers_suc_p : forall (k : nat) (v : list nat),
  ~ OrderedNums k v -> ~ OrderedNums (S k) v.
Proof.
  intros k v Hk HSk.
  apply Hk. apply check_numbers_suc. auto.
Qed.

Theorem check_numbers_two : forall (k : nat) (l : list nat),
  check_numbers k l = false -> ~ OrderedNums k l.
Proof.
  intros k l.
  generalize dependent k.
  (* Go by induction on the list. *)
  induction l; intros k Heq Hk.
  - (* The list is empty, so we can't have ordered numbers. *)
    inversion Hk.
  - (* The evaluation depends on whether or not k is equal to the given number. *)
    simpl in Heq. destruct (Nat.eq_dec k a) eqn:Heqk.
    + (* k is equal to the number; what we do next depends on k. *)
      destruct k; subst.
      * (* k is zero, so we return true. Contradictory assumption. *)
        inversion Heq.
      * (* k is not zero, we make a recurisve call. *)
        (* k = S k'. So the recursive call returns false, and we know that
           there aren't k' numbers in a row. *)
        inversion Hk; subst;
        (* We know that if there are no k' numbers, there also can't be k numbers. *)
        specialize (check_numbers_suc k l) as Hsuc;
        (* We know there are no k' numbers by induction. *)
        specialize (IHl k Heq);
        auto.
    + (* k is not equal to the number. We just go by induction. *)
      specialize (IHl k Heq). inversion Hk; subst; auto.
Qed.