# Induction, rewriting, and beginning reflection

 Due 2019-9-26 11:45AM Reading Programs and Proofs: Chapter 4, Chapter 5, Mathematical Components: Chapter 3, Chapter 4 Link https://github.ccs.neu.edu/verifcomp/19/asgn/2.v
This assignment will explore more complex proofs.

Require Import mathcomp.ssreflect.all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".

Exercise 1. Prove the equivalence of addition defined tail recursively and the standard non-tail recursive built-in definition.
Fixpoint addtail (n m : nat) : nat :=
match n, m with
| 0, m => m
| n'.+1, m => addtail n' (m.+1)
end.

# Note:

Exercises 2-4 are lemmas that exist in the standard library. Obviously, don't just appeal to the corresponding lemma, and also, don't look at the source of those proofs (if you do decide to do so, note that the later exercises are not in the standard library, and are harder, so you're better off practicing with 2-4!).
Exercise 2.
Theorem cat_size {T : Type} : forall (s1 s2 : seq T),
size (s1 ++ s2) = size s1 + size s2.

Exercise 3.
Theorem last_last {T : Type} : forall (x : T) s1 s2,
last x (s1 ++ s2) = last (last x s1) s2.

Exercise 4. (MASTERS CREDIT ONLY)
Theorem drop_take {T : Type} : forall (n : nat) (s : seq T),
take n s ++ drop n s = s.

Exercise 5.
Lemma subtriv : forall p n, n.+1 - p = n.+1 -> p = 0.

Exercise 6.
Lemma succ_max_distr' n m : (maxn n m).+1 >= maxn (n.+1) m.