Description

Telegram bot for proof assistants.

Description

hackage.haskell.org

Bridge between Telegram Bot and several proof assistants.

Currently following proof assistant supported: Agda, Arend, Coq, Idris 2, Lean, Rzk

See README.md for more details.

README.md

hackage.haskell.org

Proof Assistant Bot

Description
Installation
1. Coq
2. Agda
3. Idris 2
4. Lean
5. Arend
6. Rzk
7. Alloy
Usage
Available instances
Acknowledgements

Description

This bot provides limited Telegram interfaces to following proof assistant programs (in order of implementation):

Coq
Agda
Idris 2
Lean
Arend
Rzk

Installation

Bot could be built via following commands:

cabal update
cabal build
cabal install --overwrite-policy=always

To launch bot you need to set environmental variables, see ./config/settings.dhall for more details.

One of them is PROOF_ASSISTANT_BOT_TOKEN. Obtain it via @BotFather and set it:

export PROOF_ASSISTANT_BOT_TOKEN="..."

Another environmental variable that unfortunately needed is NIX_PROFILE. Please add it as

export NIX_PROFILE="$HOME/.nix-profile"

Coq

Install opam >= 2.1.0, e.g. from here.

cd $HOME
opam --version
2.1.3

Install Coq.

cd $HOME
opam init
eval $(opam env)
opam pin add coq 8.16.1

Locate coqtop and set enviromental variable. Should be similar to:

export COQ_BIN_PATH="$HOME/.opam/default/bin/coqtop"

Agda

We do not need to worry about Agda since it is included in package dependencies. It will be installed automatically. Meantime, Agda standard library should be installed manually.

Get agda-stdlib from Github.
Unpack archive.

mkdir -p $PROOF_ASSISTANT_BOT_DIR/agda
cp agda-stdlib-1.7.1.tar.gz $PROOF_ASSISTANT_BOT_DIR/agda
cd $PROOF_ASSISTANT_BOT_DIR/agda
tar -xzvf agda-stdlib-1.7.1.tar.gz
export AGDA_STDLIB_PATH=$PROOF_ASSISTANT_BOT_DIR/agda/agda-stdlib-1.7.1

Create file $HOME/.agda/defaults with following content:

standard-library

Create file $HOME/.agda/libraries with following content:

$AGDA_STDLIB_PATH/standard-library.agda-lib

Idris 2

Get nix from nixos.org.
Install idris2 via nix:

nix-env -i idris2

Set environmental variable:

export IDRIS2_BIN_PATH="$HOME/.nix-profile/bin/idris2"

Lean

Get nix from nixos.org.
Install lean via nix:

nix-env -i lean

Install leanproject via nix:

nix-env -i mathlibtools

Run leanproject new lean.
Set LEAN_BIN_PATH environmental variable:

export LEAN_BIN_PATH="$HOME/.nix-profile/bin/lean"

Set LEAN_PROJECT_PATH to the newly created project directory.

Arend

Get nix from nixos.org.
Get java and openjdk17 via nix:

nix-env -i openjdk-17.0.4+8

Set JAVA_HOME environment variable to your openjdk location. You can use readlink $HOME/.nix-profile/bin/java and strip /bin/java from the end.
Create project directory to store arend projects (for different Telegram chats) and set AREND_ROOT_PROJECT_DIR.
Get Arend standard library from the official site and store in ${AREND_ROOT_PROJECT_DIR}/libs.
Point AREND_STDLIB_PATH environment variable to the same location as AREND_ROOT_PROJECT_DIR.
Download Arend.jar and set AREND_PATH environment variable to its location, e.g.

export AREND_PATH="${AREND_ROOT_PROJECT_DIR}/Arend.jar"

Rzk

No actions required. See cabal.project for more details.

Alloy 6 / Alloy CLI Wrapper

You can read about CLI Wrapper here: https://github.com/AlloyTools/org.alloytools.alloy/issues/211

Get nix from nixos.org.
Get java and openjdk17 via nix:

nix-env -i openjdk-17.0.4+8

Set JAVA_HOME environment variable to your openjdk location. You can use readlink $HOME/.nix-profile/bin/java and strip /bin/java from the end.
Get alloy6 via nix:

nix-env -i alloy6

