Library Combi.Combi.bintree: Binary Trees

Binary Trees

A binary tree is a rooted tree such that each node has two distiguished, children the left one and the right one. The main goal of this file is to construct the Tamari lattice which is the transitive closure of the directed graph of left rotation. We show that it is indeed a lattice.

Basic definitions:

bintree == the type of binary trees this is canonically a countType
BinLeaf == the leaf for binary trees
BinNode left right == the binary tree with subtrees left right

Binary trees of size n:

size_tree t == the number of node of the tree t
enum_bintreesz n == the list of a trees of size n
bintreesz n == the Sigma type for trees of size n. This is canonically a finType with enumeration enum_bintreesz n
Catalan_bin n == Catalan number defined using the binary tree recursion: C_0 = 1 and C_{n+1} = sum__(i+j = n) C_i C_j. We show that they count the number of binary trees of size n. The binomial formula will be proved using Dyck word.

Left branch surgery:

left_branch t == the sequence of the right subtrees of the nodes starting for the root of t and going only left
from_left s == the tree whose left branch is s
cat_left t1 t2 == the tree whose left branch is the concatenation of the left branches of t1 and t2
rightcomb n == the right comb binary tree of size n as a bintree
leftcomb n == the left comb binary tree of size n as a bintree
flip t == the left/right mirror of t
rightcombsz n == the right comb binary tree of size n as a bintreesz n
leftcombsz n == the left comb binary tree of size n as a bintreesz n
flipsz t == the left/right mirror of t as a bintreesz n

Rotations and Tamari order:

rotations t == the list of right rotations of the tree t
t1 <=T t2 == t1 is smaller than t2 in the Tamari order

Tamari bracketing vectors:

right_sizes t == the sequence in infix order reading of the node of t of the the sizes of the right subtrees
from_vct vct == recovers the tree t from its right sizes vector.
v \is a TamariVector == v is the right sizes vector of some tree t. The characterization of a Tamari vector of size n is that for all i < n then v_i + 1 < n and for all j such that i < j <= v_i + i then v_j + j <= v_i + i.

The function right_sizes and from_vct are two inverse bijections from binary trees to Tamari vectors as stated in theorems right_sizesK, right_sizesP and from_vctK.

