mid_08.v

Require Export mid_07.

(* problem #08: 30 points *)

(** Easy:
    Define a predicate [sorted_min: nat -> list nat -> Prop], where
    [sorted_min n l] holds iff the elements in the list [l] is greater
    than or equal to [n] and sorted in the increasing order.
 **)

Inductive sorted_min: nat -> list nat -> Prop :=
   | sort_0 : forall (n: nat), sorted_min n []
   | sort_2 : forall (n m: nat) (l: list nat), n <= m -> sorted_min n l -> sorted_min n (m::l) 
.

Lemma O_le_n: forall n,
  0 <= n.
Proof.
  induction n.
  apply le_n.
  apply le_S.
  apply IHn.
Qed.
  


Example sorted_min_example1: sorted_min 0 [1; 3; 4; 4; 5].
Proof. 
  apply sort_2.
  apply O_le_n.
  apply sort_2.
  apply O_le_n.
  apply sort_2.
  apply O_le_n.
  apply sort_2.
  apply O_le_n.
  apply sort_2.
  apply O_le_n.
  apply sort_0.
Qed.

Example sorted_min_example2: sorted_min 2 [2; 2; 3; 6].
Proof. 
  apply sort_2.
  apply le_n.
  apply sort_2.
  apply le_n.
  apply sort_2.
  apply le_S.
  apply le_n.
  apply sort_2.
  apply le_S; apply le_S; apply le_S; apply le_S.
  apply le_n.
  apply sort_0.

Example sorted_min_non_example1: sorted_min 1 [0; 1] -> False.
Proof. 
  intros.
  inversion H.
  inversion H3.
Qed.





(** Medium:
    Prove the following theorem. 
 **)

Inductive appears_in (n : nat) : list nat -> Prop :=
| ai_here : forall l, appears_in n (n::l)
| ai_later : forall m l, appears_in n l -> appears_in n (m::l).

Lemma lem0: forall n m l,
  appears_in n (m :: l) -> n <> m -> appears_in n l.
Proof.
  intros.
  unfold not in H0.
  inversion H.
  apply H0 in H2.
  inversion H2.
  apply H2.
Qed.

Lemma le_trans: forall n m o,
  n <= m -> m <= o -> n <= o.
Proof.
  intros.
  induction H0.
  apply H.
  apply le_S.
  apply IHle.
Qed.

Lemma lem1: forall n m o,
  S n <= m -> m <= o -> n < o.
Proof.
  intros.
  unfold lt.
  apply le_trans with (n := S n) (m := m) (o := o).
  apply H.
  apply H0.
Qed.

Lemma lem12: forall n,
  n = S n -> False.
Proof.
  intros.
  induction n.
  inversion H.
  apply IHn.
  inversion H.
  apply H.
Qed.



Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros.
  inversion H.
  apply le_n.
  apply le_trans with (m := S n).
  apply le_S.
  apply le_n.
  apply H1.
Qed.


Lemma lem2: forall n ,
  S n <= n -> False.
Proof.
  intros.
  induction n.
  inversion H.
  apply IHn.
  apply Sn_le_Sm__n_le_m in H.
  apply H.
Qed.
  
  

Lemma sorted_not_in: forall n m l
    (SORTED: sorted_min m l)
    (LT: n < m),
  ~ appears_in n l.
Proof.
  unfold lt.
  unfold not.
  intros.
  induction SORTED.
  inversion H.
  apply IHSORTED.
  apply LT.
  apply lem0 in H.
  apply H.
  unfold not.
  intros.
  assert (S n <= m).
  apply lem1 with (m := n0).
  apply LT.
  apply H0.
  assert (n < m).
  unfold lt.
  apply H2.
  rewrite H1 in H2.
  apply lem2 in H2.
  apply H2.
Qed.









(** Hard:
    Prove the following theorem.
 **)

(* [beq_nat n m] returns [true]  if [n = m] holds; 
                 returns [false] otherwise. *)
Check beq_nat.
Check beq_nat_false.
Check beq_nat_true.
Check beq_nat_refl.

(* [ltb n m] returns [true]  if [n < m] holds; 
             returns [false] otherwise.
   Note that [ltb n m] is displayed as [n <? m]. *)
Check ltb.
Check ltb_lt.

Fixpoint appears_inb (n: nat) (l: list nat) : bool :=
  match l with
  | nil => false
  | m :: l' => 
    if ltb n m
    then false
    else (if beq_nat n m
          then true
          else appears_inb n l')
  end.

Theorem appears_inb_correct: forall n l
    (SORTED: sorted_min 0 l)
    (NOTAPPEAR: appears_inb n l = false),
  ~ appears_in n l.
Proof.
  Admitted.
Qed