Stream: new members
Topic: Modus Ponens In Hypothesis
Henning Dieterichs (Nov 30 2020 at 17:29):
Sorry for all my questions!
I have the hypotheses
h: X and
g: Z -> X -> Y.
I would like to "rewrite"
Z -> Y. How can I do that elegantly (without an elaborate
Also, for a different use case, I would like to "rewrite"
Z -> Y, rather than
apply can only do this for the current goal.
Arguably, this kind of reasoning is untypical for mathematical proofs, but also is handwritten program verification where you have a lot of complex hypothesis.
Bryan Gin-ge Chen (Nov 30 2020 at 17:34):
You can use See tactic#replace.
replace g := g h (or
replace h := g h for your second question).
Mario Carneiro (Nov 30 2020 at 17:34):
simp [h] at g will probably work, if these are props
Mario Carneiro (Nov 30 2020 at 17:36):
You actually need
replace g := \lam z, g z h or
replace g := flip g h for the direct proof
Henning Dieterichs (Nov 30 2020 at 17:38):
Thanks for point out
replace! I was looking for that but could not find it in the standard lean tactics overview.
Henning Dieterichs (Nov 30 2020 at 17:40):
simp does not work in my case though. This works:
replace h4 := ant_eval_branch_or _ _ _ _ h4,
This does not:
simp [ant_eval_branch_or] at h4,
Mario Carneiro (Nov 30 2020 at 17:44):
if there are a lot of variables to unify it may not be as obvious to
simp as your example.
Mario Carneiro (Nov 30 2020 at 17:45):
the code you wrote is not equivalent, that will apply
h and produce
Z as a subgoal (which TBH is usually what you want)
Henning Dieterichs (Nov 30 2020 at 17:48):
You mean this (
replace h4 := ant_eval_branch_or _ _ _ _ h4,) will create a subgoal? In my case, I don't get a new subgoal...
Kevin Buzzard (Nov 30 2020 at 18:07):
If Lean can't guess what any of the
_s are, it will create new subgoals.
Last updated: May 14 2021 at 12:18 UTC