## Stream: general

### Topic: 6 cases

#### Kevin Buzzard (Nov 18 2018 at 19:46):

Is there a trick for doing this painlessly:

lemma H0 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 0 := ⟨4,0,1,rfl⟩
lemma H1 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 1 := ⟨0,5,0,rfl⟩
lemma H2 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 2 := ⟨1,0,2,rfl⟩
lemma H3 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 3 := ⟨0,3,1,rfl⟩
lemma H4 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 4 := ⟨8,0,0,rfl⟩
lemma H5 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 5 := ⟨0,1,2,rfl⟩

example (r : ℕ) (Hr : r < 6) : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + r := sorry


Currently I have

example (r : ℕ) (Hlt6 : r < 6) : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + r :=
begin
cases (lt_or_eq_of_le (nat.le_of_succ_le_succ Hlt6)) with Hlt5 Heq5,
cases (lt_or_eq_of_le (nat.le_of_succ_le_succ Hlt5)) with Hlt4 Heq4,
cases (lt_or_eq_of_le (nat.le_of_succ_le_succ Hlt4)) with Hlt3 Heq3,
cases (lt_or_eq_of_le (nat.le_of_succ_le_succ Hlt3)) with Hlt2 Heq2,
cases (lt_or_eq_of_le (nat.le_of_succ_le_succ Hlt2)) with Hlt1 Heq1,
cases (lt_or_eq_of_le (nat.le_of_succ_le_succ Hlt1)) with Hlt0 Heq0,
cases Hlt0,
rw Heq0, exact H0,
rw Heq1, exact H1,
rw Heq2, exact H2,
rw Heq3, exact H3,
rw Heq4, exact H4,
rw Heq5, exact H5,
end




#### Kevin Buzzard (Nov 18 2018 at 20:00):

Just to be clear -- "this" isn't proving the 6 lemmas, it's proving the example. I guess I'd like some tactic which replaces r < 6 -> P r with P 0 \and P 1 \and P 2 \and P 3 \and P 4 \and P 5 which I could then just kill with \<H0,H1,H2,H3,H4,H5\> on one line.

#### Kevin Buzzard (Nov 18 2018 at 20:02):

Here's the context (question and solution on an M1F example sheet):

https://github.com/ImperialCollegeLondon/M1F_example_sheets/tree/master/src/example_sheet_05/Sht05Q05

#### Bryan Gin-ge Chen (Nov 18 2018 at 20:07):

This isn't the tactic you want, but is (in my opinion) a little cleaner than what you posted:

example (r : ℕ) (Hr : r < 6) : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + r :=
match r, Hr with
| 0, H := H0
| 1, H := H1
| 2, H := H2
| 3, H := H3
| 4, H := H4
| 5, H := H5
| (n+6), H :=
begin
revert H,
simp
end
end


#### Kenny Lau (Nov 18 2018 at 20:16):

lemma H0 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 0 := ⟨4,0,1,rfl⟩
lemma H1 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 1 := ⟨0,5,0,rfl⟩
lemma H2 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 2 := ⟨1,0,2,rfl⟩
lemma H3 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 3 := ⟨0,3,1,rfl⟩
lemma H4 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 4 := ⟨8,0,0,rfl⟩
lemma H5 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 5 := ⟨0,1,2,rfl⟩

example (r : ℕ) (Hr : r < 6) : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + r :=
begin
repeat { cases Hr with _ Hr },
exacts [H5, H4, H3, H2, H1, H0]
end


#### Kevin Buzzard (Nov 18 2018 at 21:43):

Nice! exacts??

#### Kenny Lau (Nov 18 2018 at 21:43):

it clears many goals at once

#### Kenny Lau (Nov 24 2018 at 01:28):

import tactic.fin_cases

lemma H0 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 0 := ⟨4,0,1,rfl⟩
lemma H1 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 1 := ⟨0,5,0,rfl⟩
lemma H2 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 2 := ⟨1,0,2,rfl⟩
lemma H3 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 3 := ⟨0,3,1,rfl⟩
lemma H4 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 4 := ⟨8,0,0,rfl⟩
lemma H5 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 5 := ⟨0,1,2,rfl⟩

example (r : ℕ) (Hr : r < 6) : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + r :=
begin
suffices : ∀ x : fin 6, ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + x.1,
{ exact this ⟨r, Hr⟩ },
intro x,
fin_cases x,
exacts [H0, H1, H2, H3, H4, H5]
end


@Kevin Buzzard

#### Kevin Buzzard (Nov 24 2018 at 07:49):

Aah I remember Scott talking about cases on fin n. So this happened? :-) Thanks for pointing it out!

#### Kenny Lau (Nov 24 2018 at 22:20):

import tactic.interactive

