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

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.

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

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

Exercise 3.

Theorem last_last {T : Type} : forall (x : T) s1 s2,
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.

Exercise 5.

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

Exercise 6.

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

Exercise 7.

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

Exercise 8.

Theorem plus_inj : forall n m,
n + n = m + m ->
n = m.
Proof.
Admitted.