Create project directory to store Alloy projects (for different telegram chats) and set ALLOY_PROJECT_DIR.
Create directory for Alloy CLI wrapper and prepare Alloy CLI Wrapper:

mkdir -p $ALLOY_PROJECT_DIR/bin
cd $ALLOY_PROJECT_DIR
# Download Alloy CLI Wrapper
curl https://gist.githubusercontent.com/swamp-agr/560f0d9bf8dc034f99d6055a5a197285/raw/5b547616063ba834bfa2987bc1eb539f1ec8088d/Main.java > bin/Main.java
javac -cp "$NIX_PROFILE/share/alloy/*" -Xlint:all bin/Main.java
# Test: should be empty output and exit code 0
java -cp $NIX_PROFILE/share/alloy/alloy6.jar:$ALLOY_PROJECT_DIR/bin Main

Set up graphviz and imagemagick for generating plots based on Alloy CLI Wrapper output:

nix-env -i graphviz imagemagick

Set ALLOY_PATH environment variable to $NIX_PROFILE/share/alloy/alloy6.jar.

Usage

Coq supports only typecheck of the user input via /coq command. Example:

/coq Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.

Compute (next_weekday friday).

Compute (next_weekday (next_weekday saturday)).

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.

Proof. simpl. reflexivity. Qed.

Agda is available via /agda command. Bot supports several subcommands for Agda:

/agda /load <input>. E.g.

/agda /load import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    5
  ∎

/agda /reload
/agda /typeOf <expr>. E.g. /agda /typeOf suc.
/agda <expr>. E.g. /agda suc zero + suc zero.

Idris 2 via /idris2 command. Bot supports several subcommands for Idris 2:

/idris2 /load <input>. E.g.

/idris2 /load module Main

import System.File.ReadWrite

tryPrint : Either FileError String -> IO ()
tryPrint (Left _) = putStrLn "error"
tryPrint (Right r) = putStrLn r

main : IO ()
main = do c <- readFile "hello.idr"
          tryPrint c

/idris2 /typeOf <expr>. E.g. /idris2 /typeOf Nat.
/idris2 <expr>. E.g. /idris2 2 + 3.

Lean is available via /lean command. Typecheck supported for the user input. Only several modes were tested (calc mode, conv mode, simplifier).

Example 1:

/lean import data.nat.basic

variables (a b c d e : ℕ)
variable h1 : a = b
variable h2 : b = c + 1
variable h3 : c = d
variable h4 : e = 1 + d

theorem T : a = e :=
calc
  a     = b      : h1
    ... = c + 1  : h2
    ... = d + 1  : congr_arg _ h3
    ... = 1 + d  : add_comm d (1 : ℕ)
    ... =  e     : eq.symm h4

Example 2:

/lean import topology.basic

#check topological_space

Example 3:

/lean import algebra.group.defs

variables (G : Type) [group G] (a b c : G)

example : a * a⁻¹ * 1 * b = b * c * c⁻¹ :=
begin
  simp
end

Arend is available via /arend command. Only typecheck supported.
- Example:
```
/arend \func f => 0
```

Rzk is available via /rzk command. Typechecker supported for every language.

Example:

/rzk  #lang rzk-1

#def prod : (A : U) -> (B : U) -> U
  := \A -> \B -> ∑ (x : A), B

#def isweq : (A : U) -> (B : U) -> (f : (_ : A) -> B) -> U
  := \A -> \B -> \f ->
        ∑ (g : (_ : B) -> A),
          prod ((x : A) -> g (f x) =_{A} x)
               ((y : B) -> f (g y) =_{B} y)

#def weq : (A : U) -> (B : U) -> U
  := \A -> \B -> ∑ (f : (_ : A) -> B), isweq A B f

#def Theorem-4.1
  : (I : CUBE)
  -> (psi : (t : I) -> TOPE)
  -> (phi : {(t : I) | psi t} -> TOPE)
  -> (X : U)
  -> (Y : <{t : I | psi t} -> (x : X) -> U >)
  -> (f : <{t : I | phi t} -> (x : X) -> Y t x >)
  -> weq <{t : I | psi t} -> (x : X)          -> Y t x [phi t |-> f t]>
         ((x : X)         -> <{t : I | psi t} -> Y t x [phi t |-> f t x]>)
  := \I -> \psi -> \phi -> \X -> \Y -> \f ->
    (\k -> \x -> \t -> k t x,
      (\k -> \{t : I | psi t} -> \x -> (k x) t,
        (\k -> refl_{k}, \k -> refl_{k})))

