[Merged by Bors] - feat(logic/nontrivial): a tactic to summon nontrivial instances

[semorrison]

Given a goal `a = b` or `a ≤ b` in a type `α`, generates an additional hypothesis `nontrivial α`
(as otherwise `α` is a subsingleton and the goal is trivial).

Alternatively, given a hypothesis `a ≠ b` or `a < b` in a type `α`, tries to generate a `nontrivial α`
hypothesis from existing hypotheses using `nontrivial_of_ne` and `nontrivial_of_lt`.

---

[semorrison]

@robertylewis I really struggled to come up with meaningful context-free examples to put in the doc-string. In order for this tactic to be useful, you need a "consumer" of the nontrivial instance available, and these are all a bit too interesting to put in a small example.

I added a test file, and used the tactic in an additional place in the library, in the hope that these are helpful for understanding the tactic.

I could just add the examples from the test file to the doc-string, but they are pretty lame.

[semorrison]

On the previous branch Gabriel had suggested deleting these two lines.

If I do this, we don't know which type to look for an instance of nontrivial for. It would be plausible to just look for any, by using a placeholder, but I'd worry about finding the wrong one.

[robertylewis]

Well, this failure message will never display in notriviality. Not sure if that's what Gabriel was pointing out.

You can get t more cleanly with `(@ne %%t _ _) ← target

[semorrison]

Is there a way to get t without using infer_type when I need to consider two possibilities ≠ and <? I can't get around using <|>.

Is (do `(@ne %%t _ _) ← target, return t) any better than (do `(%%a ≠ %%b) ← target, infer_type a)?

[robertylewis]

You can do something like

guardb $ e.is_app_of `ne || e.is_app_of `has_le.le,
return $ e.get_app_args.head

but looking at this again, would it be better to unify with ne or lt instead of checking syntactically, to capture ¬ a = b, >, etc?

Is (do `(@ne %%t _ _) ← target, return t) any better than (do `(%%a ≠ %%b) ← target, infer_type a)?

It's not a particularly big deal but it seems better to avoid a call to infer_type when the type info is already in the term.

[gebner]

For the record, what I wanted to say is that the tactic shouldn't be limited to = and ≤ goals. Maybe it should take an optional argument, like the inhabit tactic? That is, nontriviality α?

[semorrison]

Okay, I've switched to using unify.

I'm not entirely sure what the behaviour should be for other goals (besides = and ≤). Are we going to branch into cases and create a goal with a subsingleton hypothesis as well?

[robertylewis]

There's nothing special about the goal in the ne/lt case, is there? It just uses the goal to pick a type and then tries to prove nontriviality using hypotheses. nontriviality_by_assumption wouldn't need to be restricted to certain goals if it knew what type to look for.

I agree with Gabriel that the optional argument makes sense. If it's provided and the goal is eq/le and the types match, ignore it. If it's provided otherwise, do nontriviality_by_assumption except skip the first line. Otherwise do what you do now.

[semorrison]

Okay, I've revised the tactic, so it now takes an optional type argument.

[robertylewis]

I'd still like to see an example in the doc, even a dumb one from the tests. You can add a comment showing how the context changes after the tactic call. Lots of people seem to learn tactics by example, not by reading the descriptions.

[robertylewis]

Well, this failure message will never display in notriviality. Not sure if that's what Gabriel was pointing out.

You can get t more cleanly with `(@ne %%t _ _) ← target

[semorrison]

I've added the examples to the doc-string.

[robertylewis]

Thanks! LGTM if you're okay with the example I added.

bors d+

[bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests