Zulip Chat Archive

Stream: general

Topic: Trouble with cases and rintro / rcases


view this post on Zulip Sorawee Porncharoenwase (Nov 06 2020 at 22:12):

Consider:

import tactic.basic

inductive val : Type
| nat (n : ) : val
| list (vs : list val) : val

inductive ok : val  Prop
| nat {n : } (h : n = 1) : ok (val.nat n)
| list_nil : ok (val.list [])
| list_cons {v vs} (h : ok v) (h' : ok (val.list vs)) : ok (val.list (v :: vs))

lemma test {v : val} {vs : list val} : ok (val.list (v :: vs))  ok v :=
begin
  intro h,
  cases h with a b,
  sorry,
end

I would expect the two hypotheses introduced by cases to be named a and b. Yet, they are named h_h and h_h' .

The same occurs when I change cases h with a b, to rcases h with ⟨a, b⟩,.

Lastly, consider:

import tactic.basic

inductive val : Type
| nat (n : ) : val
| list (vs : list val) : val

mutual inductive ok, ok_aux
with ok : val  Prop
| nat {n : } (h : n = 1) : ok (val.nat n)
| list {xs} (h : ok_aux xs) : ok (val.list xs)
with ok_aux : list val  Prop
| nil : ok_aux []
| cons {v vs} (h : ok v) (h' : ok_aux vs) : ok_aux (v :: vs)

lemma test {v : val} {vs : list val} : ok (val.list (v :: vs))  ok v :=
begin
  rintro x⟩,
end

At the end, it says "goals accomplished", but at the same time it says

tactic failed, result contains meta-variables
state:
no goals

Are these bugs or do I misunderstand anything?

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 22:15):

I'm not at lean right now, but the last error is usually caused by a buggy tactic. Try recover to work around it.

view this post on Zulip Jannis Limperg (Nov 06 2020 at 22:24):

The first error is essentially an implementation detail of cases. In the with cause, you give names for all constructor arguments in order, so your a and b are interpreted as the names given to the arguments n and h of ok.nat. However, cases then realises that this constructor is impossible, so a and b never show up in the goal. Try this instead: cases h with _ _ _ _ a b.

Wrt the second issue, I would advise you to stay away from mutual inductive types (and ideally also nested inductives). They are shoddily implemented and basically untested, so you can expect a lot of random errors.

view this post on Zulip Sorawee Porncharoenwase (Nov 06 2020 at 22:35):

Thanks, cases h with _ _ _ _ a b works perfectly!

view this post on Zulip Eric Wieser (Nov 06 2020 at 23:45):

I think you can also use cases h and then case ok.list_cons : _ _ a b { sorry }

view this post on Zulip Simon Hudon (Nov 07 2020 at 04:27):

And you can write pretty_cases to see which position in the list of names names which variable.

view this post on Zulip Sorawee Porncharoenwase (Nov 07 2020 at 05:34):

@Simon Hudon pretty_cases doesn't seem to work on the above example. It generates

case [anonymous]
  { admit },

which is a syntax error.

I guess a related question is, is there a way to use case for case splitting arises from split or things like that? I currently use comment and indentation to informally structure the proof. E.g., currently I write

repeat { split },
  -- case A
  tactic_a,

  -- case B
  tactic_b,

  -- case C
  tactic_c,

But it would be nice to have an actual support from the language. E.g., being able to write:

repeat { split },
case [1] {
  tactic_a,
},
case [2] {
  tactic_b,
},
case [3] {
  tactic_c,
},

instead.

view this post on Zulip Simon Hudon (Nov 07 2020 at 05:38):

That's because pretty_cases, like case itself, relies on goal tags. induction and cases add tags to goals corresponding to the constructors. If you call any tactics afterwards (with a few exceptions), those tags will be erased.

view this post on Zulip Simon Hudon (Nov 07 2020 at 05:38):

In order to make your use case possible, you'd need split to tag the generated goals.

view this post on Zulip Simon Hudon (Nov 07 2020 at 05:40):

What benefit to do see in using case [1] { ... } instead of just { ... },?

view this post on Zulip Sorawee Porncharoenwase (Nov 07 2020 at 05:42):

I didn't know that that works! Time to refactor my code :)

view this post on Zulip Simon Hudon (Nov 07 2020 at 05:42):

:+1:

view this post on Zulip Simon Hudon (Nov 07 2020 at 05:43):

You might like refine_struct btw. It tags goals with the field names of a structure

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2020 at 05:55):

@Simon Hudon somewhat related: do you understand #4779?

view this post on Zulip Simon Hudon (Nov 07 2020 at 05:58):

Have you tried using field f1 instead of case f1?

view this post on Zulip Simon Hudon (Nov 07 2020 at 05:59):

I did not consider mixing the two. The refine_struct machinery clashes with case but I don't think it needs to be the case.

view this post on Zulip Simon Hudon (Nov 07 2020 at 06:02):

You can see here the encoding of tags: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive.lean#L311

view this post on Zulip Simon Hudon (Nov 07 2020 at 06:04):

In comparison, cases and inductive use _case as a prefix. refine_struct also uses shorter tags. In case, you have to give the fully qualified name of the constructor and I wanted to avoid it.

view this post on Zulip Simon Hudon (Nov 07 2020 at 06:06):

We could use the same convention for refine_struct and cases / inductive and use case for both, changing case to allow the omission of qualifiers in constructor and field names

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2020 at 06:12):

Ah, I see. Yes, field f1 does work. This was not at all clear to me from tactic#refine_struct and the tactic state.

view this post on Zulip Simon Hudon (Nov 07 2020 at 06:14):

I didn't think the proof state printing case foo would be a big deal but looking back, I realize that wasn't my best idea

view this post on Zulip Simon Hudon (Nov 07 2020 at 06:17):

Merging cases and refine_struct might be pretty hairy because of what case does to rename variables.

view this post on Zulip Jannis Limperg (Nov 07 2020 at 10:27):

Simon Hudon said:

In comparison, cases and inductive use _case as a prefix. refine_struct also uses shorter tags. In case, you have to give the fully qualified name of the constructor and I wanted to avoid it.

FYI, I changed case at some point so that you can now give shorter names as well. Essentially, case now looks for an unambiguous suffix, so in Sorawee's example, case list_cons would work.

view this post on Zulip Chris B (Nov 07 2020 at 17:07):

Small nitpick about rcases while it's being discussed; the doc string showing the syntax uses something called trans_rel that doesn't seem to exist.

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:18):

It's talking about docs#relation.trans_gen

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:23):

the suggested match syntax is also wrong for trans_gen, it should have 2 args in the first case and 4 in the second. But now I'm worried if I put that there that it will look confusing unless I also provide the definition of the inductive

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:23):

the point of the quote is just to say you can match on more complex inductive predicates

view this post on Zulip Chris B (Nov 07 2020 at 17:24):

Did the name get changed without the comment getting updated or do mathlib people know trans_rel |-> relation.trans_gen?

view this post on Zulip Chris B (Nov 07 2020 at 17:25):

I'm worried if I put that there that it will look confusing unless I also provide the definition of the inductive

I think if people can grep it or do like #print trans_gen and get something back it's fine right? (or use the doc search thing)

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:26):

Chris B said:

Did the name get changed without the comment getting updated or do mathlib people know trans_rel |-> relation.trans_gen?

No, I just recalled the name imperfectly from memory

view this post on Zulip Chris B (Nov 07 2020 at 18:05):

While I'm splitting hairs, I think rcases h e pat performs... is missing a colon between h and e.


Last updated: May 11 2021 at 22:14 UTC