assumptions

Stream: new members

[Geoffrey Yeung]

is there something similar to meta def assumptions : tactic unit := `[ repeat { assumption } ] somewhere in the library?

[Chris Hughes]

; assumption

[Bryan Gin-ge Chen]

What about assumption'?

[Wojciech Nawrocki]

Isn't ; assumption, which applies once to every goal different from repeat {assumption}, which applies until it fails? assumption' also seems to do the former

[Geoffrey Yeung]

I just learned about ;. In mosts cases I can replace assumptions with ; assumption, but in a few places I need ; try {assumption} instead, because some branches need furthur processing

[Rob Lewis]

assumption fails when the goal can't be closed by something in the local context. So repeat {assumption} will close the first goals until it finds one that can't be closed. ; assumption will succeed if every subgoal produced by the previous tactic can be closed by assumption, and fail otherwise. assumption' will close all open goals that can be closed by assumption, and fail if none of them can be closed.

[Rob Lewis]

They're all subtly different. But I guess repeat {assumption} is rarely the one you want.

[Geoffrey Yeung]

yeah assumption' seems to be the solution

[Rob Lewis]

; assumption' should have the same effect as ; try {assumption}.

[Geoffrey Yeung]

side question: why does
example {a b c : Prop} : a → b → c → (a ∧ b) ∧ c := by { intros , repeat{ split } ; assumption } work, but
example {a b c : Prop} : a → b → c → (a ∧ b) ∧ c := by { intros , split , split ; assumption } doesn't?

[Geoffrey Yeung]

oh never mind figured it out, the ; is only applying to the second split