Grace/Core/Data.g17

Open in Workbench Download source

Imports

Grace.Core.Nat

Declarations

• Bool datatype
• Option datatype
• List datatype
• Tree datatype
• not def
• and def
• not.involutive theorem derivation
• not.boolean theorem derivation
• getOr def
• length def
• append def
• reverse def
• length.closed theorem derivation
• append.right_unit theorem derivation
• length.append theorem derivation
• length.two theorem derivation
• length.infinite_payload theorem derivation
• size def
• mirror def
• mirror.involutive theorem derivation
• size.three theorem derivation

Source

1-- Algebraic datatypes and structural recursion2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Core.Data8namespace Grace.Core.Data9import Grace.Core.Nat10export open Grace.Core.Data1112-- Constructor values execute as compact nodes. Every constructor also has a13-- generated representation theorem identifying it with a tagged Kuratowski14-- set, so these values live in the same set universe as everything else.15datatype Bool16  | false17  | true1819datatype Option(A : Set)20  | none21  | some(value : A)2223datatype List(A : Set)24  | nil25  | cons(head : A, tail : self)2627-- Right associative: a :: b :: xs means a :: (b :: xs).28notation infixr 55 "::" => List.cons2930datatype Tree(A : Set)31  | leaf(value : A)32  | node(left right : self)3334namespace BoolOps3536def not (b : Bool) -> Bool37  | Bool.false => Bool.true38  | Bool.true => Bool.false3940def and (a : Bool, b : Bool) -> Bool41  | Bool.false, b => Bool.false42  | Bool.true, b => b4344theorem not.involutive (b : Bool)45  shows not(not(b)) = b46proof47  induction b48  | Bool.false =>49    unfold not50    rfl51  | Bool.true => simp [not]5253theorem not.boolean (b : Bool)54  shows Bool(not(b))55proof56  induction b57  | Bool.false =>58    simp [not]59    typecheck60  | Bool.true =>61    simp [not]62    typecheck6364end BoolOps6566namespace OptionOps6768def getOr {A : Set} (fallback : Set, option : Option(A)) -> Set69  | fallback, Option.none => fallback70  | fallback, Option.some(x) => x7172end OptionOps7374namespace ListOps7576def length {A : Set} (xs : List(A)) -> Nat77  | List.nil => 078  | List.cons(x, tail) => succ(length(tail))7980def append {A : Set} (ys xs : List(A)) -> List(A)81  | ys, List.nil => ys82  | ys, List.cons(x, tail) => List.cons(x, append(ys, tail))8384def reverse {A : Set} (xs : List(A)) -> List(A)85  | List.nil => List.nil86  | List.cons(x, tail) => append(List.cons(x, List.nil), reverse(tail))8788theorem length.closed {A : Set} (xs : List(A))89  shows Nat(length(xs))90proof91  induction xs92  | List.nil => settle with length, Naturals.constructor.zero93  | List.cons(x, tail) using ih => settle with length, Naturals.constructor.succ, ih9495theorem append.right_unit {A : Set} (xs : List(A))96  shows append(List.nil, xs) = xs97proof98  induction xs99  | List.nil => settle with append100  | List.cons(x, tail) using ih => settle with append, ih101102theorem length.append {A : Set} (ys xs : List(A))103  shows length(append(ys, xs)) = add(length(xs), length(ys))104proof105  induction xs106  | List.nil => settle with append, length, add107  | List.cons(x, tail) using ih => settle with append, length, add, ih108109theorem length.two110  shows length{A := omega}(List.cons(17, List.cons(4, List.nil))) = 2111proof112  compute113114-- The recursive spine is finite even when an element is an infinite set.115theorem length.infinite_payload116  shows length{A := union(pair(pair(1, 2), pair(omega, omega)))}(List.cons(1, List.cons(2, List.cons(omega, List.nil)))) = 3117proof118  compute119120end ListOps121122namespace TreeOps123124def size {A : Set} (tree : Tree(A)) -> Nat125  | Tree.leaf(value) => 1126  | Tree.node(left, right) => add(size(left), size(right))127128def mirror {A : Set} (tree : Tree(A)) -> Tree(A)129  | Tree.leaf(value) => Tree.leaf(value)130  | Tree.node(left, right) => Tree.node(mirror(right), mirror(left))131132theorem mirror.involutive {A : Set} (tree : Tree(A))133  shows mirror(mirror(tree)) = tree134proof135  induction tree136  | Tree.leaf(value) => settle with mirror137  | Tree.node(left, right) using ihLeft, ihRight => settle with mirror, ihLeft, ihRight138139theorem size.three140  shows size{omega}(Tree.node(Tree.leaf(1), Tree.node(Tree.leaf(2), Tree.leaf(3)))) = 3141proof142  compute143144end TreeOps145146eval BoolOps.not(BoolOps.not(Bool.true))147eval ListOps.length{omega}(List.cons(17, List.cons(4, List.nil)))148eval ListOps.length{A := union(pair(pair(1, 2), pair(omega, omega)))}(List.cons(1, List.cons(2, List.cons(omega, List.nil))))149eval TreeOps.size{A := omega}(Tree.node(Tree.leaf(1), Tree.node(Tree.leaf(2), Tree.leaf(3))))150151export open Grace.Core.Data.BoolOps152export open Grace.Core.Data.OptionOps153export open Grace.Core.Data.ListOps154export open Grace.Core.Data.TreeOps155156end Grace.Core.Data157