namespace tactic.interactive
open lean.parser tactic interactive
meta def nat_lt_cases (h : parse ident) : tactic unit :=
do e ← get_local h,
(%%val < %%ebound) ← infer_type e,
bound ← eval_expr ℕ ebound,
expr.local_const _ nval _ _ ← return val,
iterate_at_most bound (do val ← get_local nval,
(_,_,(_,e)::_)::_ ← tactic.cases_core val [nval,h],
tactic.clear e, swap),
e ← get_local h, val ← get_local nval,
proof ← to_expr (absurd %%e (not_lt_of_ge $nat.le_add_left %%ebound %%val)), tactic.exact proof, goals ← get_goals, set_goals goals.reverse, skip end tactic.interactive lemma H0 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 0 := ⟨4,0,1,rfl⟩ lemma H1 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 1 := ⟨0,5,0,rfl⟩ lemma H2 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 2 := ⟨1,0,2,rfl⟩ lemma H3 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 3 := ⟨0,3,1,rfl⟩ lemma H4 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 4 := ⟨8,0,0,rfl⟩ lemma H5 : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + 5 := ⟨0,1,2,rfl⟩ example (r : ℕ) (Hr : r < 6) : ∃ (a b c : ℕ), 6 * a + 9 * b + 20 * c = 44 + r := begin nat_lt_cases Hr, exacts [H0, H1, H2, H3, H4, H5] end  #### Kenny Lau (Nov 24 2018 at 22:20): @Kevin Buzzard #### Kenny Lau (Nov 24 2018 at 22:20): @Mario Carneiro how can I improve this tactic? #### Kevin Buzzard (Nov 24 2018 at 22:23): Aah, they appear in the right order this time :-) I guess you can just exacts [<4,0,1,rfl>,<0,5,0,rfl>,...] #### Kevin Buzzard (Nov 24 2018 at 22:24): Someone will want you to do it for Ha : r > 2 Hb : r <= 6 at some point #### Kenny Lau (Nov 24 2018 at 22:27): great #### Patrick Massot (Jan 25 2019 at 12:42): import tactic.interactive namespace tactic.interactive open lean.parser tactic interactive meta def nat_lt_cases (h : parse ident) : tactic unit := do e ← get_local h, (%%val < %%ebound) ← infer_type e, bound ← eval_expr ℕ ebound, expr.local_const _ nval _ _ ← return val, iterate_at_most bound (do val ← get_local nval, (_,_,(_,e)::_)::_ ← tactic.cases_core val [nval,h], tactic.clear e, swap), e ← get_local h, val ← get_local nval, proof ← to_expr (absurd %%e (not_lt_of_ge$ nat.le_add_left %%ebound %%val)),
tactic.exact proof,
goals ← get_goals,
set_goals goals.reverse,
skip
end tactic.interactive


@Kenny Lau what happened to this tactic, did it ever get PR'ed?

no it didn't

#### Patrick Massot (Jan 25 2019 at 12:42):

Is there a better recommended way do achieve the same result?

no idea

#### Patrick Massot (Jan 25 2019 at 12:50):

It doesn't work at all actually

#### Patrick Massot (Jan 25 2019 at 12:50):

Sometimes it works but this is very unstable

#### Patrick Massot (Jan 25 2019 at 12:54):

I'd be very grateful if someone can make a reliable version of this tactic

#### Patrick Massot (Jan 25 2019 at 13:17):

@Rob Lewis maybe?

#### Patrick Massot (Jan 25 2019 at 13:20):

MWE:

import tactic.interactive

namespace tactic.interactive
open lean.parser tactic interactive
meta def nat_lt_cases (h : parse ident) : tactic unit :=
do e ← get_local h,
(%%val < %%ebound) ← infer_type e,
bound ← eval_expr ℕ ebound,
expr.local_const _ nval _ _ ← return val,
iterate_at_most bound (do val ← get_local nval,
(_,_,(_,e)::_)::_ ← tactic.cases_core val [nval,h],
tactic.clear e, swap),
e ← get_local h, val ← get_local nval,

#### Patrick Massot (Jan 25 2019 at 16:22):

I tried to build a version which would also work with ≤ but failed. How would you try  (%%val < %%ebound) ← infer_type e, and then try  (%%val ≤ %%ebound) ← infer_type e,  and tweak the bound accordingly?

#### Rob Lewis (Jan 25 2019 at 16:48):

I'd just define something like this:

meta def get_lt_sides : expr → tactic (expr × ℕ)
| (%%val ≤ %%ebound) := prod.mk val <$> nat.succ <$> eval_expr ℕ ebound
| (%%val < %%ebound) := prod.mk val <$> eval_expr ℕ ebound | _ := failed  #### Rob Lewis (Jan 25 2019 at 16:50): You can probably take advantage of the fact that nat.lt is defined in terms of nat.le. #### Patrick Massot (Jan 25 2019 at 17:04): I'm afraid this will rather be a disadvantage. The le case may match when I want lt to match #### Patrick Massot (Jan 25 2019 at 17:04): But I can't use this get_lt_sides in any case #### Rob Lewis (Jan 25 2019 at 17:11): If you modify the tactic to work on an le proof instead of a lt proof, and use get_lt_sides at the beginning to compute bound, it should work when given either an le or an lt proof. #### Patrick Massot (Jan 25 2019 at 17:11): Maybe I can actually #### Patrick Massot (Jan 25 2019 at 17:14): My problem was I was not able to reconstitute ebound from bound but I cheated in namespace tactic.interactive open lean.parser tactic interactive meta def get_lt_sides : expr → tactic (expr × expr × ℕ) | (%%val < %%ebound) := prod.mk val <$> (prod.mk ebound <$> eval_expr ℕ ebound) | (%%val ≤ %%ebound) := prod.mk val <$> (prod.mk ebound <$> nat.succ <$> eval_expr ℕ ebound)
| _ := failed

