[Merged by Bors] - feat(logic/nontrivial): a tactic to summon nontrivial instances#4374
[Merged by Bors] - feat(logic/nontrivial): a tactic to summon nontrivial instances#4374
Conversation
kim-em
commented
Oct 3, 2020
|
@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 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. |
src/logic/nontrivial.lean
Outdated
| t ← (do `(%%a ≠ %%b) ← target, infer_type a) <|> (do `(%%a < %%b) ← target, infer_type a) <|> | ||
| fail "Goal is not `_ ≠ _` or `_ < _`", |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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)?
There was a problem hiding this comment.
You can do something like
guardb $ e.is_app_of `ne || e.is_app_of `has_le.le,
return $ e.get_app_args.headbut 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.
There was a problem hiding this comment.
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 α?
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Okay, I've revised the tactic, so it now takes an optional type argument.
robertylewis
left a comment
There was a problem hiding this comment.
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.
src/logic/nontrivial.lean
Outdated
| t ← (do `(%%a ≠ %%b) ← target, infer_type a) <|> (do `(%%a < %%b) ← target, infer_type a) <|> | ||
| fail "Goal is not `_ ≠ _` or `_ < _`", |
There was a problem hiding this comment.
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
|
I've added the examples to the doc-string. |
|
Thanks! LGTM if you're okay with the example I added. bors d+ |
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
``` 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`. ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |