Library HW3

Homework Assignment 3
Interactive Computer Theorem Proving
CS294-9, Fall 2006
UC Berkeley

Submit your solution file for this assignment as an attachment by e-mail with the subject "ICTP HW3" by the start of class on September 21. You should write your solutions entirely on your own, which includes not consulting any solutions to these problems that may be posted on the web.

Template source file

Require Import List.
Here are some additional tactics beyond those listed at the start of HW2 that you may find useful for this assignment. As before, you are free to use any additional tactics if you like, and the Coq manual's tactic index may be helpful.

  • constructor: This proves a goal that is an application of an inductively-defined predicate if the goal matches the conclusion of one of the rules used to define the predicate. constructor won't work if the candidate rule involves one or more quantified variables whose values can't be determined just by looking at the form of the goal. To use such rule applications, try...
  • apply name with arg1 ... argN: A simpler form of apply appeared at the start of HW2. There it was mentioned as a tool for applying lemmas, but it works just as well with constructors of inductive predicates. Use this long form of apply when the constructor or lemma that you are applying has some quantified variables whose instantiations aren't clear from the form of your goal. The space-separated list of arguments should contain the right value for each of these variables, in the order that the variables are quantified in the lemma or constructor definition. The argument list should not contain entries for variables whose values are implied by the form of the goal. Alternatively, you can use the form apply (name arg1 ... argN), where you treat the lemma or constructor like a function (which it is!) and specify the arguments to pass to it. You often need to specify more arguments explicitly with this version, since it can't take advantage of argument values that are apparent from the goal.
  • inversion H: Where H is a hypothesis stating an instance of an inductively-defined predicate, this tactic considers the ways that instance may have been derived and adds a subgoal for each case. inversion differs from simple destruct and induction in an important way: the latter two ignore the structure of the arguments to the predicate, while inversion takes them into account by adding new assumptions of equalities between the formal arguments (i.e., those that appear in the predicate's definition) and the actual arguments (i.e., those that appear in H). After a few inversions, these equality assumptions can come to dominate the context, and so it's usually a good idea to chain subst after inversion with a semicolon, so that every equality with a variable on its lefthand or righthand side is eliminated.


Your main new tools for this assignment are inductively-defined predicates and proofs by induction over their derivations.

Last elements of lists


Section last.
The definitions and theorems for this part are relative to an arbitrary set A, where we'll consider lists whose elements are of type A. The type list from the List library is a polymorphic list type, where list A denotes lists with elements of type A. You can write lists as either nil, the empty list; or h :: t, to denote the list obtained by concatenating element h to the front of list t. Lists are just another inductive type, though the parameterization on a type is different from what we've looked at in detail before. In particular, the same techniques for writing recursive functions and inductive proofs apply for lists as for inductive types in general.
   Variable A : Set.
Replace this parameter with a real definition of last as an inductively-defined predicate denoting that its first argument is the last element of its second argument. Your definition should be made with the Inductive command.
  Parameter last : A -> list A -> Prop.
Replace this parameter with a real definition of last_f as a recursive function that, for input list ls, returns Some x, if ls is non-empty and x is its last element; or None, if ls is empty. Your definition should be made with the Fixpoint command.
  Parameter last_f : list A -> option A.
Prove these two theorems showing that your two definitions agree with each other.
  Theorem lasts_agree1 : forall a ls,
    last a ls -> last_f ls = Some a.
  Admitted.

  Theorem lasts_agree2 : forall a ls,
    last_f ls = Some a -> last a ls.
  Admitted.
End last.

Permutations


Section permutation.
   Variable A : Set.
Using an inductive predicate, define what it means for one list to be a transposition of another; that is, the second list differs from the first by swapping the order of two consecutive elements. One consequence of this definition is that neither argument for an instance of transpose can ever have fewer than two elements, since you need at least two elements to have a consecutive pair to swap!
  Parameter transpose : list A -> list A -> Prop.
Using an inductive predicate, define what it means for one list to be a permutation of another; that is, the second list differs from the first by a finite number of transpositions.

Many equivalent definitions are possible here, but yours should be a literal transcription of the transposition-based definition from the previous paragraph. In particular, don't add extra constructors like a transitivity rule just to make the following theorems easier to prove.

  Parameter permutation : list A -> list A -> Prop.
Prove that permutation is an equivalence relation by showing that it satisfies the three relevant properties.

  Theorem permutation_reflexive : forall ls,
    permutation ls ls.
  Admitted.

  Theorem permutation_symmetric : forall ls1 ls2,
    permutation ls1 ls2
    -> permutation ls2 ls1.
  Admitted.

  Theorem permutation_transitive : forall ls1 ls2 ls3,
    permutation ls1 ls2
    -> permutation ls2 ls3
    -> permutation ls1 ls3.
  Admitted.
End permutation.
Index
This page has been generated by coqdoc