Zulip Chat Archive

Stream: new members

Topic: term mode replacement for cases


view this post on Zulip Jakob Scholbach (Apr 02 2021 at 09:57):

Is there a term-mode equivalent of cases? Such as in the following example (the lemma bla is of course useless, just meant to provide a mwe)

variables h1 : Prop
variables h2 : Prop
variables h3 : Prop

lemma bla : h1  h2 :=
begin sorry end

lemma blub (h1 h2 : Prop): h3 :=
begin
  cases bla h1 h2 with e f, -- this is what I want to replace by term-mode
  { sorry },
  { sorry }
end

view this post on Zulip Patrick Massot (Apr 02 2021 at 09:57):

Sure, you can use the recursor directly.

view this post on Zulip Jakob Scholbach (Apr 02 2021 at 09:58):

Just omit begin end ?

view this post on Zulip Patrick Massot (Apr 02 2021 at 09:58):

Also remember that show_term answers all these questions in principle.

view this post on Zulip Kevin Buzzard (Apr 02 2021 at 09:58):

Use or.rec or or.elim or whatever it's called

view this post on Zulip Mario Carneiro (Apr 02 2021 at 09:59):

match is also a term mode construct

view this post on Zulip Patrick Massot (Apr 02 2021 at 09:59):

lemma blub (h1 h2 : Prop): h3 :=
begin
show_term {  cases bla h1 h2 with e f, -- this is what I want to replace by term-mode
  { sorry },
  { sorry } }
end

view this post on Zulip Mario Carneiro (Apr 02 2021 at 10:00):

lemma blub (h1 h2 : Prop): h3 :=
(bla h1 h2).elim
  (λ e, sorry)
  (λ f, sorry)

view this post on Zulip Mario Carneiro (Apr 02 2021 at 10:01):

lemma blub (h1 h2 : Prop): h3 :=
match bla h1 h2 with
| or.inl e := sorry
| or.inr f := sorry
end

Last updated: May 18 2021 at 16:25 UTC