 Sylph 0.2.3

There is a newer version of this package available.
See the version list below for details.
Install-Package Sylph -Version 0.2.3
dotnet add package Sylph --version 0.2.3
<PackageReference Include="Sylph" Version="0.2.3" />
For projects that support PackageReference, copy this XML node into the project file to reference the package.
#r "nuget: Sylph, 0.2.3"
#r directive can be used in F# Interactive, C# scripting and .NET Interactive. Copy this into the interactive tool or source code of the script to reference the package.
// Install Sylph as a Cake Addin

// Install Sylph as a Cake Tool
#tool nuget:?package=Sylph&version=0.2.3

Sylph

Sylph (symbolic proof helper) is a language-integrated proof assistant for F#.

open Sylvester
open IntegerAlgebra

// Declare some integer variables for use in formulae
let a,b,c = var3<int>

// Prove the identity a * 0 = 0 use the rules and axioms of integer algebra
let p1 = proof <@ a * 0 = 0 @> integer_algebra [
// a * 0 = a * 0 + 0 is axiomatic in the integer_algebra theory.
let lemma1 = <@ a * 0 = a * 0 + 0 @> |> int_id_ax

// 0 = -(a * 0 ) + (a * 0) can be proved in the integer_algebra theory.
let lemma2 = <@ 0 = -(a * 0) + (a * 0) @> |> int_id [Commute |> EntireB]

// Substitute the identity in lemma1 into A
lemma1 |> EntireA

// A is commutative
Commute |> EntireA
// Subsititute the identity in lemma2 into the left of A
lemma2 |> LeftA
// Subsititute the identity in lemma2 into B
lemma2 |> EntireB
RightAssoc |> EntireA
LeftCancel |> AB
Collect |> EntireA
Reduce |> EntireA
]
[Lemma] Proof of A: a ⋅ 0 ≡ B: a ⋅ 0 + 0:
[Lemma] ⊢ a ⋅ 0 ≡ a ⋅ 0 + 0. [Axiom of Identity]
[Lemma] Proof complete.

[Lemma] Proof of A: 0 ≡ B: -(a ⋅ 0) + a ⋅ 0:
[Lemma] 1. B is commutative: -(a ⋅ 0) + a ⋅ 0 ≡ a ⋅ 0 + -(a ⋅ 0).
[Lemma] ⊢ 0 ≡ a ⋅ 0 + -(a ⋅ 0). [Definition of Inverse]
[Lemma] Proof complete.

Proof of A: a ⋅ 0 ≡ B: 0:
1. Substitute a ⋅ 0 in A with a ⋅ 0 + 0.
Proof incomplete. Current state: a ⋅ 0 + 0 ≡ 0.
2. A is commutative: a ⋅ 0 + 0 ≡ 0 + a ⋅ 0.
Proof incomplete. Current state: 0 + a ⋅ 0 ≡ 0.
3. Substitute 0 in A with -(a ⋅ 0) + a ⋅ 0.
Proof incomplete. Current state: -(a ⋅ 0) + a ⋅ 0 + a ⋅ 0 ≡ 0.
4. Substitute 0 in A with -(a ⋅ 0) + a ⋅ 0.
Proof incomplete. Current state: -(a ⋅ 0) + a ⋅ 0 + a ⋅ 0 ≡ -(a ⋅ 0) + a ⋅ 0.
5. A is right-associative: -(a ⋅ 0) + a ⋅ 0 + a ⋅ 0 ≡ -(a ⋅ 0) + (a ⋅ 0 + a ⋅ 0).
Proof incomplete. Current state: -(a ⋅ 0) + (a ⋅ 0 + a ⋅ 0) ≡ -(a ⋅ 0) + a ⋅ 0.
6. Cancel equivalent terms on the LHS in A and B: (-(a ⋅ 0) + (a ⋅ 0 + a ⋅ 0), -(a ⋅ 0) + a ⋅ 0) ≡ (a ⋅ 0 + a ⋅ 0, a ⋅ 0).
Proof incomplete. Current state: a ⋅ 0 + a ⋅ 0 ≡ a ⋅ 0.
7. Collect multiplication terms distributed over addition in A: a ⋅ 0 + a ⋅ 0 ≡ a ⋅ (0 + 0).
Proof incomplete. Current state: a ⋅ (0 + 0) ≡ a ⋅ 0.
8. Reduce integer constants in A: a ⋅ (0 + 0) ≡ a ⋅ 0.
⊢ a ⋅ 0 ≡ a ⋅ 0. [Logical Axiom of Equality]
Proof complete.

Unlike other theorem provers Sylph does not require an external DSL or parser for expressing theorem statements, or an external interactive environment for creating and storing the state of proofs. Theorems are expressed as the equivalence of 2 formulas and a formula is defined as any F# expression of a particular type for which a code quotation and full expression tree is available. Formulas in a theorem do not have to be logical formulas but any 2 valid F# expressions of the same type where it makes sense to reason about them equationally.

// Define a formula of interest using an ordinary function with the Formula attribute
[<Formula>]
let f1 x = 3 * x + 6 + 2 * x + 4

// Or use an expression directly
let f2 = <@ a * a + 6 * b + 5@>
// Each formula has a symbolic expression
expand <@ f1 @>

Lambda (x, Call (None, op_Addition, [Call (None, op_Addition, [Call (None, op_Addition, [Call (None, op_Multiply, [Value (3), x]), Value (6)]), Call (None, op_Multiply, [Value (2), x])]), Value (4)]))

// And can also be decompiled to the F# source
src f2
a * a + 6 * b + 5

Proofs are constructed according to the axioms and rules of theories which define the rules that can be used to match and transform formula expressions that preserve equivalence.

//Some theorems are true axiomatically
integer_algebra |- <@ (a + b) = (b + a) @>
True
//Provable directly from axioms
let t2 = ident <@ a + b + c = a + (b + c)@> integer_algebra []
Proof of A: a + b + c ≡ B: a + (b + c):
⊢ a + b + c ≡ a + (b + c). [Axiom of Associativity]
Proof complete.

Axioms are pure functions or schemas that match patterns in primitive unary and binary formulas, which define a set of formulae that are always equivalent in a theory e.g an identity axiom for a theory is defined as:

/// x + 0 == x
let (|Identity|_|) (op: Expr<'t->'t->'t>) (zero:Expr<'t>)   =
function
| Binary op (a1, z), a2 when sequal a1 a2 && sequal zero z -> Some (pattern_desc "Identity" <@ fun (x:'t) -> (%op) x (%zero) = (%zero) @>)
| _ -> None
// True by the addition identity axiom
integer_algebra |- <@ c + a + 0 = c + a @>

NuGet packages (1)

Showing the top 1 NuGet packages that depend on Sylph:

Sylvester.AbstractAlgebra

F# Library for defining, exploring and proving concepts in abstract algebra.

GitHub repositories

This package is not used by any popular GitHub repositories.