Port Coq code to use 'done' tactic instead of 'easy' and benchmark

[ndcroos]

See https://github.com/coq-community/math-classes/issues/128 See also this discussion: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Error.20in.20MathClasses.2C.20adding.20an.20import

Todo's:

• benchmarking
• hide fast_done

[palmskog]

@ndcroos the fast_done and done tactics are as far as I know independent of the rest of stdpp. So why do you need to bundle base.v? This is a big file with lots of choices in how to configure Coq, that will take quite a lot of time to maintain inside this project.

[ndcroos]

@palmskog I need base.v for not_symmetry. I still need to delete code in (mostly) base.v that is not needed.

[ndcroos]

I got a lot of errors executing make that are due to easy --> done changes, so I think it is makes more sense to revert all the easy --> done changes, and then doing them again one by one, while making sure that the project compiles. I also moved stdpp_tactics.v to the misc directory.

(It seems like perhaps the most straightforward changes are those were easy is the last step in the proof. But I am not sure of this.)

[ndcroos]

Files where replacing 'easy' didn't work:

• theory/series
• implementations/dyadics.v
• misc/util.v (because of circular dependency)

[spitters]

Thanks @ndcroos ! What's the status of this?

[ndcroos]

@spitters I only need to do the benchmarking, using make pretty-timed, but I have not figured out yet how to execute the benchmark for the made changes. Help with this is very welcome here.