# File 2

# 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 |

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.

Theorem add_eq : forall n m, addn n m = addtail n m.

Admitted.

match n, m with

| 0, m => m

| n'.+1, m => addtail n' (m.+1)

end.

Theorem add_eq : forall n m, addn n m = addtail n m.

Admitted.

# Note:

*not*in the standard library, and are harder, so you're better off practicing with 2-4!).

Theorem cat_size {T : Type} : forall (s1 s2 : seq T),

size (s1 ++ s2) = size s1 + size s2.

Admitted.

size (s1 ++ s2) = size s1 + size s2.

Admitted.

Exercise 3.

Theorem last_last {T : Type} : forall (x : T) s1 s2,

last x (s1 ++ s2) = last (last x s1) s2.

Admitted.

last x (s1 ++ s2) = last (last x s1) s2.

Admitted.

Exercise 4. (MASTERS CREDIT ONLY)

Theorem drop_take {T : Type} : forall (n : nat) (s : seq T),

take n s ++ drop n s = s.

Admitted.

take n s ++ drop n s = s.

Admitted.

Exercise 5.

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

Admitted.

Admitted.

Exercise 6.

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

Admitted.

Admitted.

Exercise 7.

Lemma succ_min_distr' n m : (minn n m) + m <= 2 * (maxn n m).

Admitted.

Admitted.

Exercise 8.

Theorem plus_inj : forall n m,

n + n = m + m ->

n = m.

Proof.

Admitted.

n + n = m + m ->

n = m.

Proof.

Admitted.