6 cases

Stream: general

[Kevin Buzzard]

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]

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]

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]

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]

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]

Nice! exacts??

[Kenny Lau]

it clears many goals at once

[Kenny Lau]

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]

@Kevin Buzzard

[Kevin Buzzard]

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

[Kenny Lau]

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]

@Kevin Buzzard

[Kenny Lau]

@Mario Carneiro how can I improve this tactic?

[Kevin Buzzard]

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]

Someone will want you to do it for Ha : r > 2 Hb : r <= 6 at some point

[Kenny Lau]

great

[Patrick Massot]

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]

no it didn't

[Patrick Massot]

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

[Kenny Lau]

no idea

[Patrick Massot]

It doesn't work at all actually

[Patrick Massot]

Sometimes it works but this is very unstable

[Patrick Massot]

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

[Patrick Massot]

@Rob Lewis maybe?

[Patrick Massot]

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]

make another assumption that depends on hnqr so it can't be deleted :-)

[Patrick Massot]

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

[Neil Strickland]

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

[Patrick Massot]

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]

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]

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

[Rob Lewis]

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]

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

[Patrick Massot]

Pretty much the same hell as with tfae

[Rob Lewis]

Hmm, okay.

[Patrick Massot]

Can you reproduce that using my MNWE?

[Rob Lewis]

Yeah, I can reproduce.

[Patrick Massot]

And can you fix it?

[Rob Lewis]

Not instantly!

[Patrick Massot]

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

[Rob Lewis]

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

[Rob Lewis]

I don't know what tactic.clear e is supposed to achieve. Deleting that seems to solve the issue.

[Rob Lewis]

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

[Rob Lewis]

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]

Thanks! How do you "wrap in focus1"?

[Rob Lewis]

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

[Patrick Massot]

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]

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]

You can probably take advantage of the fact that nat.lt is defined in terms of nat.le.

[Patrick Massot]

I'm afraid this will rather be a disadvantage. The le case may match when I want lt to match

[Patrick Massot]

But I can't use this get_lt_sides in any case

[Rob Lewis]

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]

Maybe I can actually

[Patrick Massot]

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]

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]

Add clear_lst [h] before swap, I think.

[Rob Lewis]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

I'd love to see that

[Rob Lewis]

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]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

Thanks!