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" 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.

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.

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