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