vctleq v1 v2 = v1 <=V v2 == v1 and v2 are of the same lenght and v1 is smaller than v2 componentwise (ie. for all i then v1_i <= v2_i
vctmin v1 v2 == the componentwise min of v1 and v2

Tamari Lattice:

t1 \/T t2 == the meet of t1 and t2 in the Tamari lattice.
t1 /\T t2 == the join of t1 and t2 in the Tamari lattice.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import tools combclass ordtype.

Set Implicit Arguments.

Import Order.Theory.

Reserved Notation "x '<=T' y" (at level 70, y at next level).
Reserved Notation "x '<T' y" (at level 70, y at next level).
Reserved Notation "x '/\T' y" (at level 70, y at next level).
Reserved Notation "x '\/T' y" (at level 70, y at next level).

Inductive type for binary trees

Inductive bintree : predArgType :=
  | BinLeaf : bintree
  | BinNode : bintree -> bintree -> bintree.

Fixpoint eq_bintree (b1 b2 : bintree) : bool :=
  match b1, b2 with
  | BinLeaf, BinLeaf => true
  | BinNode l1 r1, BinNode l2 r2 => eq_bintree l1 l2 && eq_bintree r1 r2
  | _, _ => false
  end.

Lemma eq_bintreeP : Equality.axiom eq_bintree.

Fixpoint tree_encode (t : bintree) : GenTree.tree unit :=
  match t with
  | BinLeaf => GenTree.Leaf tt
  | BinNode tl tr => GenTree.Node 2 [:: tree_encode tl; tree_encode tr]
  end.
Fixpoint tree_decode (gt : GenTree.tree unit) :=
  match gt with
  | GenTree.Leaf tt => BinLeaf
  | GenTree.Node 2 [:: tl; tr] => BinNode (tree_decode tl) (tree_decode tr)
  | _ => BinLeaf

unused case

  end.

Lemma tree_encodeK : cancel tree_encode tree_decode.

Fixpoint size_tree t :=
  match t with
  | BinLeaf => 0
  | BinNode l r => 1 + (size_tree l) + (size_tree r)
  end.

Lemma LeafP t : reflect (t = BinLeaf) (size_tree t == 0).
Lemma size_tree_eq0 t : (size_tree t == 0) = (t == BinLeaf ).

Section Size.

Variable (n : nat).

Structure bintreesz : predArgType :=
  BinTreeSZ {trval :> bintree; _ : size_tree trval == n}.

Lemma bintreeszP (t : bintreesz) : size_tree t = n.

End Size.

Catalan numbers

The intent of the two following recursive definition is the recursion of lemmas CatalanS and enum_bintreeszS:
Fixpoint Catalan n :=
  if n is n'.+1 then
    sumn [Catalan i * Catalan (n - i) | i <- iota 0 n.+1]
  else 1.

however i and n - i are not structurally smaller than n.+1 so the definition is refused by coq as not well founded. So we write the following functions which returns a cache containing the list of the results of Catalan i and enum_bintreesz i for i = 0 ... n. Otherwise said, to define the enum_bintreesz function we need a strong nat induction where Coq only allows simple nat induction.

A seq of size n.+1 whose i-th element is Catalan i

Fixpoint Catalan_bin_leq n :=
  if n is n.+1 then
    let cr := Catalan_bin_leq n in
    let new := sumn [seq nth 0 cr i * nth 0 cr (n - i) | i <- iota 0 n.+1]
    in rcons cr new
  else [:: 1].
Definition Catalan_bin n := last 0 (Catalan_bin_leq n).

A seq of size n.+1 whose i-th element contains the list of all binary trees of size i

Fixpoint enum_bintreesz_leq n :=
  if n is n'.+1 then
    let rec := enum_bintreesz_leq n' in
    let listn :=
        flatten [seq [seq BinNode tl tr |
                      tl <- nth [::] rec i,
                      tr <- nth [::] rec (n' - i)] | i <- iota 0 n'.+1]
    in rcons rec listn
  else [:: [:: BinLeaf]].
Definition enum_bintreesz n := last [::] (enum_bintreesz_leq n).

Some tests :

Goal [seq Catalan_bin n | n <- iota 0 10] =
     [:: 1; 1; 2; 5; 14; 42; 132; 429; 1430; 4862].
Goal [seq size (enum_bintreesz n ) | n <- iota 0 10] =
     [:: 1; 1; 2; 5; 14; 42; 132; 429; 1430; 4862].

Lemma size_Catalan_bin_leq n : size (Catalan_bin_leq n) = n.+1.

Lemma size_enum_bintreesz n : size (enum_bintreesz_leq n) = n.+1.

Lemma size_enum_bintreeszE n : size (enum_bintreesz n) = Catalan_bin n.

Lemma Catalan_bin_leqE i m :
  i <= m -> nth 0 (Catalan_bin_leq m) i = Catalan_bin i.

Lemma enum_bintreesz_leq_leqE i n m :
  i <= n <= m ->
  nth [::] (enum_bintreesz_leq n) i = nth [::] (enum_bintreesz_leq m) i.

Lemma enum_bintreesz_leqE n m :
  n <= m -> enum_bintreesz n = nth [::] (enum_bintreesz_leq m) n.

Lemma Catalan_bin0 : Catalan_bin 0 = 1.

Lemma enum_bintreesz0 : enum_bintreesz 0 = [:: BinLeaf].

Lemma Catalan_binS n :
  Catalan_bin n.+1 = \sum_(0 <= i < n.+1) Catalan_bin i * Catalan_bin (n - i).

Lemma enum_bintreeszE n :
  enum_bintreesz n.+1 =
  flatten [seq [seq BinNode tl tr |
                tl <- enum_bintreesz i,
                tr <- enum_bintreesz (n - i)] | i <- iota 0 n.+1].

Lemma size_mem_enum_bintreeszP n t :
  t \in enum_bintreesz n -> size_tree t = n.

Lemma enum_bintreeszP n :
  all (fun t => size_tree t == n) (enum_bintreesz n).

Lemma enum_bintreesz_uniq n : uniq (enum_bintreesz n).

Lemma mem_enum_bintreesz n t :
  size_tree t == n -> t \in enum_bintreesz n.

Lemma enum_bintreesz_countE n t :
  size_tree t == n -> count_mem t (enum_bintreesz n) = 1.

Theorem card_bintreesz n : #|bintreesz n| = Catalan_bin n.

Left branch surgery in binary trees

Fixpoint left_branch t :=
  if t is BinNode l r then r :: left_branch l else [::].
Fixpoint from_left l :=
  if l is l0 :: l then BinNode (from_left l) l0 else BinLeaf.
Definition cat_left t1 t2 := from_left (left_branch t1 ++ left_branch t2).

Lemma left_branchK : cancel left_branch from_left.
Lemma from_leftK : cancel from_left left_branch.

Lemma cat_left0t t : cat_left BinLeaf t = t.
Lemma cat_leftt0 t : cat_left t BinLeaf = t.
Lemma cat_left_Node l r :
  cat_left (BinNode BinLeaf r) l = BinNode l r.
Lemma cat_leftA t u v :
  cat_left (cat_left t u) v = cat_left t (cat_left u v).
Lemma size_from_left s :
  size_tree (from_left s) = sumn [seq (size_tree t).+1 | t <- s].

Lemma size_cat_left t u :
  size_tree (cat_left t u) = size_tree t + size_tree u.

Lemma from_left_cat s1 s2 :
  from_left (s1 ++ s2) = cat_left (from_left s1) (from_left s2).

Lemma size_left_branch t :
  all (fun l => size_tree l < size_tree t) (left_branch t).

Various particular binary trees

Fixpoint rightcomb n :=
  if n is n'.+1 then
    BinNode BinLeaf (rightcomb n')
  else BinLeaf.
Fixpoint leftcomb n :=
  if n is n'.+1 then
    BinNode (leftcomb n') BinLeaf
  else BinLeaf.
Fixpoint flip t :=
  if t is BinNode l r then
    BinNode (flip r) (flip l)
  else BinLeaf.

Section SizeN.

Variable (n : nat).

Fact size_rightcomb : size_tree (rightcomb n) == n.
Canonical rightcombsz := BinTreeSZ size_rightcomb.

Lemma size_leftcomb : size_tree (leftcomb n) == n.
Canonical leftcombsz := BinTreeSZ size_leftcomb.

Lemma size_flip t : size_tree (flip t) = size_tree t.
Lemma flipK : involutive flip.
Lemma flip_rightcomb : flip (rightcomb n) = leftcomb n.
Lemma flip_leftcomb : flip (leftcomb n) = rightcomb n.

Fact flipsz_subproof (t : bintreesz n) : size_tree (flip t) == n.
Canonical flipsz t := BinTreeSZ (flipsz_subproof t).

Lemma flipszK : involutive flipsz.
Lemma flipsz_rightcomb : flipsz rightcombsz = leftcombsz.
Lemma flipsz_leftcomb : flipsz leftcombsz = rightcombsz.

End SizeN.

Tamari's lattice

Rotations in binary trees

Fixpoint rotations t :=
  if t is BinNode l r then
    let rec := [seq BinNode lrot r | lrot <- rotations l] ++
               [seq BinNode l rrot | rrot <- rotations r]
    in if l is BinNode ll lr then
         BinNode ll (BinNode lr r) :: rec
       else rec
  else [::].

Lemma rotations_left_sub l1 l2 r :
  l1 \in rotations l2 -> BinNode l1 r \in rotations (BinNode l2 r).

Lemma rotations_right_sub l r1 r2 :
  r1 \in rotations r2 -> BinNode l r1 \in rotations (BinNode l r2).

Lemma rotationP t1 t2 :
  reflect
    (exists a b c ,
        [\/ [/\ t1 = BinNode (BinNode a b) c & t2 = BinNode a (BinNode b c)],
            [/\ t1 = BinNode a c , t2 = BinNode b c & b \in rotations a ] |
            [/\ t1 = BinNode a b , t2 = BinNode a c & c \in rotations b ]])
    (t2 \in rotations t1).

Lemma size_rotations t t' :
  t' \in rotations t -> size_tree t' = size_tree t.

Lemma rotations_flip_impl t1 t2:
  (t1 \in rotations t2 ) -> (flip t2 \in rotations (flip t1)).

Lemma rotations_flip t1 t2:
  (t1 \in rotations t2 ) = (flip t2 \in rotations (flip t1)).

Lemma catleft_rotations t t1 t2 :
  t1 \in rotations t2 -> (cat_left t t1 ) \in rotations (cat_left t t2).

Lemma rightcomb_rotations n : rotations (rightcomb n) = [::].
Lemma rightcomb_rotationsE t :
  (rotations t == [::]) = (t == rightcomb (size_tree t)).
Lemma leftcomb_rotations t : leftcomb (size_tree t) \notin rotations t.

Tamari vectors

Fixpoint right_sizes t :=
  if t is BinNode l r then
        right_sizes l ++ size_tree r :: right_sizes r
  else [::].
Fixpoint is_Tamari v :=
  if v is v0 :: v' then
    [&& v0 <= size v',
     is_Tamari v' &
     all (fun i => nth 0 v' i + i < v0) (iota 0 v0)]
  else true.
Definition TamariVector := [qualify a v : seq nat | is_Tamari v ].

Lemma sumn_right_sizes_gt t t' :
  t' \in rotations t -> sumn (right_sizes t) < sumn (right_sizes t').

Lemma rotations_neq t t' : t' \in rotations t -> t != t'.

Lemma size_right_sizes t : size (right_sizes t) = size_tree t.

Lemma right_sizes_left_comb n :
  right_sizes (leftcomb n) = nseq n 0.

Lemma right_sizes_from_left s :
  right_sizes (from_left s) =
  flatten [seq size_tree t :: right_sizes t | t <- rev s].

Lemma right_sizes_cat_left t1 t2 :
  right_sizes (cat_left t1 t2) = right_sizes t2 ++ right_sizes t1.

Lemma Tamari_consP v0 v :
  reflect
    [/\ v0 <= size v ,
     v \is a TamariVector &
     forall i, i < v0 -> nth 0 v i + i < v0 ]
    (v0 :: v \is a TamariVector).

Lemma TamariP v :
  reflect
    ((forall i, i < size v -> nth 0 v i + i < size v ) /\
     (forall i j, i < j <= nth 0 v i + i -> nth 0 v j + j <= nth 0 v i + i ))
    (v \is a TamariVector).

Lemma Tamari_drop n v :
  v \is a TamariVector -> drop n v \is a TamariVector.

Lemma Tamari_catr u v :
  u ++ v \is a TamariVector -> v \is a TamariVector.

Lemma Tamari_take v0 v :
  v0 :: v \is a TamariVector -> take v0 v \is a TamariVector.

Lemma Tamari_cat v1 v2 :
  v1 \is a TamariVector ->
  v2 \is a TamariVector ->
  v1 ++ v2 \is a TamariVector.

Lemma cons_TamariP v : v \is a TamariVector -> size v :: v \is a TamariVector.

Theorem right_sizesP t : right_sizes t \is a TamariVector.

#[local] Hint Resolve right_sizesP : core.

Bijection with Tamari vectors

Fixpoint from_vct_rec fuel lft vct :=
  if fuel is fuel.+1 then
    if vct is v0 :: vct' then
      from_vct_rec fuel
                   (BinNode lft (from_vct_rec fuel BinLeaf (take v0 vct')))
                   (drop v0 vct')
    else lft
  else BinLeaf.
Definition from_vct_acc lft vct := from_vct_rec (size vct).+1 lft vct.
Definition from_vct := from_vct_acc BinLeaf.

Section Tests.

Goal [seq right_sizes t | t <- enum_bintreesz 3] =
[:: [:: 2; 1; 0]; [:: 2; 0; 0]; [:: 0; 1; 0]; [:: 1; 0; 0]; [:: 0; 0; 0]].

Goal [seq right_sizes t | t <- enum_bintreesz 4] =
[:: [:: 3; 2; 1; 0]; [:: 3; 2; 0; 0]; [:: 3; 0; 1; 0]; [:: 3; 1; 0; 0];
    [:: 3; 0; 0; 0]; [:: 0; 2; 1; 0]; [:: 0; 2; 0; 0]; [:: 1; 0; 1; 0];
    [:: 0; 0; 1; 0]; [:: 2; 1; 0; 0]; [:: 2; 0; 0; 0]; [:: 0; 1; 0; 0];
    [:: 1; 0; 0; 0]; [:: 0; 0; 0; 0] ].

Let bla := Eval hnf in nth BinLeaf (enum_bintreesz 5) 21.
Goal right_sizes bla = [:: 0; 0; 2; 1; 0].

Goal [seq right_sizes rot | rot <- rotations bla ] =
[:: [:: 0; 3; 2; 1; 0]; [:: 1; 0; 2; 1; 0]].

Goal all
     (fun i => all (fun t => t == from_vct (right_sizes t )) (enum_bintreesz i ))
     (iota 0 7).

Goal all
     (fun i => all (fun t => right_sizes t \is a TamariVector ) (enum_bintreesz i ))
     (iota 0 7).

Goal [:: 1; 1; 0] \isn't a TamariVector.
Goal [:: 2; 0; 1; 0] \isn't a TamariVector.

Goal [:: 2; 0; 0; 1; 0] \is a TamariVector.

End Tests.

Lemma from_vct_acc_nil lft : from_vct_acc lft [::] = lft.

Lemma from_vct_fuelE fuel lft vct :
  size vct < fuel -> from_vct_rec fuel lft vct = from_vct_acc lft vct.

Lemma from_vct_accE lft v0 vct :
  from_vct_acc lft (v0 :: vct) =
  from_vct_acc (BinNode lft (from_vct_acc BinLeaf (take v0 vct)))
               (drop v0 vct).

Lemma from_vct_cat_leftE lft vct :
  from_vct_acc lft vct = cat_left (from_vct_acc BinLeaf vct) lft.

Lemma size_from_vct_acc s :
  size_tree (from_vct_acc BinLeaf s) = size s.

Lemma size_from_vct s :
  size_tree (from_vct s) = size s.

Theorem right_sizesK : cancel right_sizes from_vct.

Theorem from_vctK : {in TamariVector , cancel from_vct right_sizes }.

Lemma from_vct_cat u v t :
  u \is a TamariVector ->
  from_vct_acc t (u ++ v) = from_vct_acc (from_vct_acc t u) v.

Lemma from_vct0 n : from_vct (nseq n 0) = leftcomb n.

Comparison of Tamari vectors

Definition vctleq v1 v2 :=
  (size v1 == size v2 ) && (all (fun p => p .1 <= p .2) (zip v1 v2)).
Definition vctmin v1 v2 := [seq minn p .1 p .2 | p <- zip v1 v2].

#[local] Notation "x '<=V' y" := (vctleq x y) (at level 70, y at next level).

Section TestsComp.

Goal all (fun t => all
                     (vctleq (right_sizes t ))
                     [seq right_sizes rot | rot <- rotations t ])
     (enum_bintreesz 6).

End TestsComp.

Lemma vctleqP v1 v2 :
  reflect (size v1 = size v2 /\ forall i, nth 0 v1 i <= nth 0 v2 i)
          (v1 <=V v2).

Lemma vctleq_refl : reflexive vctleq.
Lemma vctleq_trans : transitive vctleq.
Lemma vctleq_anti : antisymmetric vctleq.

Lemma vctleq_sumn_right_sizes t1 t2 :
  right_sizes t1 <=V right_sizes t2 ->
  sumn (right_sizes t1) <= sumn (right_sizes t2) ?= iff (t1 == t2).

Lemma all_leqzip_refl l : all (fun p => p .1 <= p .2) (zip l l).

Lemma size_vctmin v1 v2 : size (vctmin v1 v2) = minn (size v1) (size v2).
Lemma nth_vctmin v1 v2 i :
  nth 0 (vctmin v1 v2) i = minn (nth 0 v1 i) (nth 0 v2 i).

Lemma vctminC: commutative vctmin.

Lemma vctminPr v1 v2 :
  size v1 = size v2 -> vctmin v1 v2 <=V v2.

Lemma vctminPl v1 v2 :
  size v1 = size v2 -> vctmin v1 v2 <=V v1.

Lemma vctminP v1 v2 v :
  v <=V v1 -> v <=V v2 -> v <=V (vctmin v1 v2 ).

Lemma vctmin_Tamari v1 v2 :
  size v1 = size v2 ->
  v1 \is a TamariVector ->
  v2 \is a TamariVector ->
  vctmin v1 v2 \is a TamariVector.

Correspondence between rotation on binary trees and Tamari vectors

Lemma rotations_vctleq_impl t1 t2 :
  t1 \in rotations t2 -> right_sizes t2 <=V right_sizes t1.

Lemma Tamari_add_head v0 v :
  v0 :: v \is a TamariVector ->
  v0 < size v ->
  (nth 0 v v0 + v0).+1 :: v \is a TamariVector.

Lemma rotations_add_head v0 v t :
  v0 :: v \is a TamariVector ->
  (nth 0 v v0 + v0).+1 :: v \is a TamariVector ->
  from_vct_acc t ((nth 0 v v0 + v0).+1 :: v) \in
    rotations (from_vct_acc t (v0 :: v)).

Lemma Tamari_add_min u v0 v w0 w :
  u ++ w0 :: w \is a TamariVector ->
  u ++ v0 :: v <=V u ++ w0 :: w ->
  v0 < w0 ->
  nth 0 v v0 + v0 < w0.

Lemma Tamari_add_bounded u v0 v w0 w :
  u ++ v0 :: v \is a TamariVector ->
  u ++ w0 :: w \is a TamariVector ->
  u ++ v0 :: v <=V u ++ w0 :: w ->
  v0 < w0 ->
  u ++ (nth 0 v v0 + v0).+1 :: v \is a TamariVector.

Lemma rotations_add u v0 v :
  u ++ v0 :: v \is a TamariVector ->
  u ++ (nth 0 v v0 + v0).+1 :: v \is a TamariVector ->
  from_vct (u ++ (nth 0 v v0 + v0).+1 :: v)
           \in rotations (from_vct (u ++ v0 :: v)).

Lemma rotations_add_bounded u v0 v w0 w :
  u ++ v0 :: v \is a TamariVector ->
  u ++ w0 :: w \is a TamariVector ->
  u ++ v0 :: v <=V u ++ w0 :: w ->
  v0 < w0 ->
  from_vct (u ++ (nth 0 v v0 + v0).+1 :: v)
           \in rotations (from_vct (u ++ v0 :: v)).

Lemma vctleq_rotation t1 t2 :
  right_sizes t1 <=V right_sizes t2 ->
  t1 != t2 ->
  exists t , t \in rotations t1 /\ right_sizes t <=V right_sizes t2.

Theorem rotations_right_sizesP t1 t2 :
  reflect
    (exists u v0 v ,
        right_sizes t1 = u ++ v0 :: v /\
        right_sizes t2 = u ++ (nth 0 v v0 + v0).+1 :: v)
    (t2 \in rotations t1).

Lemma vct_succ u v0 v w :
  w \is a TamariVector ->
  u ++ v0 :: v <=V w ->
  w <=V u ++ (nth 0 v v0 + v0).+1 :: v ->
  w = u ++ v0 :: v \/ w = u ++ (nth 0 v v0 + v0).+1 :: v.

Fact Tamari_display : unit.
Notation "x <=T y" := (@Order.le Tamari_display _ x y).
Notation "x <T y" := (@Order.lt Tamari_display _ x y).
Notation "x /\T y" := (@Order.meet Tamari_display _ x y).
Notation "x \/T y" := (@Order.join Tamari_display _ x y).

Definition of Tamari order

Module TamariLattice.
Section TamariLattice.

Variable n : nat.
Implicit Type t : bintreesz n.

Definition Tamari := connect (fun t1 t2 : bintreesz n => grel rotations t1 t2).

Lemma Tamari_sumn_right_sizes t1 t2 :
  Tamari t1 t2 ->
  sumn (right_sizes t1) <= sumn (right_sizes t2) ?= iff (t1 == t2).

Fact Tamari_refl : reflexive Tamari.
Fact Tamari_trans : transitive Tamari.
Fact Tamari_anti : antisymmetric Tamari.

#[export ] HB.instance Definition _ :=
  Order.Le_isPOrder.Build Tamari_display (bintreesz n )
    Tamari_refl Tamari_anti Tamari_trans.

Lemma TamariE t1 t2 :
  (t1 <=T t2 ) = connect (fun t t' => grel rotations t t') t1 t2.

Lemma rotations_Tamari t t' : trval t' \in rotations t -> t <T t'.

Lemma Tamari_flip t1 t2 : (flipsz t2 <=T flipsz t1 ) = (t1 <=T t2 ).

Theorem Tamari_vctleq t1 t2 :
  (right_sizes t1 <=V right_sizes t2 ) = (t1 <=T t2 ).

Lemma Tmeet_proof t1 t2 :
  size_tree (from_vct (vctmin (right_sizes t1) (right_sizes t2))) == n.
Definition Tmeet t1 t2 := BinTreeSZ (Tmeet_proof t1 t2).
Definition Tjoin t1 t2 := flipsz (Tmeet (flipsz t1) (flipsz t2)).

Lemma TmeetC t1 t2 : Tmeet t1 t2 = Tmeet t2 t1.

Lemma TmeetPr t1 t2 : Tmeet t1 t2 <=T t2.

Fact TmeetP t t1 t2 : (t <=T Tmeet t1 t2 ) = (t <=T t1 ) && (t <=T t2 ).
Fact TjoinP t1 t2 t : (Tjoin t1 t2 <=T t ) = (t1 <=T t ) && (t2 <=T t ).
#[export ] HB.instance Definition _ :=
  Order.POrder_MeetJoin_isLattice.Build Tamari_display
    (bintreesz n ) TmeetP TjoinP.

Lemma flipsz_meet t1 t2 : flipsz (t1 \/T t2) = (flipsz t1 /\T flipsz t2 ).
Lemma flipsz_join t1 t2 : flipsz (t1 /\T t2) = (flipsz t1 \/T flipsz t2 ).

Lemma right_sizes_meet t1 t2 :
  right_sizes (t1 /\T t2) = vctmin (right_sizes t1) (right_sizes t2).

Fact leftcomb_bottom t : leftcombsz n <=T t.
Fact rightcomb_top t : t <=T rightcombsz n.
#[export ] HB.instance Definition _ :=
  Order.hasBottom.Build Tamari_display (bintreesz n ) leftcomb_bottom.
#[export ] HB.instance Definition _ :=
  Order.hasTop.Build Tamari_display (bintreesz n ) rightcomb_top.

Lemma botETamari : 0%O = leftcombsz n.
Lemma topETamari : 1%O = rightcombsz n.

End TamariLattice.

Module Exports.

Definition TamariE := TamariE.
Definition rotations_Tamari := rotations_Tamari.
Definition Tamari_flip := Tamari_flip.
Definition Tamari_vctleq := Tamari_vctleq.
Definition flipsz_meet := flipsz_meet.
Definition flipsz_join := flipsz_join.
Definition right_sizes_meet := right_sizes_meet.
Definition botETamari := botETamari.
Definition topETamari := topETamari.

End Exports.
End TamariLattice.

Section TamariCover.

Variable n : nat.
Implicit Type t : bintreesz n.

Lemma Tamari_succ t1 t2 t :
  trval t2 \in rotations t1 -> t1 <=T t -> t <=T t2 -> t = t1 \/ t = t2.

Lemma covers_Tamari t1 t2 : (trval t2 \in rotations t1 ) = (covers t1 t2 ).

End TamariCover.