// SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
// For more information, please refer to <https://unlicense.org/>
// SPDX-License-Identifier: Unlicense

module TreeJazz

// A simple inductively-defined type, some simple functions on it,
// with some simple intrinsic and extrinsic proofs of their properties.

type tree a =
    | Leaf   : leaf:a -> tree a
    | Branch : left:tree a -> right:tree a -> tree a

let rec size #a (t:tree a) : result:nat { result >= 1 } =
    match t with
        | Leaf _            -> 1
        | Branch left right -> size left + size right

let rec reflect #a (t:tree a) : result:tree a { size t = size result } =
    match t with
        | Leaf n            -> Leaf n
        | Branch left right -> Branch (reflect right) (reflect left)

let rec reflect_involutive #a (t:tree a) : Lemma (reflect (reflect t) == t) =
    match t with
        | Leaf n            -> ()
        | Branch left right ->
            reflect_involutive right;
            reflect_involutive left