Require Import List.
Import ListNotations.
Require Import PeanoNat.
Import Nat.

(*
Question 1:

a) Define a recursive function replace so that replace n m l replaces every occurrence of the 
natural number n by the number m in the list l.
Example: 
Eval compute in replace 2 3 [1;2;3;2;1].
yields [1; 3; 3; 3; 1].
Hint: 
- Use x =? y two compare two natural numbers (returns bool).
*)

(*
b) Prove the lemma below. 
Hints:
- Use induction on l.
- Use the tactic contradiction if your assumptions are contradictory.
- 
*)

Lemma L1 : forall (n m : nat) (l : list nat), In n (replace n m l) -> m=n.

(*
c) Prove the lemma below. 
Hints:
- Use induction on l.
- You might find the lemmas useful:
   + eqb_eq : forall n m : nat, (n =? m) = true <-> n = m
   + eqb_neq : forall x y : nat, (x =? y) = false <-> x <> y
   + f_equal : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y
*)

Definition Injective {A B :Type} (f : A -> B) : Prop := forall (x y : A),  x <> y -> f x <> f y .

Lemma L2 :  forall (f : nat -> nat) (n m : nat) (l : list nat), Injective f -> map f (replace n m l) = replace (f n) (f m) (map f l).

(*
Question 2:

a) Define the data type tree A of binary trees that store elements of an arbitrary type A in the
leaves and in the inner nodes. An example of a tree of type tree nat is visualized below. Note 
that this is not the actual implementation, of course.
           2
         /   \
        3    1
       /  \
      1   4
*) 

(*
b) Implement a recursive function mapTree that applies a function f : A -> B to all elements in a 
tree of type tree A returning a tree of type tree B.
Example: map S "tree from a)" yields the tree
           3
         /   \
        4    2
       /  \
      2   5
*)

(*
c) Implement a recursive function collapse that collects all elements in a tree of type tree A in a 
list of type list A. Collect the elements in a infix manner, i.e., first the elements of the left subtree,
then the element at the current node followed by the elements in the right subtree.
Example: collapse "tree from a)" yields [1;3;4;2;1].
Hint: Use the append function ++.
*)

(*
d) Prove the lemma below.
Hints:
- Use induction on the tree t.
- You might find the lemma 
      map_app : forall (A B : Type) (f : A -> B) (l l' : list A), map f (l ++ l') = map f l ++ map f l' 
  useful.
*)

Lemma L3 {A B : Type} : forall (f : A -> B) (t : tree A), collapse (mapTree f t) = map f (collapse t).