Zulip Chat Archive

Stream: new members

Topic: assumptions


view this post on Zulip Geoffrey Yeung (Jan 21 2019 at 20:11):

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

view this post on Zulip Chris Hughes (Jan 21 2019 at 20:46):

; assumption

view this post on Zulip Bryan Gin-ge Chen (Jan 21 2019 at 21:02):

What about assumption'?

view this post on Zulip Wojciech Nawrocki (Jan 21 2019 at 21:34):

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

view this post on Zulip Geoffrey Yeung (Jan 21 2019 at 21:53):

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

view this post on Zulip Rob Lewis (Jan 21 2019 at 21:54):

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.

view this post on Zulip Rob Lewis (Jan 21 2019 at 21:56):

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

view this post on Zulip Geoffrey Yeung (Jan 21 2019 at 21:58):

yeah assumption' seems to be the solution

view this post on Zulip Rob Lewis (Jan 21 2019 at 21:58):

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

view this post on Zulip Geoffrey Yeung (Jan 21 2019 at 21:59):

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?

view this post on Zulip Geoffrey Yeung (Jan 21 2019 at 22:01):

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


Last updated: May 15 2021 at 23:13 UTC