Modus Ponens In Hypothesis

Stream: new members

[Henning Dieterichs]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

You actually need replace g := \lam z, g z h or replace g := flip g h for the direct proof

[Henning Dieterichs]

Thanks for point out replace! I was looking for that but could not find it in the standard lean tactics overview.

[Henning Dieterichs]

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]

if there are a lot of variables to unify it may not be as obvious to simp as your example.

[Mario Carneiro]

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]

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]

If Lean can't guess what any of the _s are, it will create new subgoals.