Skip to content

Instantly share code, notes, and snippets.

@bivoje
Last active June 28, 2019 03:23
Show Gist options
  • Save bivoje/5dcfdcef9cb8d1f833884ddba0e46582 to your computer and use it in GitHub Desktop.
Save bivoje/5dcfdcef9cb8d1f833884ddba0e46582 to your computer and use it in GitHub Desktop.
proofs on restoration of some binary tree traverse
(*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.*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment