6 Homework 7
Released: Wednesday, February 22, 2023 at 6:00pm
Due: Thursday, March 2, 2023 at 6:00pm
What to Download:
Please start with this file, filling in where appropriate, and submit your homework to the hw7 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.
Your overall task In this assignment, there are many theorems that have sorry as their proof. Your goal is to replace those with other tactics that complete the proof. If you are unable to complete a proof, you can always give up at any point with sorry, leaving whatever in-progress state you had.
6.1 Problem 1: Redoing proofs with tactics
In this first section, you’ll redo proofs you did in HW5, this time using tactics you have learned. Try to avoid using exact, or if you must use it, use it on small terms, rather than large terms that replicate what you did in HW5.
variable (P Q R S : Prop)
theorem t1 : P -> P :=
by sorry
theorem t2 : P -> Q -> P :=
by sorry
theorem t3 : (P -> Q) -> (Q -> R) -> P -> R :=
by sorry
theorem t4 : P -> Q -> (Q -> P -> R) -> R :=
by sorry
theorem t5 : (P -> Q) -> (P -> R) -> (R -> Q -> S) -> P -> S :=
by sorry
theorem t6 : (P -> Q -> R) -> (P -> Q) -> P -> R :=
by sorry
theorem p3 : P ∧ Q -> (Q -> R) -> R ∧ P :=
by sorry
theorem p4 : P ∨ Q -> (P -> R) -> (Q -> R) -> R :=
by sorry
theorem p5 : P ∨ Q -> (P -> R) -> R ∨ Q :=
by sorry
theorem p6 : ¬ Q -> (R -> Q) -> (R ∨ ¬ S) -> S -> False :=
by sorry
6.2 Problem 2: More complex logical proofs
In this problem, you’ll tackle a few more complex logical equivalences.
theorem and_distrib_or: ∀ A B C : Prop,
A ∧ (B ∨ C) ↔ (A ∧ B) ∨ (A ∧ C) := by sorry
theorem or_distrib_and: ∀ A B C : Prop,
A ∨ (B ∧ C) ↔ (A ∨ B) ∧ (A ∨ C) := by sorry
6.3 Problem 3: Induction on numbers and lists
Finally, you’ll do a few proofs that will likely require induction. Note that this entire assignment redefines the built in types Nat and List, and redefines many of the operations on them. The reason for doing that is the standard library has some automation that can get in the way of our proofs, at least to start. This way, all of the definitions used are readily available: it does mean that, for example, the special infix syntax for Lists is not available (as that is only for the built in ones).
When approaching inductive proofs, remember that it can be very tempting to "do induction again". That’s _rarely_ the right solution: usually, the answer is actually to start more generally (and perform induction before you have introduced any extra variables into the context, so that your inductive hypothesis is as strong as possible).
In these proofs, to help keep you within the rails, we’ve provided line counts for our reference proofs. We certainly don’t expect you to have the exact same numbers (and lines are a pretty poor metric of code), but if you see that we did a proof in 5 lines, and you’re at 50, it’s a good indication that maybe you should reconsider your approach. On the other hand, if we had 10, and you have 15, there is no reason to think you did anything wrong! And of course, if we did something in 8 that you did in 4, that is also fine!
def addtail (n m : Nat) : Nat :=
match n, m with
| Nat.zero, m => m
| Nat.succ n', m => addtail n' (Nat.succ m)
-- 8 lines
theorem addtail_succ : forall n m,
Nat.succ (addtail n m) = addtail (Nat.succ n) m :=
by sorry
-- 10 lines
theorem add_eq : forall n m, Nat.add n m = addtail n m :=
by sorry
-- 9 lines
theorem app_associative: ∀ L1 L2 L3 : List Nat,
List.append L1 (List.append L2 L3) =
List.append (List.append L1 L2) L3 :=
by sorry
-- 7 lines
theorem minus_x_x: ∀ x : Nat, Nat.sub x x = 0
:=
by sorry
-- 5 lines
theorem add_n_1 : ∀ x : Nat, Nat.add x 1 = Nat.succ x :=
by sorry
-- 9 lines
theorem mult_1_x: ∀ x : Nat, Nat.mul 1 x = x :=
by sorry
-- 7 lines
theorem add_assoc: ∀ x y z : Nat,
Nat.add x (Nat.add y z) = Nat.add (Nat.add x y) z :=
by sorry
-- 6 lines
theorem add_x_Sy : forall x y,
Nat.add x (Nat.succ y) = Nat.succ (Nat.add x y) :=
by sorry
-- 4 lines
theorem add_n_0 : forall n, Nat.add n Nat.zero = n :=
by sorry
-- 13 lines
theorem mult_2_x: ∀ x : Nat, Nat.mul 2 x = Nat.add x x :=
by sorry
-- 10 lines
theorem length_append : forall (T : Type) (L1 L2 : List T),
List.length (List.append L1 L2) = Nat.add (List.length L1) (List.length L2) :=
by sorry
-- 8 lines
theorem rev_length: ∀ L : List Nat,
List.length (List.reverse L) = List.length L :=
by sorry
-- Consider the following pair of definitions
def even : Nat -> Bool
| 0 => true
| 1 => false
| Nat.succ (Nat.succ n) => even n
def double : Nat → Nat
| 0 => 0
| (Nat.succ x) => Nat.succ (Nat.succ (double x))
-- 5 lines
theorem even_double: ∀ x : Nat, even (double x) = true :=
by sorry