ProofKit

ADT toolkit and Proof verifier based on LogicKit.

Project WIKI: link

PetriKit Lib: link

Implemented ADTs

Currently implemented ADT and Operators

ADT	Generators	Constructor	Operators
Boolean	True() False()	n(Bool)	not(x) and(x,y) or(x,y)
Nat	zero() succ(x)	n(Int)	add(x,y) mul(x,y) sub(x,y) div(x,y) mod(x) lt(x,y) gt(x,y) eq(x,y) gcd(x,y)
Integer	int(x,y)	n(Int)	add(x,y) mul(x,y) sub(x,y) div(x,y) abs(x), normalize(x) lt(x,y) gt(x,y) eq(x,y) sign(x)
Multiset	empty() cons(first, rest)	n([Term])	first(x) rest(x) contains(x,y) size(x) concat(x,y) removeOne(x,y) removeAll(x,y) eq(x,y)
Set	empty() cons(first, rest)	n([Term])	union(x,y) subSet(x,y) intersection(x,y) difference(x,y) contains(x,y) size(x) removeOne(x,y) eq(x,y) insert(x,y)
Sequence	empty(), cons(value,index,rest)	n([Term])	push(value,rest), getAt(sequence, index), setAt(sequence, index, value) size(sequence)

Implemented Proofs:

Name	Call	Status
reflexivity	Proof.reflexivity(Term) -> Rule	tested
symmetry	Proof.symmetry(Rule) -> Rule	tested
transitivity	Proof.transitivity(Rule, Rule) -> Rule	tested
substitution	Proof.substitution(Rule, Variable, Term) -> Rule	tested
substitutivity	Proof.substitutivity((Term...)->Term, [Term], [Term]) -> Rule	tested
inductive	Proof.inductive(Rule, Variable, ADT, [String:(Rule...)->Rule])	-

Your first code

Write your first code is simple, just import ProofKit inside your package.swift:

import PackageDescription

let package = Package(
    name: "YourPackageName",
    dependencies: [
        // Dependencies declare other packages that this package depends on.
        .package(
            url: "https://github.com/Mandarancio/ProofKit.git",
            .branch("master")
        ),
    ],
    targets: [
        .target(
            name: "YourPackageName",
            dependencies: ["ProofKit"]),
        .testTarget(
            name: "YourPackageNameTests",
            dependencies: ["YourPackageName"]),
    ]
)

And finally your code in main.swift:

import SwiftKanren
import ProofKit

let x = Variable(named: "x")
let y = Variable(named: "y")

let goal = (x < Nat.self && y < Nat.self) => ((x + y) <-> Nat.n(5))
for solution in solve(goal).prefix(11)
{
  let rsolution = solution.reified()
  print("x: \(ADTm.pprint(rsolution[x])), y: \(ADTm.pprint(rsolution[y]))")
}

Once compiled and executed (remember: the binary is located .build/debug/YOUR_PROJECT_NAME) the output should be:

x: 0, y: 5
x: 1, y: 4
x: 2, y: 3
x: 3, y: 2
x: 4, y: 1
x: 5, y: 0

Advanced usage

Rule

The struct Rule is the container of axioms and future theorems. Is composed in left and right components (both Term) and implement both a function to apply the rule and one to pretty print it. To create a rule simply:

 1> let r = Rule(
      Nat.add(Variable(named: "x"), Nat.zero()), // left component
      Variable(named: "x"), // right component
      Boolean.True() // optional Boolean condition (default: Boolean.True())
    )

Print the rule:

 2> print(r)
x + 0 = x

Apply it:

 3> let g : Goal = r.apply(Nat.n(4) + Nat.zero(), Variable(named: x)) // create goal (4+0) to applay rule
 4> let res : Term = get_result(g,x) //function solve goal and return the substitution of x
 5> print(ADTm.pprint(res))
4

ADT

All ADTm extend the base class ADT, this contains both generator, opertors generator and operators axioms as well as some basic helpers such a chek type and a pretty print function.

To access to axioms, generators and operators there are always two methods, a long and a shortcut, e.g. get_generator("name") and g("name").

For both generators and operators is possible to access just using ["name"].

Adding operators and axioms is possible only internally. A simple example is a simplify version of the boolean adt:

public class Boolean : ADT {
    public init(){
      super.init("boolean")
      self.add_generator("true", Boolean.True)
      self.add_generator("false", Boolean.False)
      self.add_operator("not", Boolean.not, [
        Rule(Boolean.not(Boolean.False()),Boolean.True()),
        Rule(Boolean.not(Boolean.True()),Boolean.False())
      ], ["boolean"])
    }
    public static func True(_:Term...) -> Term{
      return new_term(Value<Bool>(true), "boolean")
    }

    public static func False(_:Term...) -> Term{
      return new_term(Value<Bool>(false), "boolean")
    }

    public static func not(_ operands: Term...)->Term{
      return Operator.n(Value("nil"), operands[0], "not")
    }
}

ADTManager

Finally to manage the ADT and have the possibility to mixit together in the future we use an ADTManager. This is composed by a dictionary of ADT and some helper function (such as the pretty printer).

To avoid the creation of multiple ADTManager, there is a single ADTManager (as the constructor is private) instance called ADTm.

To get or add an ADT from the instance ADTm:

