Indprop2

Require Export DMFP.Indprop.

Reasoning about minima

As practice with ≤, we'll prove some properties about min3 and argmin3. We'll need these properties to show that some edit functions are 'better' than others.
To do so, we'll need a bunch of other results. These are great practice problems. We won't grade them, but if you're having trouble understanding inductive propositions, doing some of these will defiitely help.

Exercise: 4 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.
Even if you don't do these proofs, look carefully at the properties... these are very useful facts!
Lemma le_trans : ∀ m n o, m ≤ n → n ≤ o → m ≤ o.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: le_trans *)
Theorem O_le_n : ∀ n,
    0 ≤ n.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: O_le_n *)
Theorem n_le_m__Sn_le_Sm : ∀ n m,
    n ≤ m → S n ≤ S m.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: n_le_m__Sn_le_Sm *)
Theorem Sn_le_Sm__n_le_m : ∀ n m,
    S n ≤ S m → n ≤ m.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: Sn_le_Sm__n_le_m *)
Lemma leb_nm__leb_mn : ∀ (n m : nat),
    leb n m = false → leb m n = true.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: leb_nm__leb_mn *)
Lemma leb_spec : ∀ (n m : nat),
    leb n m = true ∨ (leb n m = false ∧ leb m n = true).
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: leb_spec *)
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.
(* GRADE_THEOREM 0.25: leb_nm__leb_mn' *)
Theorem leb_complete : ∀ n m,
    leb n m = true → n ≤ m.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: leb_complete *)
Theorem le_plus_l : ∀ a b,
    a ≤ a + b.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: le_plus_l *)
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.
(* GRADE_THEOREM 0.25: minus_Sn_m *)
Theorem lt_S : ∀ n m,
    n < m →
    n < S m.
Proof.
  (* FILL IN HERE *) Admitted.
(* GRADE_THEOREM 0.25: lt_S *)
Hint: The next one may be easiest to prove by induction on m.
Theorem leb_correct : ∀ n m,
    n ≤ m →
    leb n m = true.
Proof.
  (* FILL IN HERE *) Admitted.
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.
(* GRADE_THEOREM 0.25: leb_true_trans *)
☐

Exercise: 1 star, standard, optional (leb_iff)

Same here: just reuse some results.
Theorem leb_iff : ∀ n m,
    leb n m = true ↔ n ≤ m.
Proof.
  (* FILL IN HERE *) Admitted.
☐
Okay: let's get down to business. This lemma is the linchpin. You'll want to use leb_nm__leb_mn or leb_spec to get things right here; also remember that you can destruct compound expressions!
The key idea here is you need to find a way to simplify the min3 operations by thinking about the possible cases---here, the cases you want are the ones that take you to different branches of min3.
This is not going to be an induction proof!

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.
☐
These next three lemmas should all follow from min3_min and previous lemmas.

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.
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.
☐

In and All

The logical connectives that we have seen provide a rich vocabulary for defining complex propositions from simpler ones. To illustrate, let's look at how to express the claim that an element x occurs in a list l. Notice that this property has a simple recursive structure:
  • If l is the empty list, then x cannot occur on it, so the property "x appears in l" is simply false.
  • Otherwise, l has the form x' :: l'. In this case, x occurs in l if either it is equal to x' or it occurs in l'.
We can translate this directly into an inductive proposition:
Inductive In {A : Type} : A → list A → Prop :=
| In_here (x:A) (l:list A) : In x (x::l)
| In_cons (x y:A) (l:list A) (H: In x l) : In x (y::l).
Example In_example_1 : In 4 [1; 2; 3; 4; 5].
Proof.
  (* WORKED IN CLASS *)
  apply In_cons.
  apply In_cons.
  apply In_cons.
  apply In_here.
Qed.
Example In_example_2 :
  ∀ n, In n [2; 4] →
  ∃ n', n = 2 × n'.
