proofs on restoration of some binary tree traverse

bintree_traverse.v

(*doc generation command
  coqtop -compile infix.v -o infix.vo && # compile
  coqdoc infix.v --no-index &&           # coqdoc
  sed -i -e 's/monospace/"Ubuntu Mono"/g' coqdoc.css &&    # use UbuntuMono instread of default monospace typeface. it will be used for code section.
  sed -i -e 's/>\( \+\)</><pre>\1<\/pre></g' infix.html && # make spaces visible (especially in code) to preserve aligning.
  echo "pre { font-family: "Ubuntu Mono"; display: inline; margin: 0; }" >> coqdoc.css # style for 'pre' making above line work.
*)

(** * Predefinition *)

(** Assuming only binary operators allowed, AST of mathematical
    expression is a full-binary-Tree. A denotes the type of labels
    for operators and operands. e.g. for labels like ["24" "+"
    "356"].., A is string. You could use different types for
    operators and operands ...only to burden following proof works. *)
Inductive Tree {A} : Type :=
  | Leaf : A -> Tree
  | Node : A -> Tree -> Tree -> Tree.

(* prevent implicit parameter for Tree.
   while leaving Leaf and Node to accept implicit. *)
Arguments Tree (A) : clear implicits.

(** This is sample tree that we will use to test algorithms before
    actually writing proof for them. We use A := nat to denote labels.
    For instance situation, imagine you have 1-based array of string tokens
    << ["4"; "5"; "3"; "x"; "-"; "2"; "+"] >> .
    Then tree_eg denote mathematical expression [(4 - 5 x 3) + 6],
    with more or less parenthesis. *)
Definition tree_eg : Tree nat :=
  Node 7
    (Node 5
      (Leaf 1)
      (Node 4
        (Leaf 2)
        (Leaf 3)))
    (Leaf 6).