let nat : ADT = ADTm["nat"] // to get adt
/// or
ADTm["boolean"] = Boolean() // to add adt

To pretty print any term:

let t = Nat.n(1) + Nat.n(1)
print("\(ADTm.pprint(t))")
//// 1 + 1
print(t)
//// [type: operator, name: "+", 0: [type: nat, value: [succ: [type: nat, value: 0]]]....

Universal Evaluator

A simple inner most universal evaluator is implemented. To use it:

let operation : Term = Nat.n(2) * Nat.n(3)
let result : Term = ADTm.eval(operation)
print(" \(ADTm.pprint(operation)) => \(ADTm.pprint(result))")
//// 2 * 3 => 6

To be able to perform any type of computation it trys to solve the inner most operation first using the operation axioms and the generator evaluator.

How to create an ADT?

You can see an exemple at Source/ADTDemo First create a file with the name of your adt. You have a typical example at Source/ADTDemo/char.swift Two mains steps when you create your own ADT:

• Create Generators
• Create Operators

You have to add this in public init() and create a function for each generator and operator.

Moreover you have to override some basics functions for the inheritance if you want that your ADT works! This functions are:

• belong (Goal to know if a term belong to this adt)
• check (Simple check to check if a term is of this adt type)
• pprint (Print nicely your term)

Nice you have your ADT, but it's not the end! We have seen above the ADTManager. You have to add all of your ADT in this ADTManager. You can do it easily as follows:

// Then you add your new adt to the manager
ADTm["char"] = Char()

You have a simple example how ADTManager works at Source/ADTDemo/main.swift. You can make tests with your own ADT that you can add into an ADTManager to use it. Now you can easily use and test your ADT. Use your ADT to create your variable and use the ADTManager to evaluate operations.

// Example:

let a = Char.a()
let b = Char.b()
var op = a == b
var r = ADTm.eval(op)
print("\(ADTm.pprint(op)) => \(ADTm.pprint(r))")
// a == b => false

Proofs

Now we have all ADT that we need and we can use it for proofs. Firstly, you have several examples avaible in Source/EqProofDemo. When you want to verify a proof, you need to write all the steps. For classical proof you just have to follow the example that are avaible.

If you want to create your own induction proof, here are the steps to follow:

1. You just have to specify axioms that you will need.

 let ax0 = ADTm["nat"].a("+")[0]
 let ax1 = ADTm["nat"].a("+")[1]

2. Write the conjecture you want to verify.

// We try to proof that succ(0) + x = suc(x)
let conj = Rule(
  Nat.add(Nat.succ(x: Nat.zero()), Variable(named:"x")),
  Nat.succ(x: Variable(named: "x"))
)

3. For each generators you have to verify the initial case and the higher rank. Here we have just one generator!

// Initial case
func zero_proof(t: Rule...)->Rule{
  let ax0 = ADTm["nat"].a("+")[0]
  // s(0)+0 = s(0)
  return Proof.substitution(ax0, Variable(named: "x"), Nat.succ(x: Nat.zero()))
}

// Higher rank
 func succ_proof(t: Rule...)->Rule{
   let ax1 = ADTm["nat"].a("+")[1]
   // s(0) + s(y) = s(s(0) + y)
   let t2 = Proof.substitution(ax1, Variable(named: "x"), Nat.succ(x: Nat.zero()))
   // s(s(0) + x) = s(s(x))
   let t3 = Proof.substitutivity (Nat.succ, [t[0]])
   // s(0) + s(y) = s(s(y))
   return Proof.transitivity(t2, t3)
 }

4. Now we can call out our function to know if steps are good.

do {
  let teo = try Proof.inductive(conj, Variable(named: "x"), ADTm["nat"], [
    "zero": zero_proof,
    "succ": succ_proof
  ])
  print("Indcutive result: \(teo)")
}
// If the induction failed
catch ProofError.InductionFail {
  print("Induction failed!")
}

Great! Now you can see "true" if all are good!

Syntattic Sugar

LogicKit integration:

Syntax	Semantic
Term ∈ ADT.Type: Goal	Term in ADT
Term < ADT.Type: Goal	Term in ADT
Goal => Goal: Goal	Goal such that Goal
Term <-> Term: Goal	evalue(Term) equal to evalue(Term)

Mathematical operations:

Operation	Symbol	Supported types
sum	+	Nat, Integer
diffrence	-	Nat, Integer
multiply	*	Nat, Integer
divide	/	Nat, Integer
equal	==	All types
great	>	Nat, Integer
less	<	Nat, Integer
and	&&	Boolean
or	||	Boolean

Using LogicKit and the ADTm.geval() method is possible to evaluate simple logic expressions:

let x = Variable(named: "x")
let y = Variable(named: "y")

// x,y ∈ Nat => (x+y) < 9 && x<y
let goal = x ∈ Nat.self &&  y ∈ Nat.self => (x+y) <-> Nat.n(6) && (x<y) <-> Boolean.True()
// NOTE < can be used instead of ∈

for sol in solve(goal).prefix(3){ // NOTE .prefix(N) is used to stop the research of possible solution after N found
  let rsol = sol.reified()
  print(" x: \(ADTm.pprint(rsol[x]), y: \(ADTm.pprint(rsol[y]))")
}

Resulting in:

 x: 0, y: 6
 x: 1, y: 5
 x: 2, y: 4