FranckS / RingIdris

-- Franck Slama, Edwin Brady
-- University of St Andrews
-- File README
-- Brief description of what's in this repository
---------------------------------------------------

The current version of the hierarchy of provers is 0.6 (05/06/2016), and it works with Idris 0.11

I/ Summary :
---------------------------------------------------------------------

This is the implementation of a collection of tactics for Idris, in Idris. These tactics automatically prove equivalences between terms in algebraic structures, with universally quantified variables.

II/ News :
---------------------------------------------------------------------

New with version 0.6 : The collection of tactics compiles with Idris 0.11 (released on March 2016)
____________________

New with version 0.5 : The collection of tactics compiles with Idris 0.9.15.1, and various improvements
____________________

New with version 0.4 : Each prover can now deal with any equivalence relation, instead of just the propositional equality.
____________________


III/ Current state (05/06/2016) : 
---------------------------------------------------------------------

All the provers work, but the automatic reflection does not, because of some issues with Idris, that might be addressed in Idris 2.


IV/ How to load the tactics :
---------------------------------------------------------------------
Simply do :

idris main.idr -p contrib

That will load and typecheck the 7 tactics that are implemented at the moment + the tests (which includes instances of the corresponding typeclass) for each of them.

V/ How to use it :
---------------------------------------------------------------------

- The automatic reflection mechanism does not work due to some issues with the way reflection works in Idris. Therefore, you still have to encode by hand the two sides of the equality you wish to prove.

- You can have a look at the test files commutativeGroup_test.idr and group_test.idr (and the other test files) for some detailed examples.


VI/ A fairly big example
---------------------------------------------------------------------

A fairly big example can be found in the file binary.idr.
Simply run : 

idris ./PotentialApplications/binary.idr -p contrib

That will load the tactics and that will generate the proof required (in the term goal_aux).

To see the proof generated, simply ask for the evaluation of :

\l,c,bit0,bit1,x,x1,v,v1,known => goal_aux l c bit0 bit1 x x1 v v1 known

Note that because the automatic reflexion does not work, this file is terrible to read because of the encodings that are done by hand

VII/ About the technique :
---------------------------------------------------------------------

1) Note that we are interested in the proof of correctness (which is precisely the proof of equality/equivalence that we want) and not by the normalised terms, which are just a vector for building the required proofs.

2) We follow a "correct by construction" approach : rather than implementing the normalization of terms and afterwards proving that a normalized term and the original term denote the same value, we do it "bit by bit" : we construct this proof at the same time as we normalize the two terms.
The result if that the proof of correctness (which is in what we are interested) is a lot easier to obtain : for each little step of rewriting, the proof is really trivial.

3) We work by reflection in the langage itself (Idris), rather than implementing each tactic in the host language (Haskell). That's something nice, especially for a future bootstrapping of Idris.

4) Each prover uses the algebraic provers of the structures underneath : we avoid duplication between different levels as much as possible, which implies converting terms between different structures.
For instance, dealing with neutral elements (which appears for the first time at the Monoid level) is NOT re-implemented in the structures above (ie, Group, CommutativeGroup, etc). Instead, the Group prover converts the terms, and calls the Monoid prover. 
Some encodings had to be developped for doing some of these conversions (when we convert to a structure which is less expressive than the initial structure, as it is the case when converting from a ring to a commutative group, because the possibility to express products is lost).