Polynomial division

[strub]

No description provided.

[Boutry]

Hi PY,

Did you replace the lengthy set calls by sequences of rewrites?

[Boutry]

Also I might have some uncommitted proofs. I will check later today.

[strub]

@Boutry I changed nothing. I just pulled out the PolyDiv file from the finite fields branch so that we can eventually merge it. What do you mean by "lengthly sets calls"?

[fdupress]

I assume smt?

[Boutry]

I assume smt?

Indeed. Got auto"corrected". Is there something to measure the duration of set calls atm? Maybe I do not need to replace them all if only a few take too much time.

We should also try and merge the field extension development at some point. After the 29th I can start by rebasing it. There were only a few admits left I think.

https://github.com/EasyCrypt/easycrypt/blob/3787dc9536faa1460783c1470618a0b59d72b4de/theories/algebra/Perms.ec

[strub]

When the file compiles, we can start looking at smt calls :)

[strub]

And yes, the ultimate goal is to merge the finite field theory. However, I'd like to merge polydiv first.

[strub]

Going back to that. I don't think we need to pseudo-division (TL;DR we do crypto). I would like to prune that part and just to keep the division for k[x] for k a field. Moreover, a large of the results could be then directly imported for the GCD-domain theory.