Zulip Chat Archive

Stream: new members

Topic: Modus Ponens In Hypothesis


view this post on Zulip 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" g to Z -> Y. How can I do that elegantly (without an elaborate have proof)?

Also, for a different use case, I would like to "rewrite" h to Z -> Y, rather than g.
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.

view this post on Zulip Bryan Gin-ge Chen (Nov 30 2020 at 17:34):

You can use replace g := g h (or replace h := g h for your second question). See tactic#replace.

view this post on Zulip Mario Carneiro (Nov 30 2020 at 17:34):

simp [h] at g will probably work, if these are props

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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,

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip 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