Zulip Chat Archive

Stream: general

Topic: 6 cases


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 21:43):

Nice! exacts??

view this post on Zulip Kenny Lau (Nov 18 2018 at 21:43):

it clears many goals at once

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 24 2018 at 01:29):

@Kevin Buzzard

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 24 2018 at 22:20):

@Kevin Buzzard

view this post on Zulip Kenny Lau (Nov 24 2018 at 22:20):

@Mario Carneiro how can I improve this tactic?

view this post on Zulip 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>,...]

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 24 2018 at 22:27):

great

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jan 25 2019 at 12:42):

no it didn't

view this post on Zulip Patrick Massot (Jan 25 2019 at 12:42):

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

view this post on Zulip Kenny Lau (Jan 25 2019 at 12:43):

no idea

view this post on Zulip Patrick Massot (Jan 25 2019 at 12:50):

It doesn't work at all actually

view this post on Zulip Patrick Massot (Jan 25 2019 at 12:50):

Sometimes it works but this is very unstable

view this post on Zulip Patrick Massot (Jan 25 2019 at 12:54):

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

view this post on Zulip Patrick Massot (Jan 25 2019 at 13:17):

@Rob Lewis maybe?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 13:24):

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

view this post on Zulip Patrick Massot (Jan 25 2019 at 13:27):

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

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 25 2019 at 13:54):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 25 2019 at 13:58):

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

view this post on Zulip Patrick Massot (Jan 25 2019 at 13:58):

Pretty much the same hell as with tfae

view this post on Zulip Rob Lewis (Jan 25 2019 at 13:58):

Hmm, okay.

view this post on Zulip Patrick Massot (Jan 25 2019 at 14:06):

Can you reproduce that using my MNWE?

view this post on Zulip Rob Lewis (Jan 25 2019 at 14:21):

Yeah, I can reproduce.

view this post on Zulip Patrick Massot (Jan 25 2019 at 14:22):

And can you fix it?

view this post on Zulip Rob Lewis (Jan 25 2019 at 14:22):

Not instantly!

view this post on Zulip Patrick Massot (Jan 25 2019 at 14:22):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jan 25 2019 at 14:39):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 25 2019 at 14:42):

Thanks! How do you "wrap in focus1"?

view this post on Zulip Rob Lewis (Jan 25 2019 at 14:42):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 25 2019 at 17:04):

But I can't use this get_lt_sides in any case

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 25 2019 at 17:11):

Maybe I can actually

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Rob Lewis (Jan 25 2019 at 17:22):

Add clear_lst [h] before swap, I think.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 25 2019 at 17:39):

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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Rob Lewis (Jan 25 2019 at 18:03):

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

view this post on Zulip Patrick Massot (Jan 25 2019 at 18:03):

I'd love to see that

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 25 2019 at 18:13):

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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Jan 25 2019 at 19:46):

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

view this post on Zulip Patrick Massot (Jan 25 2019 at 19:48):

Thanks!


Last updated: May 13 2021 at 04:21 UTC