meta def nat_cases (h : parse ident) : tactic unit :=
focus1 $do e ← get_local h, ⟨val, ⟨ebound, bound⟩⟩ ← infer_type e >>= get_lt_sides, expr.local_const _ nval _ _ ← return val, iterate_at_most bound (do val ← get_local nval, (_,_,(_,e)::_)::_ ← tactic.cases_core val [nval,h], swap), e ← get_local h, val ← get_local nval, proof ← to_expr (absurd %%e (not_lt_of_ge$ nat.le_add_left %%ebound %%val)),
tactic.exact proof,
goals ← get_goals,
set_goals goals.reverse,
skip
end tactic.interactive


#### Patrick Massot (Jan 25 2019 at 17:18):

But we still have the esthetic problem that you removed the tactic.clear which was meant to get rid of the bound assumption (which is turned into silly inequalities after running the tactic)

#### Rob Lewis (Jan 25 2019 at 17:22):

Add clear_lst [h] before swap, I think.

#### Rob Lewis (Jan 25 2019 at 17:22):

clear takes an expr, clear_lst takes a list of names, I think we're missing a version that takes a single name.

#### Patrick Massot (Jan 25 2019 at 17:32):

Thank you very much Rob (and Kenny for the initial version). What I currently have is:

open tactic
meta def get_nat_ineq : expr → tactic (expr × expr × ℕ)
| (%%val < %%ebound) := prod.mk val <$> (prod.mk ebound <$> eval_expr ℕ ebound)
| (%%val ≤ %%ebound) := prod.mk val <$> (prod.mk ebound <$> nat.succ <$> eval_expr ℕ ebound) | _ := failed namespace tactic.interactive open lean.parser interactive meta def nat_cases (h : parse ident) : tactic unit := focus1$ do
e ← get_local h,
⟨val, ⟨ebound, bound⟩⟩ ← infer_type e >>= get_nat_ineq,
expr.local_const _ nval _ _ ← return val,
iterate_at_most bound $do { val ← get_local nval, (_,_,(_,e)::_)::_ ← tactic.cases_core val [nval, h], clear_lst [h], swap}, e ← get_local h, val ← get_local nval, proof ← to_expr (absurd %%e (not_lt_of_ge$ nat.le_add_left %%ebound %%val)),
tactic.exact proof,
goals ← get_goals,
set_goals goals.reverse
end tactic.interactive


It works for me, and I think this is a very useful tactic. Do you want to open a PR? Would you like me to do it?

#### Patrick Massot (Jan 25 2019 at 17:39):

Or should we wait until someone does a version consuming an optional lower bound?

#### Patrick Massot (Jan 25 2019 at 17:39):

I also have tests if you want to PR:

example (n : ℕ) (h : n ≤ 4) : n ≤ 10 :=
begin
nat_cases h,
do { goals ← get_goals, guard (goals.length = 5) },
all_goals { exact dec_trivial},
end

example (n : ℕ) (h : n < 4) : n ≤ 10 :=
begin
nat_cases h,
do { goals ← get_goals, guard (goals.length = 4) },
all_goals { exact dec_trivial},
end


#### Rob Lewis (Jan 25 2019 at 18:01):

Nice! I think this is "complete" when it takes an optional lower bound (and in that case, works for int also). When you write something that does x, and y looks similar to x, people will eventually ask you to make it do y as well. :slight_smile:

#### Rob Lewis (Jan 25 2019 at 18:03):

Going from here to there is nontrivial but not super difficult.

#### Patrick Massot (Jan 25 2019 at 18:03):

I'd love to see that

#### Rob Lewis (Jan 25 2019 at 18:05):

This could be a good exercise for anyone looking to get better at writing tactics. I don't mind seeing this PR'ed as is, with a little cleanup, with the expectation that someone will finish it.

#### Rob Lewis (Jan 25 2019 at 18:07):

For cleanup: you don't need to bind the result of cases_core. There are some unneeded tactic. names since you have tactic open.

#### Patrick Massot (Jan 25 2019 at 18:13):

I think that tactic.exact is there to disambiguate from tactic.interactive.exact

#### Patrick Massot (Jan 25 2019 at 18:45):

I'd like to know how to avoid that ebound hack though. Inside a tactic, I have a nat taken from a function returning tactic nat, how can I turn it into an expr?

#### Simon Hudon (Jan 25 2019 at 19:46):

if n is your nat, reflect n will give you an expression that corresponds to it

#### Patrick Massot (Jan 25 2019 at 19:48):

Thanks!

Last updated: May 13 2021 at 04:21 UTC