Library mathcomp_eulerian.mmtree

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section MMTree.

Inductive mmtree (T : Type) : Type :=
  | Leaf : mmtree T
  | Node : mmtree T → T → mmtree T → mmtree T.

Arguments Leaf {T}.
Arguments Node {T} _ _ _.

Fixpoint mmtree_to_seq {T : Type} (t : mmtree T) : seq T :=
  match t with
  | Leaf ⇒ [::]
  | Node l x r ⇒ mmtree_to_seq l ++ x :: mmtree_to_seq r
  end.

Definition min_pos (s : seq nat) : nat :=
  index (foldr minn (head 0 s) (behead s)) s.

Lemma min_in s a : foldr minn a s \in a :: s.
Proof.
elim: s a ⇒ [| b s IH] a /=.
  by rewrite inE eqxx.
rewrite !inE.
case: leqP ⇒ _; first by rewrite eqxx orbT.
have := IH a; rewrite inE ⇒ /orP [->|->] //; by rewrite !orbT.
Qed.

Lemma min_pos_lt s : s ≠ [::] → min_pos s < size s.
Proof.
case: s ⇒ [// | a s _]; rewrite /min_pos.
have → : head 0 (a :: s) = a by [].
have → : behead (a :: s) = s by [].
by rewrite index_mem; exact: min_in.
Qed.

Fixpoint mmtree_of_seq_fuel (fuel : nat) (s : seq nat) : mmtree nat :=
  match fuel with
  | 0 ⇒ Leaf
  | fuel'.+1 ⇒
      match s with
      | [::] ⇒ Leaf
      | _ :: _ ⇒
          let j := min_pos s in
          Node (mmtree_of_seq_fuel fuel' (take j s))
               (nth 0 s j)
               (mmtree_of_seq_fuel fuel' (drop j.+1 s))
      end
  end.

Definition mmtree_of_seq (s : seq nat) : mmtree nat :=
  mmtree_of_seq_fuel (size s) s.


Lemma mmtree_of_seq_fuel_correct :
  ∀ fuel s, size s ≤ fuel →
    mmtree_to_seq (mmtree_of_seq_fuel fuel s) = s.
Proof.
elim ⇒ [| fuel IH] s.
  by rewrite leqn0 ⇒ /nilP →.
case: s ⇒ [// | a s Hsz] /=.
set s0 := a :: s in Hsz ×.
have Hs0 : s0 ≠ [::] by [].
have Hj : min_pos s0 < size s0 by apply: min_pos_lt.
have Hleft : size (take (min_pos s0) s0) ≤ fuel.
  rewrite size_take Hj.
  by rewrite -ltnS; apply: (leq_trans Hj).
have Hright : size (drop (min_pos s0).+1 s0) ≤ fuel.
  rewrite size_drop.
  have : size s0 ≤ fuel.+1 by [].
  move: Hj; case: (size s0) ⇒ // k Hk Hk1.
  by rewrite subSS; apply: (leq_trans (leq_subr _ _)).
rewrite (IH _ Hleft) (IH _ Hright).
rewrite -[RHS](cat_take_drop (min_pos s0) s0).
congr (_ ++ _).
by rewrite (drop_nth 0 Hj).
Qed.

Theorem mmtree_of_seqK : ∀ s, mmtree_to_seq (mmtree_of_seq s) = s.
Proof.
move⇒ s; rewrite /mmtree_of_seq; apply: mmtree_of_seq_fuel_correct.
exact: leqnn.
Qed.


Definition ex_seq := [:: 3; 1; 4; 1; 5; 9; 2; 6].

Example ex_nontrivial :
  match mmtree_of_seq ex_seq with
  | Leaf ⇒ false
  | Node Leaf _ _ ⇒ false
  | Node _ _ Leaf ⇒ false
  | _ ⇒ true
  end = true.
Proof. by []. Qed.

Example ex_roundtrip :
  mmtree_to_seq (mmtree_of_seq ex_seq) = ex_seq.
Proof. exact: mmtree_of_seqK. Qed.

Example ex_roundtrip_compute :
  (mmtree_to_seq (mmtree_of_seq ex_seq) == ex_seq) = true.
Proof. by []. Qed.

End MMTree.