(*
Przykładowy dowód w Coqu
autor: Tomasz Drab (tomasz.drab@cs.uni.wroc.pl)
data: 3 kwietnia 2019 r.
licencja: CC-BY
*)

Require Import Coq.Lists.List.
Infix "::" := cons.
Infix "++" := app.

Fail Check tree_ind.

(* drzewo o elementach typu A *)
Inductive tree (A:Type) : Type :=
| leaf : tree A
| node : A -> (tree A -> (tree A -> tree A)).

Arguments leaf {A}.
Arguments node {A} v l r.

Check tree_ind.

(* spłaszczenie drzewa *)
Fixpoint flat_app {A:Type} (t: tree A) (xs: list A) : list A :=
  match t with
  | (leaf)       => xs
  | (node v l r) => (flat_app l (cons v (flat_app r xs)))
  end.

Definition flatten {A:Type} (t: tree A) : list A := flat_app t nil.

(* map dla drzew *)
Fixpoint tree_map {A B:Type} (f: A -> B) (t: tree A) : tree B :=
  match t with
  | (leaf)       => (leaf)
  | (node v l r) => (node (f v) (tree_map f l) (tree_map f r))
  end.

(* lemat *)
Theorem flat_app_lemma {A: Type} : forall (t: tree A) (xs: list A),
  (flat_app t xs) = (app (flatten t) xs).
Proof.
  induction t as [|v l Pl r Pr].
  + reflexivity.
  + intros xs.
    unfold flatten.
    simpl.
    rewrite Pl.
    rewrite Pl.
    rewrite Pr.
    rewrite Pr.
    Check app_nil_r.
    rewrite app_nil_r.
    rewrite app_comm_cons.
    rewrite app_assoc.
    reflexivity.
Qed.

(* główne twierdzenie *)
Theorem map_flatten {A B:Type} :
  forall (f: A -> B) (t: tree A),
  (map f (flatten t)) = (flatten (tree_map f t)).
Proof.
  intros f.
  induction t as [|v l Pl r Pr].
  + replace (flatten leaf)    with (@nil A)  by auto.
    replace (map f nil)       with (@nil B)  by auto.
    replace (tree_map f leaf) with (@leaf B) by auto.
    replace (flatten leaf)    with (@nil B)  by auto.
    reflexivity.
  + unfold flatten.
    replace (flat_app (node v l r) nil) with
      (flat_app l (cons v (flat_app r nil))) by auto.
    replace (tree_map f (node v l r)) with
      (node (f v) (tree_map f l) (tree_map f r)) by auto.
    simpl.
    rewrite flat_app_lemma.
    rewrite flat_app_lemma.
    rewrite flat_app_lemma.
    rewrite flat_app_lemma.
    rewrite app_nil_r.
    rewrite app_nil_r.
    Check map_app.
    rewrite map_app.
    rewrite Pl.
    replace (map f (v :: flatten r)) with
      ((f v) :: map f (flatten r)) by auto.
    rewrite Pr.
    reflexivity.
Qed.