To start the our theorem prover for intuitionistic HOL under the system ELPI, do the following:
1) uncompress elpi-LFMTP16.tar.gz in my_folder
2) change the directory to my_folder/elpi
3) $make
4) $./elpi bench/sources/hollight/elpi-hol-light.mod
If you see:
loading /home/dell/lpcic/elpi/pervasives.elpi
loading bench/sources/hollight/hollight_safe.mod
goal>
then the elpi-hol-light.mod is loaded in the ELPI interpreter.
5) go.
This enters in the theorem prover. Once the theorems in the
elpi-hol-light.mod are proved, the theorem prover prints:
"Welcome to HOL extra-light"
"Enter a command or "stop.""
which means that it is ready for work.
Below we provide an example in interactive mode. We would like to
prove the statement:
(forall x) (x -> ((x = x) /\ x))
, where '->' is an implication and '/\' is a conjunction.
In the shell we proceed as follows:
"Enter a command or "stop.""
theorem my_theorem (! x \ x ==> ((x = x) && x)).
"|------------------"
! x19 \ x19 ==> (x19 <=> x19) && x19
forall_i.
"|------------------"
x19 ==> (x19 <=> x19) && x19
i.
x19
"|------------------"
(x19 <=> x19) && x19
conj.
x19
"|------------------"
x19
x19
"|------------------"
x19 <=> x19
r.
x19
"|------------------"
x19
h.
"proof completed"
theorem my_theorem
((! x19 \ x19 ==> x19 && x19) ,
[then forall_i (bind prop x19 \ then i (then conj h))])
[] my_theorem ":" ! x19 \ x19 ==> x19 && x19
As soon as the theorem is proved, its certificate is printed as well. The tactical 'then' has the usual meaning as in HOL.