Day17_indprop2
Reasoning about minima
Exercise: 3 stars, standard, optional (le_exercises)
Here are a number of facts about the ≤ and < relations that we are going to need later in the course. The proofs make good practice exercises.
Lemma le_trans : ∀ m n o, m ≤ n → n ≤ o → m ≤ o.
Proof.
(* FILL IN HERE *) Admitted.
Theorem O_le_n : ∀ n,
0 ≤ n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem n_le_m__Sn_le_Sm : ∀ n m,
n ≤ m → S n ≤ S m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem Sn_le_Sm__n_le_m : ∀ n m,
S n ≤ S m → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Lemma leb_nm__leb_mn : ∀ (n m : nat),
leb n m = false → leb m n = true.
Proof.
(* FILL IN HERE *) Admitted.
Lemma leb_spec : ∀ (n m : nat),
leb n m = true ∨ (leb n m = false ∧ leb m n = true).
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
Theorem O_le_n : ∀ n,
0 ≤ n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem n_le_m__Sn_le_Sm : ∀ n m,
n ≤ m → S n ≤ S m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem Sn_le_Sm__n_le_m : ∀ n m,
S n ≤ S m → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Lemma leb_nm__leb_mn : ∀ (n m : nat),
leb n m = false → leb m n = true.
Proof.
(* FILL IN HERE *) Admitted.
Lemma leb_spec : ∀ (n m : nat),
leb n m = true ∨ (leb n m = false ∧ leb m n = true).
Proof.
(* FILL IN HERE *) Admitted.
We can even view leb_nm__leb_mn as a specialization of leb_spec:
Lemma leb_nm__leb_mn' : ∀ (n m : nat),
leb n m = false → leb m n = true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_complete : ∀ n m,
leb n m = true → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem le_plus_l : ∀ a b,
a ≤ a + b.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_lt : ∀ n1 n2 m,
n1 + n2 < m →
n1 < m ∧ n2 < m.
Proof.
unfold lt.
(* FILL IN HERE *) Admitted.
Lemma minus_Sn_m: ∀ n m : nat,
m ≤ n → S (n - m) = S n - m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem lt_S : ∀ n m,
n < m →
n < S m.
Proof.
(* FILL IN HERE *) Admitted.
leb n m = false → leb m n = true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_complete : ∀ n m,
leb n m = true → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem le_plus_l : ∀ a b,
a ≤ a + b.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_lt : ∀ n1 n2 m,
n1 + n2 < m →
n1 < m ∧ n2 < m.
Proof.
unfold lt.
(* FILL IN HERE *) Admitted.
Lemma minus_Sn_m: ∀ n m : nat,
m ≤ n → S (n - m) = S n - m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem lt_S : ∀ n m,
n < m →
n < S m.
Proof.
(* FILL IN HERE *) Admitted.
Hint: The next one may be easiest to prove by induction on m.
Hint: This theorem can easily be proved without using induction.
Theorem leb_true_trans : ∀ n m o,
leb n m = true → leb m o = true → leb n o = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
leb n m = true → leb m o = true → leb n o = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (min3_min)
Lemma min3_min : ∀ n1 n2 n3,
min3 n1 n2 n3 ≤ n1 ∧
min3 n1 n2 n3 ≤ n2 ∧
min3 n1 n2 n3 ≤ n3.
Proof.
(* FILL IN HERE *) Admitted.
☐
min3 n1 n2 n3 ≤ n1 ∧
min3 n1 n2 n3 ≤ n2 ∧
min3 n1 n2 n3 ≤ n3.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, optional (min3_leb)
Lemma min3_leb : ∀ n1 n2 n3 m,
n1 ≤ m ∨ n2 ≤ m ∨ n3 ≤ m →
min3 n1 n2 n3 ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
n1 ≤ m ∨ n2 ≤ m ∨ n3 ≤ m →
min3 n1 n2 n3 ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
A hint.
Check argmin3_min3.
Lemma argmin3_min : ∀ {A:Type} cost (o1 o2 o3:A),
cost (argmin3 cost o1 o2 o3) ≤ cost o1 ∧
cost (argmin3 cost o1 o2 o3) ≤ cost o2 ∧
cost (argmin3 cost o1 o2 o3) ≤ cost o3.
Proof.
(* FILL IN HERE *) Admitted.
Lemma argmin3_leb : ∀ {A:Type} cost (o1 o2 o3:A) other,
cost o1 ≤ cost other ∨ cost o2 ≤ cost other ∨ cost o3 ≤ cost other →
cost (argmin3 cost o1 o2 o3) ≤ cost other.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma argmin3_min : ∀ {A:Type} cost (o1 o2 o3:A),
cost (argmin3 cost o1 o2 o3) ≤ cost o1 ∧
cost (argmin3 cost o1 o2 o3) ≤ cost o2 ∧
cost (argmin3 cost o1 o2 o3) ≤ cost o3.
Proof.
(* FILL IN HERE *) Admitted.
Lemma argmin3_leb : ∀ {A:Type} cost (o1 o2 o3:A) other,
cost o1 ≤ cost other ∨ cost o2 ≤ cost other ∨ cost o3 ≤ cost other →
cost (argmin3 cost o1 o2 o3) ≤ cost other.
Proof.
(* FILL IN HERE *) Admitted.
☐
Case study: getting natset right
Fixpoint is_setlike (l : natset) : bool :=
match l with
| [] ⇒ true
| x :: l' ⇒ negb (member x l') && is_setlike l'
end.
Fixpoint intersection (l1 l2 : natset) : natset :=
match l1 with
| [] ⇒ []
| x::l1' ⇒ if member x l2
then x::intersection l1' l2
else intersection l1' l2
end.
Fixpoint subset (l1 l2 : natset) : bool :=
match l1 with
| [] ⇒ true
| x::l1' ⇒ member x l2 && subset l1' l2
end.
match l with
| [] ⇒ true
| x :: l' ⇒ negb (member x l') && is_setlike l'
end.
Fixpoint intersection (l1 l2 : natset) : natset :=
match l1 with
| [] ⇒ []
| x::l1' ⇒ if member x l2
then x::intersection l1' l2
else intersection l1' l2
end.
Fixpoint subset (l1 l2 : natset) : bool :=
match l1 with
| [] ⇒ true
| x::l1' ⇒ member x l2 && subset l1' l2
end.
We can characterize those natsets which are setlike using an
inductive predicate.
Inductive setlike : natset → Prop :=
| setlike_nil : setlike []
| setlike_cons (x:nat) (l:natset) (Hin: ¬ In x l) (H: setlike l) : setlike (x :: l).
| setlike_nil : setlike []
| setlike_cons (x:nat) (l:natset) (Hin: ¬ In x l) (H: setlike l) : setlike (x :: l).
Exercise: 2 stars, standard (setlike_egs)
Let's get a feel for the setlike predicate. It's always important to have positive examples---things that should satisfy the property, like setlike_eg1---as well as negative examples---things that should not satisfy the property, like setlike_eg2.
Example setlike_eg1 :
setlike [1;2;3;4].
Proof.
(* FILL IN HERE *) Admitted.
Example setlike_eg2 :
¬ setlike [1;2;3;4;1].
Proof.
(* FILL IN HERE *) Admitted.
☐
setlike [1;2;3;4].
Proof.
(* FILL IN HERE *) Admitted.
Example setlike_eg2 :
¬ setlike [1;2;3;4;1].
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, optional (In_member_iff)
The member function returns true exactly when the In predicate holds. This is good practice about inductive proof; it's needed for the next few exercises (but you can do them without doing this proof!).Exercise: 2 stars, standard (is_setlike__setlike)
We should, as always, double check our ideas. We have a setlike predicate on sets defined inductively and an is_setlike function defined recursively. Do these notions coincide?
Lemma is_setlike__setlike : ∀ l,
is_setlike l = true ↔ setlike l.
Proof.
(* FILL IN HERE *) Admitted.
☐
is_setlike l = true ↔ setlike l.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma insert_preserves_setlike : ∀ x l,
setlike l →
setlike (set_insert x l).
Proof.
(* FILL IN HERE *) Admitted.
☐
setlike l →
setlike (set_insert x l).
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma union_preserves_setlike : ∀ l1 l2,
setlike l1 →
setlike l2 →
setlike (union l1 l2).
Proof.
(* FILL IN HERE *) Admitted.
☐
setlike l1 →
setlike l2 →
setlike (union l1 l2).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, standard, optional (union_intersection_dist)
The setlike predicate isn't just useful for checking that we've implemented our operations correctly---sometimes we need to use setlike in proofs!
Lemma union_intersection_dist : ∀ l1 l2 l3,
setlike l1 → setlike l2 → setlike l3 →
intersection (union l1 l2) l3 =
union (intersection l1 l3) (intersection l2 l3).
Proof.
(* FILL IN HERE *) Admitted.
☐
setlike l1 → setlike l2 → setlike l3 →
intersection (union l1 l2) l3 =
union (intersection l1 l3) (intersection l2 l3).
Proof.
(* FILL IN HERE *) Admitted.
☐
(* 2021-09-28 15:37 *)