Zulip Chat Archive

Stream: general

Topic: One of many pattern match hygiene


view this post on Zulip Scott Viteri (Mar 19 2021 at 20:48):

Suppose I have some predicate P and tactic t1 and t2 such that

lemma l :  (o₁ o₂ o₃ : option ), P o₁ o₂ o₃
| none _ _ := by t₁
| _ none _ := by t₁
| _ _ none := by t₁
| (some a) (some b) (some c) := by t₂

I would like to condense the proof so that it looks like:

lemma l :  (o₁ o₂ o₃ : option ), P o₁ o₂ o₃
| one_is_none case := by t₁
| (some a) (some b) (some c) := by t₂

view this post on Zulip Scott Viteri (Mar 19 2021 at 20:48):

Is this possible/recommended?

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 20:51):

... :=
begin
  rintro (_ | _) (_ | _) (_ | _);
  { t₁ <|> t₂ }
end

view this post on Zulip Scott Viteri (Mar 19 2021 at 21:03):

This is nice thank you

view this post on Zulip Scott Viteri (Mar 19 2021 at 21:03):

for long t1 and t2 I am finding this makes the proof less readable

view this post on Zulip Scott Viteri (Mar 19 2021 at 21:03):

not sure what to do about that

view this post on Zulip Mario Carneiro (Mar 19 2021 at 22:10):

For more targeted calls I would do this:

lemma l (o₁ o₂ o₃ : option ) : P o₁ o₂ o₃ :=
begin
  cases o₁ with a, swap,
  cases o₂ with b, swap,
  cases o₃ with b, swap,
  { t₂ },
  all_goals {
    t₁
  }
end

view this post on Zulip Eric Wieser (Mar 19 2021 at 22:12):

Could also use tactic#case to pull out just the some some some goal without the swaps

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 22:27):

lemma l :  (o₁ o₂ o₃ : option ), P o₁ o₂ o₃ :=
begin
  repeat { all_goals { rintro (_ | _) }, swap },
  t1,
  all_goals { t2 }
end

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 22:27):

For your "variadic" needs


Last updated: May 18 2021 at 17:44 UTC