#def Theorem-4.2_uncurry_ext
  : (I : CUBE)
  -> (J : CUBE)
  -> (psi : (t : I) -> TOPE)
  -> (zeta : (s : J) -> TOPE)
  -> (X : <{t : I | psi t} -> <{s : J | zeta s} -> U> >)
  -> (chi : {(t : I) | psi t} -> TOPE)
  -> (phi : {(s : J) | zeta s} -> TOPE)
  -> (f : <{(t, s) : I * J | psi t /\ zeta s} -> X t s >)
  -> (_ : <{t : I | psi t}
            -> <{s : J | zeta s}
                 -> X t s [chi s |-> f (t, s)]>
               [phi t |-> \s -> f (t, s)]>)
  -> <{(t, s) : I * J | psi t /\ zeta s}
        -> X t s [(phi t /\ zeta s) \/ (psi t /\ chi s) |-> f (t, s)]>
  := \I -> \J -> \psi -> \zeta -> \X -> \chi -> \phi -> \f ->
    \k -> \(t, s) -> k t s

Alloy is available via /alloy command.

Example:

/alloy open util/ordering[Id]

sig Node {
 id : one Id,
 succ : one Node,
 var inbox : set Id,
 var outbox : set Id
} 

sig Id {}

fact ring {
 all i : Id | lone id.i
 all n : Node | Node in n.^succ
}

var sig elected in Node {}

fact elected {
 always {
  elected = {n : Node | once (n.id in n.inbox)}
 }
}

enum Event { Send, Compute }

pred send [n : Node] {
 some i : n.outbox {
  n.outbox' = n.outbox - i
  n.succ.inbox' = n.succ.inbox + i
 }
 all m : Node - n.succ | m.inbox' = m.inbox
 all m : Node - n | m.outbox' = m.outbox
}

fun send : Event -> Node {
 Send -> { n : Node | send[n] }
}

pred compute [n : Node] {
 some i : n.inbox {
  n.inbox' = n.inbox - i
  n.outbox' = n.outbox + (i - n.id.*(~next))
 }
 all m : Node - n | m.inbox' = m.inbox
 all m : Node - n | m.outbox' = m.outbox
}

fun compute : Event -> Node {
 Compute -> { n : Node | compute[n] }
}

fun events : set Event {
 (send+compute).Node
}

pred skip {
 inbox' = inbox
 outbox' = outbox
}

fact init {
 no inbox
 outbox = id
}

fact behaviour {
 always (skip or some n : Node | send[n] or compute[n])
}


run {} for 4 but exactly 4 Node, 10 steps
run example {eventually some elected} for 3 but exactly 3 Node, 6 steps

assert safety {
 always lone elected
}
check safety for 3 but 15 steps


pred sendEnabled [n : Node] {
 some n.outbox
}

pred computeEnabled [n : Node] {
 some n.inbox
}

pred fairness {
 always (all n : Node | (always sendEnabled[n] implies eventually send[n]))
 always (all n : Node | (always computeEnabled[n] implies eventually compute[n]))
}

assert liveness {
 fairness and some Node implies eventually some elected
}
check liveness for 3

As result you can see:

Alloy temporal model instance with two different states

Available instances

@ProofBot (online)
@ProofDebugBot (for debug purpose, offline most of the time)

Acknowledgements

PLTT Community
Nikolay Kudasov
Andrey Borzenkov
Matúš Tejiščák
My wife.

proof-assistant-bot

Proof Assistant Bot

Description

Installation

Coq

Agda

Idris 2

Lean

Arend

Rzk

Alloy 6 / Alloy CLI Wrapper

Usage

Available instances

Acknowledgements

Version

License

Status

Source

Homepage

Platforms (75)

Proof Assistant Bot

Description

Installation

Coq

Agda

Idris 2

Lean

Arend

Rzk

Alloy 6 / Alloy CLI Wrapper

Usage

Available instances

Acknowledgements

Version

License

Status

Source

Homepage

Platforms75 (75)

Platforms (75)