The Interactive Theorem Prover — Idris 1.0 documentation

# The Interactive Theorem Prover

This short guide contributed by a community member illustrates how to prove associativity of addition on `Nat` using the interactive theorem prover.

First we define a module `Foo.idr`

    module Foo

    plusAssoc : plus n (plus m o) = plus (plus n m) o
    plusAssoc = ?rhs

We wish to perform induction on `n`. First we load the file into the Idris `REPL` as follows:

    $ idris Foo.idr

We will be given the following prompt, in future releases the version string will differ:

         ____    __     _
        /  _/___/ /____(_)____
        / // __  / ___/ / ___/     Version 0.9.18.1
      _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
     /___/\__,_/_/  /_/____/       Type :? for help

    Idris is free software with ABSOLUTELY NO WARRANTY.
    For details type :warranty.
    Type checking ./Foo.idr
    Metavariables: Foo.rhs
    *Foo>

## Explore the Context

We start the interactive session by asking Idris to prove the hole `rhs` using the command `:p rhs`. Idris by default will show us the initial context. This looks as follows:

    *Foo> :p rhs
    ----------                 Goal:                  ----------
    { hole 0 }:
     (n : Nat) ->
     (m : Nat) ->
     (o : Nat) ->
     plus n (plus m o) = plus (plus n m) o

## Application of Intros

We first apply the `intros` tactic:

    -Foo.rhs> intros
    ----------              Other goals:              ----------
    { hole 2 }
    { hole 1 }
    { hole 0 }
    ----------              Assumptions:              ----------
     n : Nat
     m : Nat
     o : Nat
    ----------                 Goal:                  ----------
    { hole 3 }:
     plus n (plus m o) = plus (plus n m) o

## Induction on `n`

Then apply `induction` on to `n`:

    -Foo.rhs> induction n
    ----------              Other goals:              ----------
    elim_S0
    { hole 2 }
    { hole 1 }
    { hole 0 }
    ----------              Assumptions:              ----------
     n : Nat
     m : Nat
     o : Nat
    ----------                 Goal:                  ----------
    elim_Z0:
     plus Z (plus m o) = plus (plus Z m) o

## Compute

    -Foo.rhs> compute
    ----------              Other goals:              ----------
    elim_S0
    { hole 2 }
    { hole 1 }
    { hole 0 }
    ----------              Assumptions:              ----------
     n : Nat
     m : Nat
     o : Nat
    ----------                 Goal:                  ----------
    elim_Z0:
     plus m o = plus m o

## Trivial

    -Foo.rhs> trivial
    ----------              Other goals:              ----------
    { hole 2 }
    { hole 1 }
    { hole 0 }
    ----------              Assumptions:              ----------
     n : Nat
     m : Nat
     o : Nat
    ----------                 Goal:                  ----------
    elim_S0:
     (n__0 : Nat) ->
     (plus n__0 (plus m o) = plus (plus n__0 m) o) ->
     plus (S n__0) (plus m o) = plus (plus (S n__0) m) o

## Intros

    -Foo.rhs> intros
    ----------              Other goals:              ----------
    { hole 4 }
    elim_S0
    { hole 2 }
    { hole 1 }
    { hole 0 }
    ----------              Assumptions:              ----------
     n : Nat
     m : Nat
     o : Nat
     n__0 : Nat
     ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
    ----------                 Goal:                  ----------
    { hole 5 }:
     plus (S n__0) (plus m o) = plus (plus (S n__0) m) o

## Compute

    -Foo.rhs> compute
    ----------              Other goals:              ----------
    { hole 4 }
    elim_S0
    { hole 2 }
    { hole 1 }
    { hole 0 }
    ----------              Assumptions:              ----------
     n : Nat
     m : Nat
     o : Nat
     n__0 : Nat
     ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
    ----------                 Goal:                  ----------
    { hole 5 }:
     S (plus n__0 (plus m o)) = S (plus (plus n__0 m) o)

## Rewrite

    -Foo.rhs> rewrite ihn__0
    ----------              Other goals:              ----------
    { hole 5 }
    { hole 4 }
    elim_S0
    { hole 2 }
    { hole 1 }
    { hole 0 }
    ----------              Assumptions:              ----------
     n : Nat
     m : Nat
     o : Nat
     n__0 : Nat
     ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
    ----------                 Goal:                  ----------
    { hole 6 }:
     S (plus n__0 (plus m o)) = S (plus n__0 (plus m o))

## Trivial

    -Foo.rhs> trivial
    rhs: No more goals.
    -Foo.rhs> qed
    Proof completed!
    Foo.rhs = proof
      intros
      induction n
      compute
      trivial
      intros
      compute
      rewrite ihn__0
      trivial

Two goals were created: one for `Z` and one for `S`. Here we have proven associativity, and assembled a tactic based proof script. This proof script can be added to `Foo.idr`.