Trouble with cases and rintro / rcases

Stream: general

[Sorawee Porncharoenwase]

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?

[Kevin Buzzard]

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

[Jannis Limperg]

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.

[Sorawee Porncharoenwase]

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

[Eric Wieser]

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

[Simon Hudon]

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

[Sorawee Porncharoenwase]

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

[Simon Hudon]

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.

[Simon Hudon]

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

[Simon Hudon]

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

[Sorawee Porncharoenwase]

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

[Simon Hudon]

:+1:

[Simon Hudon]

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

[Bryan Gin-ge Chen]

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

[Simon Hudon]

Have you tried using field f1 instead of case f1?

[Simon Hudon]

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.

[Simon Hudon]

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

[Simon Hudon]

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.

[Simon Hudon]

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

[Bryan Gin-ge Chen]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Jannis Limperg]

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.

[Chris B]

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.

[Mario Carneiro]

It's talking about docs#relation.trans_gen

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris B]

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

[Chris B]

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)

[Mario Carneiro]

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

[Chris B]

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