rcases question

Stream: mathlib4

[Matthew Ballard]

I don't understand the behavior of rintro in the following. Hopefully I am just dense.

import Std.Tactic.RCases

inductive BaseType : Type where
  | one
  | two

open BaseType

inductive BaseTypeHom : BaseType → BaseType → Type where
  | left : BaseTypeHom one two
  | right : BaseTypeHom one two
  | id (X : BaseType) : BaseTypeHom X X

def triv : (X Y : BaseType) → BaseTypeHom X Y → Unit := by
  rintro (_|_) (_|_) (_|_|_);  --- rcases tactic failed: one is not a fvar

[Matthew Ballard]

I am guessing it is trying to pull the X from the id branch of BaseTypeHom but making it implicit doesn't help

[Matthew Ballard]

If my understanding is correct, what is the proper incantation with | and _ to capture all three constructors for BaseTypeHom?

[Matthew Ballard]

This is fine

def triv (X Y : BaseType) : BaseTypeHom X Y → Unit := by
  rintro (_|_|_)

[Matthew Ballard]

This works as expected

import Std.Tactic.RCases

inductive Hom : Unit → Unit → Type where
  | loop : Hom unit unit
  | id (X : Unit) : Hom X X

def triv₂ : Hom unit unit → Unit := by
  rintro (_|_)

[Matthew Ballard]

This does not

import Std.Tactic.RCases

inductive BaseType : Type where
  | one

open BaseType

inductive BaseTypeHom : BaseType → BaseType → Type where
  | loop : BaseTypeHom one one
  | id (X : BaseType) : BaseTypeHom X X

def triv₂ : BaseTypeHom one one → Unit := by
  rintro (_|_) -- rcases tactic failed: one is not a fvar

[Matthew Ballard]

@Mario Carneiro is this expected behavior?

[Mario Carneiro]

yes this is expected

[Mario Carneiro]

try using \<\<\>\> instead for the last pattern match

[Mario Carneiro]

if your goal is just to pattern match once on BaseTypeHom and get three cases, the earlier pattern matches are only confusing matters. Just use _ _ (_|_|_)

[Matthew Ballard]

def triv₂ : BaseTypeHom one one → Unit := by
  rintro ⟨⟨⟩⟩

gives the same not an fvar error

[Mario Carneiro]

does intro h; cases h work in the last example?

[Matthew Ballard]

Mario Carneiro said:

if your goal is just to pattern match once on BaseTypeHom and get three cases, the earlier pattern matches are only confusing matters. Just use _ _ (_|_|_)

I think this works for my use. Thanks

[Matthew Ballard]

Mario Carneiro said:

does intro h; cases h work in the last example?

Yes that does work for the last example.

[Mario Carneiro]

in that case I think there is a bug in rcases

[Mario Carneiro]

the "one is not an fvar" error is not supposed to happen

[Matthew Ballard]

Should I make an issue?

[Matthew Ballard]

Darn. The error also pops up in

def triv₃ : (X : BaseType) → BaseTypeHom X X → BaseTypeHom X X → Unit := by
  rintro _ (_|_) (_|_)

[Matthew Ballard]

Over the second hom

[Mario Carneiro]

you can probably just do rintro _ (_|_) h <;> cases h

[Matthew Ballard]

Mario Carneiro said:

you can probably just do rintro _ (_|_) h <;> cases h

Hmm that tosses the same error I think the infoview wasn't updating...It wasn't