Sylph 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 @>