Ring/field tactics available as soon as an instance is found

[Boutry]

No description provided.

[strub]

The diff. seems a bit polluted by whitespaces removal. Is this done on purpose?

[Boutry]

The diff. seems a bit polluted by whitespaces removal. Is this done on purpose?

I just removed them when I saw them. Should I undo it?

[strub]

That makes the diff. hard to read. I agree that we should remove the trailing spaces, but we should do this in a dedicated PR and create a CI target that rejects future PR that reintroduce trailing spaces.

[Boutry]

That makes the diff. hard to read. I agree that we should remove the trailing spaces, but we should do this in a dedicated PR and create a CI target that rejects future PR that reintroduce trailing spaces.

I opened an issue (#359) for it. I assume that for this one it is ok.

[strub]

I am sorry, but I do not understand the PR. Why is it ok to remove the check that the required theories are loaded before using ring / field and why some proofs are now more complex (e.g. a chain of tactic instead of simply calling ring)?

[Boutry]

Writing down some elements before our discussion on Tuesday. I believe that the ring / field theories are not necessary to be loaded to use the ring / field tactics. Indeed, we already check that algtactic is loaded (

easycrypt/src/ecAlgTactic.ml

Line 13 in 1c34624

let tmod = EcPath.fromqsymbol ([EcCoreLib.i_top; "AlgTactic"], "Requires")

) which I believe to be enough as it contains the list of necessary properties to be able to use the tactics. Moreover while I think it is not necessary to check that these theories are loaded, it also prevents from loading the algtactic file inside the ring file. This matters because it makes it impossible to show, inside the ring file, that these theories are sufficient to be able to use the ring / field tactics. That's precisely what I do in the ring file: I show that they are instances of the supposedly associated algtactic theories. This makes it so that, when declaring a ring / field, we already have access to the tactics.

To address why some (just the proof that BitWord is an instance of a ring) proof are now more complex, there is a simple explanation. I removed the proof that they form an instance of an algtactic as it will come for free from showing it is an instance of a BoolRing. Thus, I do not have access to the ring tactic when showing that it is a BoolRing.