# Zulip Chat Archive

## 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):

#### 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

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

@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?

#### Kenny Lau (Jan 25 2019 at 12:42):

no it didn't

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

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

#### Kenny Lau (Jan 25 2019 at 12:43):

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, 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 def pair (n : ℕ) := ∃ k, n = 2*k def impair (n : ℕ) := ∃ k, n = 2*k + 1 lemma div_euclide (a b : ℕ) (hb : b > 0 . tactic.exact_dec_trivial) : ∃ q : ℕ, ∃ r : ℕ, a = b*q + r ∧ r < b := ⟨a/b, ⟨a % b, by simp [add_comm, nat.mod_add_div, nat.mod_lt a hb]⟩⟩ lemma pair_ou_impair : ∀ n : ℕ, pair n ∨ impair n := begin intro n, rcases div_euclide n 2 with ⟨q, r, hnqr, hr⟩, nat_lt_cases hr, { left, use q, exact hnqr }, { right, use q, exact hnqr } end

The assumption `hnqr`

randomly disappears from context in either or both of the branches

#### Kevin Buzzard (Jan 25 2019 at 13:24):

make another assumption that depends on `hnqr`

so it can't be deleted :-)

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

Kevin, how would you do this proof in your classes?

#### Neil Strickland (Jan 25 2019 at 13:45):

Isn't fin_cases supposed to do this? (But fin_cases failed for unclear reasons, the only time I tried it.)

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

My data is not in `fin 2`

, it is a `nat`

which, by assumption, is less than 2. I don't want the overhead of translating back and forth between those two setups (that are mathematically indistinguishable)

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

I'm about to start classes on mathematical reasoning. I'll try to use Lean as a tool, but I'm not running a Lean course

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

I want all the technical Lean stuff to be hidden in mathlib or custom imports

#### Rob Lewis (Jan 25 2019 at 13:58):

I can take a shot at it. When you say the assumption randomly disappears, do you really mean its behavior changes in the same proof?

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

Yes, it can change if you restart Lean, or add unrelated stuff before the lemma etc.

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

Pretty much the same hell as with `tfae`

#### Rob Lewis (Jan 25 2019 at 13:58):

Hmm, okay.

#### Patrick Massot (Jan 25 2019 at 14:06):

Can you reproduce that using my MNWE?

#### Rob Lewis (Jan 25 2019 at 14:21):

Yeah, I can reproduce.

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

And can you fix it?

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

Not instantly!

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

I see your grant money drifting away from you...

#### Rob Lewis (Jan 25 2019 at 14:24):

I know grant proposals are usually ambitious, but "I can fix any bug in 10 seconds" might scare off even the ERC.

#### Rob Lewis (Jan 25 2019 at 14:39):

I don't know what `tactic.clear e`

is supposed to achieve. Deleting that seems to solve the issue.

#### Rob Lewis (Jan 25 2019 at 14:39):

But I also don't know where the undeterminism is coming from.

#### Rob Lewis (Jan 25 2019 at 14:40):

This whole tactic should probably be wrapped in `focus1`

. If there's more than one goal when you call it, the order gets screwed up.

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

Thanks! How do you "wrap in `focus1`

"?

#### Rob Lewis (Jan 25 2019 at 14:42):

`meta def nat_lt_cases (h : parse ident) : tactic unit := focus1 $ do ...`

#### 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