(** 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.