Require Import List.
(* Exercise 1 *)
(* Use an inductive predicate to characterize lists with an even length.
(* Name this predicate even_len *)
(* insert your solution here. *)
Implicit Arguments even_len.
Lemma even_len_example :
forall a : nat, even_len (a::(2*a)::(3*a)::(4*a)::nil).
Admitted.
(* Exercise 2 *)
(* Define an inductive predicate named transp to express that a list l1
is the same as a list l2 where two consecutive elements have been
transposed.
- use one constructor to express that the first two elements of the
list have been transposed and the rest is the same for the two lists.
For instance (transp (1::3::2::4::nil) (3::1::2::4::nil)) should be
provable using this constructor.
- use one constructor to express that the two lists have the same first
element, but their tails exhibit a transposition.
For instance (transp (1::3::2::4::nil) (1::2::3::4::nil)) should have
a proof that starts by using this constructor.
This predicate should have three arguments: a type A and two lists of
type A. Make the type A an implicit argument using the command
"Implicit Arguments transp." *)
Lemma transp_ex : transp (1::3::2::4::nil) (1::2::3::4::nil).
Admitted.
(* Exercise 3 *)
(* Define an inductive relation named permutation that is satisfied by l1 l2 if
one of the following cases is satisfied:
1/ l1 and l2 are the same
2/ l1 is a transposition of l3 and l3 is a permutation of l2.
Again, this relation should be polymorphic, and you should add an
implicit argument declaration. *)
(* Exercise 4 *)
Lemma permutation_refl : forall (A : Type) (l1 : list A), permutation l1 l1.
Admitted.
Lemma permutation_transitive : forall (A : Type) (l1 l2 l3 : list A),
permutation l1 l2 -> permutation l2 l3 -> permutation l1 l3.
Admitted.
Lemma transp_sym : forall A (l1 l2:list A), transp l1 l2 -> transp l2 l1.
Admitted.
Lemma permutation_sym : forall (A : Type) (l1 l2 : list A), permutation l1 l2 -> permutation l2 l1.
Admitted.
Lemma permutation_C : forall A (a:A) l1 l2, permutation l1 l2 -> permutation (a::l1) (a::l2).
(* The following function definitions describe a sorting algorithm
(insertion sort) *)
Fixpoint insert x l :=
match l with
nil => x::nil
| y::tl => if leb x y then x::l else y::insert x tl
end.
Fixpoint sort l :=
match l with
nil => nil
| x::tl => insert x (sort tl)
end.
(* Now we wish to prove that sorting a list returns an output that
satisfies the permutation relation with the input. *)
Lemma insert_permutation : forall x l, permutation (insert x l) (x::l).
Admitted.
Lemma sort_permutation : forall l, permutation (sort l) l.
Admitted.
(* Now if you are courageous enough, you should describe what a sorted
list is (for instance using an inductive predicate) and show
that the output of sort is a sorted list. You will need concepts
introduced in lesson 7, though! *)