mono and ac_mono in the nursery

Stream: general

[Simon Hudon]

My mono and ac_mono are, I believe, ready for use. I have put them in the nursery https://github.com/leanprover-community/mathlib-nursery so that people can try them out as I get them merged into mathlib.

[Patrick Massot]

Why is there so much meta and lemmas in the test file? Is it meant to be part of mathlib?

[Simon Hudon]

It is. It's meant to test individual parts of the tactics. Maybe I should split it into test and example

[Patrick Massot]

I see

[Patrick Massot]

I always find it hard to read your examples or tests which actually don't prove anything, either because the announced statement is true or because it ends with admit

[Patrick Massot]

Where is monotonicity when the target is an equality as in https://github.com/leanprover-community/mathlib-nursery/blob/master/test/tactic/monotonicity.lean#L326?

[Simon Hudon]

In that case, monotonicity is a generalization of congr

[Patrick Massot]

Maybe you could explain that in the documentation (and add a couple of example there too)

[Patrick Massot]

It looks very useful

[Simon Hudon]

I see what you mean with true. I state those theorems using suffices : x * y < w * z, trivial, just so that I don't have to complete all the proofs. I could use assumptions instead of guard_target maybe , that would be clearer

[Simon Hudon]

Thanks for the advice, I'll try to select the ones that illustrate best the obvious use cases

[Simon Hudon]

It looks very useful

I'm hoping it will be. Please report any trouble you run across, I feel like I must have overlooked lots of cases and lots of lemmas.

[Patrick Massot]

Unfortunately I don't think any of my current projects will need this, but certainly I will need it at some point.