7 Homework 9
Released: Monday, March 13, 2023 at 6:00pm
Due: Wednesday, March 22, 2023 at 6:00pm
What to Download:
Please start with this file, filling in where appropriate, and submit your homework to the hw9 assignment on Gradescope. This page has additional information, and allows us to format things nicely.
To do this assignment in the browser: Create a Codespace.
In this homework assignment, you will get significantly more practice doing more challenging proofs in Lean.
As before, we provide line counts for how long our reference solutions are: these are not the only ways to do the proofs (and you will not be penalized if you proofs take longer), and lines are a poor metric of complexity (as you can easily make things more compact or spread out), but are intended as a tool to help you not go too far down a path that isn’t working. For example, if we had a proof that took 20 lines, and you are 100 lines into an attempt and it isn’t working, it might be an indication that you made a decision (choice of what to do induction on, etc) that isn’t working.
7.1 Problem 1: Append and Reverse
First, a few proofs about append and reverse. For this assignment, we are using the standard library data structures, but here we define our own definition of append (called app), instead of List.append, and our own reverse (called rev) instead of List.reverse.
def app : List Nat -> List Nat -> List Nat
| List.nil, bs => bs
| List.cons a as, bs => List.cons a (app as bs)
def rev : List Nat -> List Nat
| List.nil => List.nil
| List.cons a L => app (rev L) (List.cons a List.nil)
-- 6 lines
theorem app_nil : forall (l : List Nat), app l [] = l :=
by sorry
-- 6 lines
theorem app_assoc : forall (l1 l2 l3 : List Nat),
app (app l1 l2) l3 = app l1 (app l2 l3) :=
by sorry
-- 8 lines
theorem rev_app_distr: forall l1 l2 : List Nat,
rev (app l1 l2) = app (rev l2) (rev l1) :=
by sorry
-- 8 lines
theorem rev_involutive : forall l : List Nat,
rev (rev l) = l :=
by sorry
7.2 Problem 2: Evenness (and Relations)
In this problem, you will practice more with expressing properties using relations (rather than boolean predicates). Here we have two different definitions of evenness (one of which you have seen in lecture before), and among other proofs, you will prove that the two are equivalent.
inductive ev : Nat -> Prop
| O : ev 0
| SS (n : Nat) (H : ev n) : ev (Nat.succ (Nat.succ n))
def double : Nat -> Nat
| 0 => 0
| Nat.succ n => Nat.succ (Nat.succ (double n))
-- 5 lines
theorem ev_double : forall n, ev (double n) :=
by sorry
-- 15 lines
theorem ev_sum : forall n m, ev n -> ev m -> ev (Nat.add n m) :=
by sorry
-- 3 lines
theorem three_not_ev : Not (ev 3) :=
by sorry
inductive ev' : Nat -> Prop :=
| O : ev' 0
| SSO : ev' 2
| sum n m (Hn : ev' n) (Hm : ev' m) : ev' (Nat.add n m)
-- 21 lines
theorem ev'_ev : forall n, ev' n <-> ev n :=
by sorry
7.3 Problem 3: Subsequences
In this problem, you will see a new relation, expressing when one list of natural numbers is a subsequence of another. To practice dealing with the relation (and understand how it works), you will prove a few properties about it.
inductive subseq : List Nat -> List Nat -> Prop
| empty : subseq [] []
| include x l1 l2 (H : subseq l1 l2) : subseq (x::l1) (x::l2)
| skip x l1 l2 (H : subseq l1 l2) : subseq l1 (x::l2)
-- 6 lines
theorem subseq_refl : forall (l : List Nat),
subseq l l :=
by sorry
-- 5 lines
theorem subseq_empty : forall l, subseq [] l :=
by sorry
-- 13 lines
theorem subseq_app : forall (l1 l2 l3 : List Nat),
subseq l1 l2 ->
subseq l1 (List.append l2 l3) :=
by sorry
7.4 Problem 4: Insertion Sort
In this problem, you will prove insertion sort is correct. This will be done in several steps, first by proving various properties about the insert function, which you will then be able to use to prove the same properties about isort.
There are two halves of the problem: first, to prove that isort (and insert) produces sorted lists, where we have a relation that defines what it means to be sorted. This relation uses another relation, All, as a helper: All is a relation that holds when a property holds for all elements of a list, in this case, we use it to show that the front of a sorted list is less or equal to all other elements of the list.
The other half of the problem is to ensure that isort (and insert) produce permutations of the input lists. This relies upon a new definition of permutation, which is a relation that holds when two lists have the same elements, but possibly in a different order. To practice with this definition (which is similar to the subsequence definition from Problem 3), we have a few theorems for you to prove, before proving the main results.
We provide a few helper theorems that you may use in your proofs (we did in ours). In general, defining helper theorems is a good idea, as it can help you break down a problem into smaller pieces.
Note: the proofs for the insert functions are where most of the work is!
def insert : Nat -> List Nat -> List Nat
| y, [] => [y]
| y, x::xs => if Nat.ble y x
then y :: x :: xs
else x :: insert y xs
def isort : List Nat -> List Nat
| [] => []
| x :: xs => insert x (isort xs)
inductive All : {T : Type} -> (T -> Prop) -> List T -> Prop
| nil : All P []
| cons : forall x L, P x -> All P L -> All P (x :: L)
inductive Sorted : List Nat -> Prop
| nil : Sorted []
| cons : forall n l, Sorted l ->
All (Nat.le n) l ->
Sorted (n :: l)
theorem all_trans : forall (P : T -> Prop) (Q : T -> Prop) L,
All P L ->
(forall x, P x -> Q x) ->
All Q L :=
by intros P Q L Hall PtoQ
induction Hall
case nil => constructor
case cons P x L Px HL =>
constructor
apply PtoQ
assumption
assumption
-- 23 lines
theorem insert_le : forall n x l,
All (Nat.le n) l ->
Nat.le n x ->
All (Nat.le n) (insert x l) :=
by sorry
theorem ble_inv : forall a b,
Nat.ble a b = false
-> Nat.ble b a = true :=
by intros a b H
rw [Nat.ble_eq]
cases (Nat.le_total b a)
assumption
rw [<- Nat.not_lt_eq]
rw [<- Bool.not_eq_true] at H
rw [Nat.ble_eq] at H
contradiction
-- 37 lines
theorem insert_sorted : forall x l,
Sorted l ->
Sorted (insert x l) :=
by sorry
-- 8 lines
theorem isort_sorted : forall l, Sorted (isort l) :=
by sorry
inductive Permutation : {T : Type} -> List T -> List T -> Prop
| nil : Permutation [] []
| skip : forall (x : A) (l l' : List A),
Permutation l l' ->
Permutation (x :: l) (x :: l')
| swap : forall (x y : A) (l : List A),
Permutation (y :: x :: l) (x :: y :: l)
| trans : forall l l' l'' : List A,
Permutation l l' ->
Permutation l' l'' ->
Permutation l l''
example : Permutation [true,true,false] [false,true,true] :=
by apply Permutation.trans (l' := [true,false,true])
. apply Permutation.skip
apply Permutation.swap
. apply Permutation.swap
-- 6 lines
theorem perm_refl : forall {T : Type} (l : List T),
Permutation l l :=
by sorry
-- 10 lines
theorem perm_length : forall {T : Type} (l1 l2 : List T),
Permutation l1 l2 -> l1.length = l2.length :=
by sorry
-- 12 lines
theorem perm_sym : forall {T : Type} (l1 l2 : List T),
Permutation l1 l2 -> Permutation l2 l1 :=
by sorry
-- 18 lines
theorem insert_perm : forall x l,
Permutation (x :: l) (insert x l) :=
by sorry
-- 10 lines
theorem isort_perm : forall l, Permutation l (isort l) :=
by sorry