Grace/Core/Syntax.g17

Open in Workbench Download source

Imports

Grace.Core.Nat

Declarations

• TermSyntax datatype
• FormulaSyntax datatype
• GoalSyntax datatype
• TacticSyntax datatype
• size def
• size.atom theorem derivation
• cost def
• cost.example theorem derivation

Source

1-- Syntax datatypes for metaprogramming2-- 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.Syntax8namespace Grace.Core.Syntax9import Grace.Core.Nat10open Grace.Core.Nat.Rec1112-- Kernel-facing syntax is set-theoretic data.  Names are Sets;13-- recursive syntax positions are checked by the generated inductive class.14datatype TermSyntax15  | variable(name : Set)16  | application(function : Set, argument : self)1718datatype FormulaSyntax19  | atom(relation left right : Set)20  | implication(left right : self)21  | universal(variable : Set, body : self)2223datatype GoalSyntax24  | goal(context target : Set)2526-- This is a small executable language for compiled tactic plans.  An27-- interpreter can later map these constructors to checked proof-producing28-- primitives; the datatype itself never extends the trusted kernel.29datatype TacticSyntax30  | exactStep(theoremName : Set)31  | introStep(name : Set, continuation : self)32  | sequence(first second : self)33  | choice(first second : self)34  | repeatStep(body : self)3536namespace Formula3738def size (formula : FormulaSyntax) -> Nat39  | FormulaSyntax.atom(relation, left, right) => 140  | FormulaSyntax.implication(left, right) => succ(add(size(left), size(right)))41  | FormulaSyntax.universal(variable, body) => succ(size(body))4243theorem size.atom44  shows size(FormulaSyntax.atom(1, 2, 3)) = 145proof46  compute4748end Formula4950namespace Tactic5152def cost (tactic : TacticSyntax) -> Nat53  | TacticSyntax.exactStep(theoremName) => 154  | TacticSyntax.introStep(name, continuation) => succ(cost(continuation))55  | TacticSyntax.sequence(first, second) => add(cost(first), cost(second))56  | TacticSyntax.choice(first, second) => add(cost(first), cost(second))57  | TacticSyntax.repeatStep(body) => succ(cost(body))5859theorem cost.example60  shows cost(TacticSyntax.sequence(TacticSyntax.exactStep(1), TacticSyntax.introStep(2, TacticSyntax.exactStep(3)))) = 361proof62  compute6364end Tactic6566eval Formula.size(FormulaSyntax.implication(FormulaSyntax.atom(1, 2, 3), FormulaSyntax.universal(4, FormulaSyntax.atom(5, 6, 7))))67eval Tactic.cost(TacticSyntax.sequence(TacticSyntax.exactStep(1), TacticSyntax.introStep(2, TacticSyntax.exactStep(3))))6869end Grace.Core.Syntax70