@hackage proof-assistant-bot0.2.0

Telegram bot for proof assistants

Categories
License
MIT
Maintainer
persiantiger@yandex.ru
Links
- Homepage
- Documentation
- No source repository
- Changelog
Versions
- 0.2.2 Wed, 7 Feb 2024
- 0.2.1 Tue, 7 Feb 2023
- 0.2.0 Sat, 10 Dec 2022

Installation
In your cabal file:
Dependencies (15)
- base <4.17
- bytestring
- directory
- filepath
- mtl
- process
Dependents (0)

Proof Assistant Bot

Description
Installation
1. Coq
2. Agda
3. Idris 2
4. Lean
5. Arend
6. Rzk
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="..."

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.

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

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

@hackage proof-assistant-bot0.2.0

Categories

License

Maintainer

Links

Versions

Installation

Dependencies (15)

Dependents (0)

Proof Assistant Bot

Description

Installation

Coq

Agda

Idris 2

Lean

Arend

Rzk

Usage

Available instances

Acknowledgements