Proof.
  (* WORKED IN CLASS *)
  intros n HIn.
  inversion HIn as [x l' | x y l' HRest].
  - ∃ 1. reflexivity.
  - inversion HRest as [x' l'' | x' y' l'' []].
    ∃ 2. reflexivity.
Qed.
(Notice the use of the empty pattern to discharge the last case en passant.)
We can also prove more generic, higher-level lemmas about In.
Note, in the next, how In starts out applied to a variable and only gets expanded when we do case analysis on this variable:
Lemma In_map :
  ∀ (A B : Type) (f : A → B) (l : list A) (x : A),
    In x l →
    In (f x) (map f l).
Proof.
  (* Let A, B, f, l, and x be given.  WTP In x l → In (f x) (map f l). *)
  intros A B f l x HIn.
  (* We go by induction on _how we know_ In x l *)
  induction HIn as [ y l' | y z l' HRest IH].
  - apply In_here.
  - simpl map.
    apply In_cons.
    apply IH.
Qed.

Exercise: 2 stars, standard (In_map_iff)

Lemma In_map_iff :
  ∀ (A B : Type) (f : A → B) (l : list A) (y : B),
    In y (map f l) ↔
    ∃ x, f x = y ∧ In x l.
Proof.
  intros A B f l y. split.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard, optional (In_app_iff)

Lemma In_app_iff : ∀ A l l' (a:A),
  In a (l++l') ↔ In a l ∨ In a l'.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard, optional (In_flat_map)

Fixpoint flat_map {X Y: Type} (f: X → list Y) (l: list X)
                   : (list Y) :=
  match l with
  | [] ⇒ []
  | h :: t ⇒ (f h) ++ (flat_map f t)
  end.
Lemma In_flat_map:
  ∀ (A B : Type) (f : A → list B) (l : list A) (y : B),
  In y (flat_map f l) → (∃ x : A, In y (f x) ∧ In x l).
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 3 stars, standard, especially useful (All_In)

All, below, is to forallb as In is to member from the sorting chapter.
Inductive All {T : Type} : (T → Prop) → list T → Prop :=
| All_nil (P:T → Prop) : All P []
| All_cons (P:T → Prop) (t:T) (l:list T) (H1: P t) (H2:All P l) : All P (t::l).
Lemma All_In :
  ∀ T (P : T → Prop) (l : list T),
    (∀ x, In x l → P x) ↔
    All P l.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard, especially useful (All_forallb)

Recall the function forallb::
Fixpoint forallb {X : Type} (test : X → bool) (l : list X) : bool :=
  match l with
  | [] ⇒ true
  | x :: l' ⇒ andb (test x) (forallb test l')
  end.
Prove the theorem below, which relates forallb to the All property of the above exercise.
Theorem forallb_true_iff : ∀ X test (l : list X),
   forallb test l = true ↔ All (fun x ⇒ test x = true) l.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Case study: getting natset right

There's an important set of properties that we haven't proved about our no-duplicates invariant for list-based sets of naturals: that we maintain the natset invariant that each element appears at most once!
Before we begin, we'll insert our own definitions of some operations you defined a while back.
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.
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).

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.
☐

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!).
Lemma In_member_iff : ∀ x l,
    In x l ↔ member x l = true.
Proof.
  (* FILL IN HERE *) Admitted.
☐

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.
☐

Exercise: 2 stars, standard (insert_preserves_setlike)

Lemma insert_preserves_setlike : ∀ x l,
    setlike l →
    setlike (set_insert x l).
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard (union_preserves_setlike)

Lemma union_preserves_setlike : ∀ l1 l2,
    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!
Prove that intersection distributes over union. (You may be more familiar with distributivity from arithmetic: x × (y + z) = (x × y) + (x × z).)
You'll need several helper lemmas to prove this! A useful tip for helper lemmas: don't prove them right away, just use Admitted to see if they would let you finish your proof. If you prove them right away, you might spend a long time proving a helper lemma that isn't so... helpful.
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.
☐
(* 2022-01-12 10:20 *)