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.

Modeling.

Consider the following famous puzzle, taken from Raymond E. Smullyan's book, "What is the name of this book?".

Portia's suitor is asked to solve a following puzzle to prove his worth. Her portrait is placed in one of three sealed caskets, gold, silver, and lead. Each casket has an inscription, but only one of the three inscriptions is true. The inscriptions read as follows:

Gold : "The portrait is in this casket" Silver : "The portrait is not in this casket" Lead : "The portrait is not in the gold casket"

Your task is to formalize the puzzle in Coq and prove the answer correct. hints: You can use a Variable declaration to introduce unknown variables and assumptions local to a section.

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