# Problem Set 2 : Induction and Equality

## Induction.

Next, we're going to exercise the simpl, induction and rewrite tactics. Replace the Admitted.'s with an appropriate proof. Don't forget to write Qed. to terminate your proofs. It goes without saying that you shouldn't just prove these by using a library lemma :-) However, if you get stuck proving one of these, then it is sometimes useful to look for one that does solve this, using the top-level SearchAbout command, and then Print the corresponding proof.
Module PSET2_EX1.

Require Import List.

Lemma zero_plus_x : forall n, 0 + n = n.

Proof.

Admitted.

Lemma x_plus_zero : forall n, n + 0 = n.

Proof.

Admitted.

Lemma map_map : forall {A B C:Type} (f:A->B) (g:B -> C) (xs:list A),

map g (map f xs) = map (fun x => g (f x)) xs.

Proof.

Admitted.

Lemma app_assoc : forall {A:Type} (xs ys zs:list A),

xs ++ (ys ++ zs) = (xs ++ ys) ++ zs.

Proof.

Admitted.

Lemma map_is_fold : forall {A B} (f:A->B) (xs:list A),

map f xs = fold_right (fun x y => (f x)::y) nil xs.

Proof.

Admitted.

Definition list_sum (xs:list nat) : nat := fold_right plus 0 xs.

Lemma list_sum_app : forall (t1 t2: list nat),

list_sum (t1 ++ t2) = list_sum t1 + list_sum t2.

Proof.

Admitted.

Inductive tree(A:Type) : Type :=

| Leaf : tree A

| Node : tree A -> A -> tree A -> tree A.

Implicit Arguments Leaf [A].

Implicit Arguments Node [A].

Fixpoint mirror{A:Type} (t:tree A) : tree A :=

match t with

| Leaf => Leaf

| Node lft v rgt => Node (mirror rgt) v (mirror lft)

end.

Lemma mirror_mirror : forall A (t:tree A), mirror (mirror t) = t.

Proof.

Admitted.

Fixpoint flatten {A:Type} (t:tree A) : list A :=

match t with

| Leaf => nil

| Node lft v rgt => (flatten lft) ++ v::(flatten rgt)

end.

Fixpoint tree_sum (t:tree nat) : nat :=

match t with

| Leaf => 0

| Node lft v rgt => (tree_sum lft) + v + (tree_sum rgt)

end.

Lemma tree_flatten_sum : forall t, tree_sum t = list_sum (flatten t).

Proof.

Admitted.

End PSET2_EX1.

Module PSET2_EX2.

Require Import List.

Lemma zero_plus_x : forall n, 0 + n = n.

Proof.

Admitted.

Lemma x_plus_zero : forall n, n + 0 = n.

Proof.

Admitted.

Lemma map_map : forall {A B C:Type} (f:A->B) (g:B -> C) (xs:list A),

map g (map f xs) = map (fun x => g (f x)) xs.

Proof.

Admitted.

Lemma app_assoc : forall {A:Type} (xs ys zs:list A),

xs ++ (ys ++ zs) = (xs ++ ys) ++ zs.

Proof.

Admitted.

Lemma map_is_fold : forall {A B} (f:A->B) (xs:list A),

map f xs = fold_right (fun x y => (f x)::y) nil xs.

Proof.

Admitted.

Definition list_sum (xs:list nat) : nat := fold_right plus 0 xs.

Lemma list_sum_app : forall (t1 t2: list nat),

list_sum (t1 ++ t2) = list_sum t1 + list_sum t2.

Proof.

Admitted.

Inductive tree(A:Type) : Type :=

| Leaf : tree A

| Node : tree A -> A -> tree A -> tree A.

Implicit Arguments Leaf [A].

Implicit Arguments Node [A].

Fixpoint mirror{A:Type} (t:tree A) : tree A :=

match t with

| Leaf => Leaf

| Node lft v rgt => Node (mirror rgt) v (mirror lft)

end.

Lemma mirror_mirror : forall A (t:tree A), mirror (mirror t) = t.

Proof.

Admitted.

Fixpoint flatten {A:Type} (t:tree A) : list A :=

match t with

| Leaf => nil

| Node lft v rgt => (flatten lft) ++ v::(flatten rgt)

end.

Fixpoint tree_sum (t:tree nat) : nat :=

match t with

| Leaf => 0

| Node lft v rgt => (tree_sum lft) + v + (tree_sum rgt)

end.

Lemma tree_flatten_sum : forall t, tree_sum t = list_sum (flatten t).

Proof.

Admitted.

End PSET2_EX1.

Module PSET2_EX2.

## Modeling.

Section SmullyanPuzzle.

Sections are a convenient way to develop theories that are universally quantified
over some variables.

Inductive chest : Type :=

| Silver

| Gold

| Lead.

Unlike an axiom, Variables are just universally quantified
in the items in this section below that mention them.
See the output of Check ItsSilver after the section is closed.

Variable location : chest.

a. Replace this variable with a Definition.

Variable inChest: chest -> Prop.

b. Give a definition for the inscriptions on the chests.
c. Capture the assumption that only one chest is truthful.

Theorem ItsSilver : inChest Silver.

Admitted.

d. Finish this proof.

Check ItsSilver.

End SmullyanPuzzle.

When we end a section, Coq adds universal
quantifiers to ensure that everything is closed.

Check ItsSilver.

This page has been generated by coqdoc