Skip to content

Instantly share code, notes, and snippets.

@jeehoonkang
Created May 12, 2015 09:47
Show Gist options
  • Save jeehoonkang/4de7367737202f2c1062 to your computer and use it in GitHub Desktop.
Save jeehoonkang/4de7367737202f2c1062 to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment