Proof Assistant Bot

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

1. Bot could be built via following commands:

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

2. 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

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

cd $HOME
opam --version
2.1.3

2. Install Coq.

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

3. 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.

1. Get agda-stdlib from Github.

2. 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

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

standard-library

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

$AGDA_STDLIB_PATH/standard-library.agda-lib

Idris 2

1. Get nix from nixos.org.

2. Install idris2 via nix:

nix-env -i idris2

3. Set environmental variable:

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

Lean

1. Get nix from nixos.org.

2. Install lean via nix:

nix-env -i lean

3. Install leanproject via nix:

nix-env -i mathlibtools

4. Run leanproject new lean.

5. Set LEAN_BIN_PATH environmental variable:

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

6. Set LEAN_PROJECT_PATH to the newly created project directory.

Arend

1. Get nix from nixos.org.

2. Get java and openjdk17 via nix:

nix-env -i openjdk-17.0.4+8

3. 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.

4. Create project directory to store arend projects (for different Telegram chats) and set AREND_ROOT_PROJECT_DIR.

5. Get Arend standard library from the official site and store in ${AREND_ROOT_PROJECT_DIR}/libs.

6. Point AREND_STDLIB_PATH environment variable to the same location as AREND_ROOT_PROJECT_DIR.

7. 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

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

Acknowledgements

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