-- Algebraic datatypes and structural recursion
-- Part of the Grace17 proof assistant for mathematics based on set theory.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Core.Data
namespace Grace.Core.Data
import Grace.Core.Nat
export open Grace.Core.Data

-- Constructor values execute as compact nodes. Every constructor also has a
-- generated representation theorem identifying it with a tagged Kuratowski
-- set, so these values live in the same set universe as everything else.
datatype Bool
  | false
  | true

datatype Option(A : Set)
  | none
  | some(value : A)

datatype List(A : Set)
  | nil
  | cons(head : A, tail : self)

-- Right associative: a :: b :: xs means a :: (b :: xs).
notation infixr 55 "::" => List.cons

datatype Tree(A : Set)
  | leaf(value : A)
  | node(left right : self)

namespace BoolOps

def not (b : Bool) -> Bool
  | Bool.false => Bool.true
  | Bool.true => Bool.false

def and (a : Bool, b : Bool) -> Bool
  | Bool.false, b => Bool.false
  | Bool.true, b => b

theorem not.involutive (b : Bool)
  shows not(not(b)) = b
proof
  induction b
  | Bool.false =>
    unfold not
    rfl
  | Bool.true => simp [not]

theorem not.boolean (b : Bool)
  shows Bool(not(b))
proof
  induction b
  | Bool.false =>
    simp [not]
    typecheck
  | Bool.true =>
    simp [not]
    typecheck

end BoolOps

namespace OptionOps

def getOr {A : Set} (fallback : Set, option : Option(A)) -> Set
  | fallback, Option.none => fallback
  | fallback, Option.some(x) => x

end OptionOps

namespace ListOps

def length {A : Set} (xs : List(A)) -> Nat
  | List.nil => 0
  | List.cons(x, tail) => succ(length(tail))

def append {A : Set} (ys xs : List(A)) -> List(A)
  | ys, List.nil => ys
  | ys, List.cons(x, tail) => List.cons(x, append(ys, tail))

def reverse {A : Set} (xs : List(A)) -> List(A)
  | List.nil => List.nil
  | List.cons(x, tail) => append(List.cons(x, List.nil), reverse(tail))

theorem length.closed {A : Set} (xs : List(A))
  shows Nat(length(xs))
proof
  induction xs
  | List.nil => settle with length, Naturals.constructor.zero
  | List.cons(x, tail) using ih => settle with length, Naturals.constructor.succ, ih

theorem append.right_unit {A : Set} (xs : List(A))
  shows append(List.nil, xs) = xs
proof
  induction xs
  | List.nil => settle with append
  | List.cons(x, tail) using ih => settle with append, ih

theorem length.append {A : Set} (ys xs : List(A))
  shows length(append(ys, xs)) = add(length(xs), length(ys))
proof
  induction xs
  | List.nil => settle with append, length, add
  | List.cons(x, tail) using ih => settle with append, length, add, ih

theorem length.two
  shows length{A := omega}(List.cons(17, List.cons(4, List.nil))) = 2
proof
  compute

-- The recursive spine is finite even when an element is an infinite set.
theorem length.infinite_payload
  shows length{A := union(pair(pair(1, 2), pair(omega, omega)))}(List.cons(1, List.cons(2, List.cons(omega, List.nil)))) = 3
proof
  compute

end ListOps

namespace TreeOps

def size {A : Set} (tree : Tree(A)) -> Nat
  | Tree.leaf(value) => 1
  | Tree.node(left, right) => add(size(left), size(right))

def mirror {A : Set} (tree : Tree(A)) -> Tree(A)
  | Tree.leaf(value) => Tree.leaf(value)
  | Tree.node(left, right) => Tree.node(mirror(right), mirror(left))

theorem mirror.involutive {A : Set} (tree : Tree(A))
  shows mirror(mirror(tree)) = tree
proof
  induction tree
  | Tree.leaf(value) => settle with mirror
  | Tree.node(left, right) using ihLeft, ihRight => settle with mirror, ihLeft, ihRight

theorem size.three
  shows size{omega}(Tree.node(Tree.leaf(1), Tree.node(Tree.leaf(2), Tree.leaf(3)))) = 3
proof
  compute

end TreeOps

eval BoolOps.not(BoolOps.not(Bool.true))
eval ListOps.length{omega}(List.cons(17, List.cons(4, List.nil)))
eval ListOps.length{A := union(pair(pair(1, 2), pair(omega, omega)))}(List.cons(1, List.cons(2, List.cons(omega, List.nil))))
eval TreeOps.size{A := omega}(Tree.node(Tree.leaf(1), Tree.node(Tree.leaf(2), Tree.leaf(3))))

export open Grace.Core.Data.BoolOps
export open Grace.Core.Data.OptionOps
export open Grace.Core.Data.ListOps
export open Grace.Core.Data.TreeOps

end Grace.Core.Data