16
$\begingroup$

Proof assistants like Coq have their own extensible syntax that's rather different from a general purpose language.

I'm curious whether there are any well-known proof assistants that are implemented as libraries in a general-purpose programming language such as Haskell or OCaml.

For example, using pseudocode.

proofEnvironment := NewProofEnvironment()
proofEnvironment.SetGoal("forall x . x = x")
proofEnvironment.ApplyTactic(...)
// Exports a proof of the targeted goal in some manner.
// For example as a metamath proof or another similar minimal format.
proofEnvironment.Export(...)
Improve this question
$\endgroup$
5
  • 7
    $\begingroup$ Perhaps something like HOL Light? Or, more broadly, any prover following the LCF philosophy with an extensible metalanguage implementation? $\endgroup$
    – Alex Nelson
    Commented Feb 8, 2022 at 18:23
  • $\begingroup$ To the user that voted to close this so far, why does this "need more focus"? It seems two users were already able to give fairly well-received answers. I'm voting to "leave open" until I'm convinced otherwise :) $\endgroup$
    – Nike Dattani
    Commented Feb 9, 2022 at 21:14
  • $\begingroup$ I updated the preamble to remove the bit about prover9, which is extraneous. Now it just talks about Coq, which isn't an internal DSL. $\endgroup$
    – Greg Nisbet
    Commented Feb 9, 2022 at 21:58
  • $\begingroup$ What about python bindings to an SMT solver? Would that count? $\endgroup$
    – Agnishom Chattopadhyay
    Commented Feb 10, 2022 at 1:32
  • $\begingroup$ Also, what about LiquidHaskell, would that count? $\endgroup$
    – Agnishom Chattopadhyay
    Commented Mar 2, 2022 at 15:57

4 Answers 4

Reset to default
15
$\begingroup$

As Alex Nelson pointed out, I think this is exactly the LCF approach to theorem proving. See The LCF Approach to Theorem Proving for details.

HOL-Light would certainly fit this description. You literally use HOL-Light inside OCaml. (Back when I coded in HOL-Light, I would code up my proof in an editor and paste it into an OCaml interpreter.) You can get a flavor by looking at the HOL Light code. For example, here is a theorem in HOL Light:

let ARITHMETIC_PROGRESSION_LEMMA = prove
 (`!n. nsum(0..n) (\i. a + d * i) = ((n + 1) * (2 * a + n * d)) DIV 2`,
  INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;

Here prove takes two arguments, the goal to prove, and a tactic to prove that statement (which is usually a number of tactics changed together with the THEN tactical), and it outputs a theorem. Tactics are just OCaml functions of type goal -> goalstate. (There is also some tooling in HOL-Light to make it more interactive, but that also is just an OCaml DSL used inside the OCaml REPL.)

If I am not mistaken, the ML family of languages were originally designed exactly to be the Meta Language for LCF provers to implement tactics. From Wikipedia:

Historically, ML was conceived to develop proof tactics in the LCF theorem prover (whose language, pplambda, a combination of the first-order predicate calculus and the simply-typed polymorphic lambda calculus, had ML as its metalanguage).

Improve this answer
$\endgroup$
1
  • $\begingroup$ Perhaps as an example, older Isabelle theory files were named using .ml extension--they were actually ML code. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Feb 10, 2022 at 2:08
14
$\begingroup$

If you are asking about a kind of embedding advanced proving facilities into modern System F$_\omega$-wannabe languages then I would suggest you to take a look onto Proving Ground base library for Scala by Siddhartha Gadgil:

https://github.com/siddhartha-gadgil/ProvingGround

You can read original presentaion by Siddhartha or take a Course on Stepik by Dmytro Mitin.

Here is short example:

Theorem proving
import provingground.
import HoTT.
import TLImplicits.
import shapeless.

val indN assoc = 
    NatInd.induc(n :-> (m ∼>: (k ∼>: (add(add(n)(m))(k)
    =:= add(n)(add(m)(k))))))

val hyp = "(n+m)+k=n+(m+k)" :: m ∼>: k ∼>: (add(add(n)(m))(k) 
          =:= add(n)(add(m)(k)))

val assoc = indN assoc(m :∼> (k :∼> add(m)(k).refl))
    (n :∼> (hyp :-> (m :∼> (k :∼> 
         IdentityTyp.extnslty(succ)(add(add(n)(m))(k))
          (add(n)(add(m)(k))) (hyp(m)(k))))))

 assoc !: n ∼>: m ∼>: k ∼>: (add(add(n)(m))(k) =:= add(n)(add(m)(k)))

But beware Scala type systems and deal with them accurately, here is fine as we have HOL-like string internalization.

Improve this answer
$\endgroup$
11
$\begingroup$

I can't speak to how well-known it is, but holpy[1] is a fairly recent library that implements higher order logic in Python. The main selling points they describe in the arXiv paper are a "point and click" user interface, a JSON-like format implementing theories, and numerous macros that can be applied for "producing, checking, and storing proofs".

References:

  1. Bouhua Zhan, HolPy: Interactive Theorem Proving in Python. (accessed February 8, 2022)
Improve this answer
$\endgroup$
5
$\begingroup$

This is indeed the LCF approach, and is how the various HOL systems operate to this day. Typically, the systems do augment or fiddle with their underlying programming language implementations. For example, HOL Light fiddles with OCaml's lexical syntax to make the language look more like Classic (i.e., pre-SML) ML. HOL4 extends Poly/ML at the lexing level to support pretty multi-line quotation-syntax (SML string literals can only extend over multiple source-level lines through the use of trailing backslash characters) and some other tricks.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.