(** We are going to study on 3 type of binary tree sequentialization,
    namely, prefix, infix and postfix, and on restoring AST from each.
    Each elements of sequence should better be distinguishable whether
    it had been leaf or node to accomplish 2nd goal. [Report] type
    wraps elements from a tree (reporting each tree elements), so that
    we can put them in sequence ([Reports]). Again, you could choose
    differenct types for labeling nodes and leaf, but we didn't. *)
(* FIXME doesn't coq have [Either]? *)
Variant Report {A} : Type :=
  | Node' : A -> Report
  | Leaf' : A -> Report.
Arguments Report (A) : clear implicits.

Definition Reports A := list (Report A).

Require Import List.
Import ListNotations.

(* ======================================================================= *)
(** * Sequentializers *)
(** notes on lexicon. {post, in, pre}-order refers traverse methods, each
    will generate respective sequentialization, namely,
    {post, in, pre}-fix notations *)

(* ----------------------------------------------------------------------- *)
(** ** IN-ORDER sequentilizer *)
(** It is good idea to start with the most familiar one among the 3,
    infix notation. We use it everyday to write down mathematical
    expression.*)

Fixpoint in_order {A} t : @Reports A :=
  match t with
  | Leaf x => [Leaf' x]
  | Node x tl tr => in_order tl ++ [Node' x] ++ in_order tr
  end.

Example inoder_eg : in_order tree_eg =
  [Leaf' 1; Node' 5; Leaf' 2; Node' 4; Leaf' 3; Node' 7; Leaf' 6].
  auto. Qed.
  
(* ----------------------------------------------------------------------- *)
(** ** PRE-ORDER sequentilizer *)
(** Lisp, like other functional languages, uses prefix notation on writing
    expressions, mathematical expressions as well. e.g. you write
    [+ ( * 3 4) ( - 5 2)] instead of [(3*4) + (5-2)] in Lisp. *)

Fixpoint pre_order {A} (t : Tree A) : Reports A :=
  match t with
  | Leaf x => [Leaf' x]
  | Node x tl tr => Node' x :: pre_order tl ++ pre_order tr
  end.

Example pre_order_eg : pre_order tree_eg =
  [Node' 7; Node' 5; Leaf' 1; Node' 4; Leaf' 2; Leaf' 3; Leaf' 6].
  auto. Qed.

(** While Lisp is notorious for being awash with parentheses, we didn't
    insert single parenthesis in our prefix notation. Even so, the
    representation is left unambigous. [+ * 3 4 - 5 2] can be only parsed
    as previous form. Trying to parsing into another AST structure would
    result in operators ([+], [*] ..) being in leaf, which is nonsense.
    The reason Lisp requires parenthesis is because it allows operators
    to be in leaf. In other words, Lisp allows operators to be passed as
    arguments to another function (higher order function). Since Lisp
    interpretes operators as normal function named with symbol charaters,
    [(+ * 3)] (adding [*] and [3]) is not _syntactically_ wrong but only
    _semantically_ absurd. This leaves alternative AST's valid, so that
    we can't ignore those possibilities.
    This is why we need to wrap labels in [Report] type. It enables us
    to distinguish which are operators (can not be argumented) and thus
    choose unique AST. *)

(* ----------------------------------------------------------------------- *)
(** ** POST-ORDER sequentilizer *)
(** Postfix notation is similar to Prefix but operators follows their
    operands. e.g. [3*4 + 4*5] => [((3 4 * ) (4 5 * ) +)]. Postfix notations
    are often found in stack-based languages, like 'golf script'.
    see https://esolangs.org/wiki/Category:Stack-based. *)

Fixpoint post_order {A} t : Reports A :=
  match t with
  | Leaf x => [Leaf' x]
  | Node x tl tr => post_order tl ++ post_order tr ++ [Node' x]
  end.

Example post_order_eg : post_order tree_eg =
  [Leaf' 1; Leaf' 2; Leaf' 3; Node' 4; Node' 5; Leaf' 6; Node' 7].
  auto. Qed.

(** Actually, prefix and postfix are interconvertible.
    see preorder restoration for the argument. *)

(* ======================================================================= *)
(** * Restoration *)
(** reverse of traversing. restoring binary tree from sequentialized
    sequence is not a simple task, espetially in coq. For e.g. following
    haskell implementation for Restoration from pre_order sequence,
    [[
      order_pre' :: [Report a] -> Maybe (Tree a, [Report a])
      order_pre' [] = Nothing
      order_pre' (Left x : rest) = Just (Leaf x, rest)
      order_pre' (Right x : rest0) = do
        (tl, rest1) <- order_pre' rest0
        (tr, rest2) <- order_pre' rest1
        Just (Node x tl tr, rest2)
    ]]
    cannot be directly translated into coq, due to coq's limitation on
    decreasing argument of fixpoint definitions. With this in mind,
    read through the next. *)

(* ----------------------------------------------------------------------- *)
(** ** POST-ORDER restoration *)
(** The easiest one to implement in coq is pos-order. Definition of
   [order_post'] written below is alike golf script interpreter. It uses
   stack to save calculated, but not yet used values. Also note that
   [order_pose'] is iterative process rather than recursive process.
   see SICP 1.2.1 for more information. *)

Fixpoint order_post' {A} stack rps : option (Tree A) :=
  match rps with
  | [] => match stack with | [T] => Some T | _ => None end
  | Leaf' x :: rest => order_post' (Leaf x :: stack) rest
  | Node' x :: rest => match stack with
    | a :: b :: stack' => order_post' (Node x b a :: stack') rest
    | _ => None
    end
  end.

Definition order_post {A} := @order_post' A [].

Example order_post_eg : order_post (post_order tree_eg) = Some tree_eg.
  auto. Qed.

(** Now that we have claimed [order_post] as inverse of [post_order],
    it's time to actually proove it. *)

Lemma order_post_advance {A} : forall (t : Tree A) stack rps,
  order_post' stack (post_order t ++ rps)
  = order_post' (t :: stack) rps.
Proof.
  intro t. induction t. reflexivity.
  intros stack rps. simpl. do 2 rewrite <- app_assoc.
  rewrite IHt1. rewrite IHt2. simpl. reflexivity.
Qed.

Theorem post_rev {A} : forall t : Tree A,
  order_post (post_order t) = Some t.
Proof.
  intro t. induction t. reflexivity.
  unfold order_post. simpl.
  do 2 rewrite order_post_advance.
  simpl. reflexivity.
Qed.

(* ----------------------------------------------------------------------- *)
(** ** PRE-ORDER restoration *)
(** As noted above, postfix and infixnotations are interconvertible. So here,
    we exploit such property to implement [order_pre] rather than writing
    another stack algorithm.
    First, observe that [rev] of pre_order is postfix notation of a tree
    that is mirrored (a tree whose left and right children are swapped).
*)
Eval compute in (order_post (rev (pre_order tree_eg)), Some tree_eg).

(** We need to write mirror function to correct it *)

Fixpoint mirror_tree {A} (t : Tree A) : Tree A :=
  match t with
  | Leaf x => Leaf x
  | Node x tl tr => Node x (mirror_tree tr) (mirror_tree tl)

  end.

(** Verifying interconvertibility of prefix and postfix. *)

Lemma mirror_tree_inv {A} : forall t : Tree A,
  mirror_tree (mirror_tree t) = t.
Proof.
  intro t. induction t; try reflexivity.
  simpl. rewrite IHt1, IHt2. reflexivity.
Qed.

Theorem post_pre_rel {A} : forall t : Tree A,
  post_order (mirror_tree t) = rev (pre_order t).
Proof.
  intro t. induction t; try reflexivity.
  simpl. rewrite rev_app_distr. rewrite IHt1, IHt2.
  rewrite app_assoc. reflexivity.
Qed.

(** One can do the same in reversed relation since both [rev] and
   [mirror_tree] are involutive. Consequently, we have following
   definition *)

Definition order_pre {A} (rps : Reports A) : option (Tree A) :=
  option_map mirror_tree (order_post (rev rps)).

Example order_pre_eg : order_pre (pre_order tree_eg) = Some tree_eg.
  auto. Qed.

(** .. and its proof. *)

Theorem pre_rev {A} : forall t : Tree A,
  order_pre (pre_order t) = Some t.
Proof.
  intro t. unfold order_pre. rewrite <- post_pre_rel.
  rewrite post_rev. simpl. rewrite mirror_tree_inv.
  reflexivity.
Qed.


(* ----------------------------------------------------------------------- *)
(** ** IN-ORDER restoration1 *)
(** Unfotunately, it's impossible to define inverse of [in_order] as we
    did with [post_order] since [in_order] itself is not injective. *)

Example inorder_ambiguous :
  in_order (Node 1 (Node 2 (Leaf 3) (Leaf 4)) (Leaf 5)) =
  in_order (Node 2 (Leaf 3) (Node 1 (Leaf 4) (Leaf 5))).
  auto. Qed.

(** We need more sophisticated sequence notation to remove ambiguity in
    infix representation. *)
Variant Report_ {A} : Type :=
  | Leaf_ : A -> Report_
  | Node_ : A -> Report_
  | Open_ : Report_
  | Clos_ : Report_.
Arguments Report_ (A) : clear implicits.

Definition Reports_ A := list (Report_ A).

(** [Report_] is extension of [Report] where [Open_] and [Clos_] denote
    open and closed parenthesis respectively. Then we modify
    [in_order] to insert parenthesis in sequence rigorously. *)

(* wraps every operator execution with parenthesis.
   no ternary (or more) terms. (no binary terms)
   adds 2 adiditional outermost parenthesis.
   resulting seq is unambigous without precedence. *)
Fixpoint in_order1 {A} (t : Tree A) : Reports_ A :=
  match t with
  | Leaf x => [Leaf_ x]
  | Node x tl tr => [Open_] ++ in_order1 tl ++ [Node_ x] ++ in_order1 tr ++ [Clos_]
  end.

Example in_order1_eg : in_order1 tree_eg =
  [Open_; Open_; Leaf_ 1; Node_ 5; Open_; Leaf_ 2; Node_ 4; Leaf_ 3; Clos_; Clos_; Node_ 7; Leaf_ 6; Clos_].
  auto. Qed. (* ((1 <5> (2 <4> 3)) <7> 6) *)

(** Now, restoring the sequence is not that hard. It is assured that
    only 3 components (composite or not) present between open and
    closed parenthesis. As before, we use stack and iterative approach
    to solve restoration problem. There are 2 subject to concern.

    - For sub-expression nested by pair of parentheses, we need no just
    simple stack, but stack of stacks where each stack refers to
    each sub-expression. e.g. when iteration reaches at caret,
    [[
      ((1 <5> (2 <4> 3)) <7> 6)
                  ^
      stacks := [ [1; <5>]; [2; <4>] ]
    ]]
    To lessen the hassle, we use flat stack of [option]s and use
    [None] delimit substacks. e.g.
    [[
      stack := [Some 1; Some <5>, None, Some 2; Some <4>]
    ]]

    - We need to keep [Node]s without a [Leaf] in the stack. Which
    means our stack should contain partial [Tree]s. Rather than
    defining another inductive type that can contain partial tree
    we chose to recycle [Tree] type, using [Leaf] constructor for
    both leaves and partial nodes. It is possible because we used
    same label type for them and ruthless parenthesis insetion of
    [in_order1] eliminate ambiguity. (We can always determine that
    the one in the middle among 3 in substack is the Leaf). *)
(* FIXME can't we omit None? *)
Fixpoint order_in1' {A} stack rps : option (Tree A) :=
  let push st r t := order_in1' (Some t :: st) r in
  match rps with
  | [] => match stack with | [Some T] => Some T | _ => None end
  | Open_   :: rest => order_in1' (None :: stack) rest
  | Leaf_ x :: rest => push stack rest (Leaf x)
  | Node_ x :: rest => push stack rest (Leaf x)
  | Clos_   :: rest => match stack with
    | Some tr :: Some (Leaf x) :: Some tl :: None :: stack'
        => push stack' rest (Node x tl tr)
    | _ => None
    end
  end.

Definition order_in1 {A} := @order_in1' A [].

Example order_in1_eg : order_in1 (in_order1 tree_eg) = Some tree_eg.
  auto. Qed.

(** Proving validity of inverse in similar scheme as [post_rev]. *)

Lemma order_in1_advance : forall A (t : Tree A) stack rps,
  order_in1' stack (in_order1 t ++ rps)
  = order_in1' (Some t :: stack) rps.
Proof.
  intros A t. induction t. reflexivity.
  intros stack rps. simpl.
  rewrite <- app_assoc. rewrite IHt1. simpl.
  rewrite <- app_assoc. rewrite IHt2. simpl.
  reflexivity.
Qed.

Theorem in1_rev {A} : forall t : Tree A,
  order_in1 (in_order1 t) = Some t.
Proof.
  intro t. induction t. reflexivity.
  unfold order_in1. simpl.
  rewrite order_in1_advance. simpl.
  rewrite order_in1_advance. simpl.
  reflexivity.
Qed.

(* ----------------------------------------------------------------------- *)
(** ** IN-ORDER restoration2 *)
(** Sequence produced by [in_order1] is quite verbose. We don't usually
    write [((1*(2^3))+6)], but simply, [1*2^3+6]. Dropping parentheses
    did not accompany ambiguity thanks to precedence of operators.
    This approach is implemented in [in_order2] with precedence
    function [prec]. *)

Require Import Nat. (* for [<?] operator *)
Require Import Basics. (* for [∘] operator *)
Open Scope program_scope.

(* adds minimal parenthesis that makes it unambigous with
   precedence. TODO proof? *)
Fixpoint in_order2 {A} (prec' : A -> nat) (t : Tree A) : Reports_ A :=
  let prec := S ∘ prec' in
  let wrap x t' := let rps := in_order2 prec t' in
    match t' with
    | Leaf _ => rps
    | Node x' _ _ => if prec x <? prec x' then rps
                     else [Open_] ++ rps ++ [Clos_]
    end
  in match t with
  | Leaf x => [Leaf_ x]
  | Node x tl tr => wrap x tl ++ [Node_ x] ++ wrap x tr
  end.

Example in_order2_eg1 : in_order2 id tree_eg =
  [Open_; Leaf_ 1; Node_ 5; Open_; Leaf_ 2; Node_ 4; Leaf_ 3; Clos_; Clos_; Node_ 7; Leaf_ 6] .
  auto. Qed. (* (1 <5> (2 <4> 3)) <7> 6 *)

Definition tree_eg2 : Tree nat :=
  Node 2
    (Node 5
      (Leaf 1)
      (Node 5
        (Leaf 7)
        (Leaf 3)))
    (Node 1
      (Leaf 6)
      (Leaf 2)).

(* note that we insert prarenthesis when precedences are equal *)
Example in_order2_eg2 : in_order2 id tree_eg2 =
  [Leaf_ 1; Node_ 5; Open_; Leaf_ 7; Node_ 5; Leaf_ 3; Clos_; Node_ 2; Open_; Leaf_ 6; Node_ 1; Leaf_ 2; Clos_].
  auto. Qed. (* 1 <5> (7 <5> 3) <2> (6 <1> 2) *)

(* analogous to haskell's [span] but always breaks at None and returns reversed *)
Fixpoint span_op' {A} (f : A -> bool) (l : list (option A)) ret : list A * list (option A) :=
  match l with
  | [] => (ret, [])
  | None :: tl => (ret, l)
  | Some x :: tl => if f x then span_op' f tl (x::ret) else (ret,l)
  end.

Definition span_op {A} f l := @span_op' A f l [].

Example span_op_eg1 : let f := fun x => x <? 3 in
  span_op f [Some 1; Some 2; Some 3; Some 1] = ([2; 1], [Some 3; Some 1]).
  auto. Qed.

Example span_op_eg2 : let f := fun x => x <? 3 in
  span_op f [Some 1; None; Some 2; Some 3; Some 1] = ([1], [None; Some 2; Some 3; Some 1]).
  auto. Qed.

Definition flush {A} (prec' : A -> nat) (stack : list (option A)) n : list A * list (option A) :=
  let prec := S ∘ prec' in span_op (fun x => n <? prec x) stack.

(* inspirated by '혼자 연구하는 C/C++ 19-3-나' *)
Fixpoint in2_post' {A} (prec : A -> nat) (stack : list (option A)) (rps : Reports_ A) : Reports A :=
  match rps with
  | [] => let (ret,st') := flush prec stack 0 in map Node' ret (* st' == [] *)
  | Open_   :: rest => in2_post' prec (None :: stack) rest
  | Leaf_ x :: rest => Leaf' x :: in2_post' prec stack rest
  | Node_ x :: rest => let (pop,st') := flush prec stack (prec x)
                       in map Node' pop ++ in2_post' prec (Some x :: st') rest
  | Clos_   :: rest => match flush prec stack 0 with
                       | (pop, None::st') => map Node' pop ++ in2_post' prec st' rest
                       | _ => [] end (* not reached *)
  end.

Definition in2_post {A} prec := @in2_post' A prec [].

Example in2_post_eg1 : post_order tree_eg = in2_post id (in_order2 id tree_eg).
  auto. Qed.

Example in2_post_eg2 : post_order tree_eg2 = in2_post id (in_order2 id tree_eg2).
  auto. Qed.

Fixpoint squash {A} (nls : list A) (lst : list (Tree A)) {struct nls} : list (Tree A) :=
  match nls, lst with
  | [], _ => lst
  | n :: ls, tr :: tl :: lst => squash ls (Node n tl tr :: lst)
  | _, _ => [] (* not reached *)
  end.

Fixpoint order_in2' {A} prec (nst : list (option A)) (lst : list (Tree A)) rps {struct rps} : option (Tree A) :=
  match rps with
  | [] => let (pop,st') := flush prec nst 0 in hd_error (squash pop lst) (* st' == [], squash pop lst == singlton *)
  | Open_   :: rest => order_in2' prec (None :: nst) lst rest
  | Leaf_ x :: rest => order_in2' prec nst (Leaf x :: lst) rest
  | Node_ x :: rest => let (pop,st') := flush prec nst (prec x)
                       in order_in2' prec (Some x :: st') (squash pop lst) rest
  | Clos_   :: rest => match flush prec nst 0 with
                       | (pop, None::st') => order_in2' prec st' (squash pop lst) rest
                       | _ => None end
  end.

Definition order_in2 {A} prec := @order_in2' A prec [] [].

Example order_in2_eg1 : order_in2 id (in_order2 id tree_eg) = Some tree_eg.
  auto. Qed.

Example order_in2_eg2 : order_in2 id (in_order2 id tree_eg2) = Some tree_eg2.
  auto. Qed.

Lemma span_op'_advance1 {A} : forall p nst ret (x:A),
  p x = true -> span_op' p (Some x :: nst) ret = span_op' p nst (x::ret).
Proof. intros. simpl. rewrite H. auto. Qed.

Lemma span_op'_advance2 {A} : forall (p : A -> bool) nst ret,
  fst (span_op' p nst ret) = fst (span_op' p nst []) ++ ret.
Proof.
  intros. generalize nst, ret; clear nst ret.
  induction nst; intro ret; auto.
  simpl. destruct a; auto. case (p a); auto.
  rewrite IHnst, (IHnst [a]), <- app_assoc. auto.
Qed.

Corollary span_op'_advance {A} : forall p nst ret (x:A),
  p x = true ->
  fst (span_op' p (Some x :: nst) ret) = fst (span_op' p nst []) ++ x :: ret.
Proof. intros.
  rewrite span_op'_advance1; auto.
  rewrite span_op'_advance2; auto.
Qed.

Lemma flush_0 {A} : forall p nst (x:A),
  fst (flush p (Some x :: nst) 0) = fst (flush p nst 0) ++ [x].
Proof.
  intros. unfold flush, span_op.
  rewrite span_op'_advance; auto.
Qed.

Theorem in2_post_valid {A} : forall p (t : Tree A),
  in2_post p (in_order2 p t) = post_order t.
Proof.
  intros.
  induction t.
  simpl. auto.
  simpl.
Abort.

Inductive pathway {A} : Tree A -> Tree A -> list A -> Prop :=
  | capriole : forall t, pathway t t []
  | descend_l : forall t p c l x, pathway p c l -> pathway (Node x p t) c (x::l)
  | descend_r : forall t p c l x, pathway p c l -> pathway (Node x t p) c (x::l).

Example pathway_eg1 : pathway tree_eg (Leaf 6) [7].
Proof. apply descend_r. apply capriole. Qed.

Example pathway_eg2 : pathway tree_eg (Node 4 (Leaf 2) (Leaf 3)) [7; 5].
Proof. apply descend_l. apply descend_r. apply capriole. Qed.

Example pathway_eg3 : pathway tree_eg (Leaf 3) [7; 5; 4].
Proof. apply descend_l. apply descend_r. apply descend_r. apply capriole. Qed.

(* unable to finish the proof 
pathway ? ? lst

(* order_in2' {A} prec nst lst rps {struct rps} : option (Tree A) *)
 
order_in2'

Lemma order_in2_advance {A} : forall (t : Tree A) p nst lst rps,
  order_in2' p nst lst (Open_ :: in_order2 p t ++ [Clos_] ++ rps)
  = order_in2' p nst (t :: lst) rps.
Proof.
  intros t p. induction t. reflexivity.
  intros. destruct t1, t2.
  - auto.
  - remember (Node a1 t2_1 t2_2) as N. simpl. subst N.
    case ((S ∘ p) a <? (S ∘ p) a1).
    
    
  -
  simpl (in_order2 p (Node a (Leaf a0) (Leaf a1))).
  - simpl. 
  rewrite <- app_assoc. rewrite IHt1. simpl.
  rewrite <- app_assoc. rewrite IHt2. simpl.
  reflexivity.
Qed.

Lemma order_in1_advance : forall A (t : Tree A) stack rps,
  order_in1' stack (in_order1 t ++ rps)
  = order_in1' (Some t :: stack) rps.
Proof.
  intros A t. induction t. reflexivity.
  intros stack rps. simpl.
  rewrite <- app_assoc. rewrite IHt1. simpl.
  rewrite <- app_assoc. rewrite IHt2. simpl.
  reflexivity.
Qed.


Theorem in_rev {A} : forall p (t : Tree A), order_in2 p (in_order2 p t) = Some t.
Proof.
  intros. induction t; try reflexivity.
  simpl.

use Clear to redefine previous definition, instead of deleting it.*)