## Stream: general

### Topic: cases on wrapper type

#### Johan Commelin (Feb 11 2019 at 19:03):

We have

def with_zero X := option X

instance has_zero (with_zero X) := \< none \>

instance has_coe X (with_zero X) := \< some \>


Now, if I have x : with_zero X, and I run cases x,
I get two cases, none or some x. However, this means that the option-type is leaking through. I already have a ton of simp-lemmas and other API in the form of zero and coercions: 0 and \u x. Can I somehow produce cases that manifestly stay in the with_zero world, instead of leaking into the option world?

#### Johan Commelin (Feb 26 2019 at 10:21):

I'm currently cleaning up a lot of with_zero stuff. What is the correct thing to do here?

#### Johan Commelin (Feb 26 2019 at 10:21):

Does this mean that cases x if just a "bad tactic move" if x : with_zero X?

#### Johan Commelin (Feb 26 2019 at 10:22):

And instead people should use some lemma from an extensive API that is built to prevent this leakage?

#### Chris Hughes (Feb 26 2019 at 10:27):

Could you write a with_top.cases_on lemma and do cases ... using with_top.cases_on?

#### Johan Commelin (Feb 26 2019 at 10:28):

Hmmm, maybe that works. I will try in a moment.
It would be nice if cases could pick up this cases_on lemma by itself.

#### Johan Commelin (Feb 26 2019 at 10:36):

lemma one_div_eq_inv [group α] (x : with_zero α) : 1 / x = x⁻¹ :=
begin
cases x using with_zero.cases_on, -- red lines under "using"
refl,
show (_ * _) = _,
simp
end


error: invalid 'begin-end' expression, ',' expected

#### Mario Carneiro (Feb 26 2019 at 10:36):

cases doesn't have using

#### Mario Carneiro (Feb 26 2019 at 10:36):

induction has it though

#### Mario Carneiro (Feb 26 2019 at 10:36):

it basically never works, but try it anyway

#### Patrick Massot (Feb 26 2019 at 10:36):

induction has it, but will not let you using it

It does!

#### Johan Commelin (Feb 26 2019 at 10:37):

The labels or a bit of though case a and case a. But anyway, that works.

#### Johan Commelin (Feb 26 2019 at 10:37):

Too bad that you can't use cases. It reads more natural to me.

#### Mario Carneiro (Feb 26 2019 at 10:37):

I just use refine

#### Johan Commelin (Feb 26 2019 at 10:41):

In fact, induction does the right thing, whereas apply/refine give me stupid goals that are false.

#### Chris Hughes (Feb 26 2019 at 13:11):

If you revert everything that depends on the variable you're doing cases on first, refine works. But that is a bit long.

#### Johan Commelin (Feb 26 2019 at 13:24):

I've now resorted to writing the proofs using pattern matching. I think it's quite nice that way:

lemma one_div : ∀ (x : with_zero α), 1 / x = x⁻¹
| 0       := rfl
| (a : α) := show _ * _ = _, by simp


#### Patrick Massot (Feb 26 2019 at 13:25):

After the fight over lifts this morning, Johan has been secretly taken down and replaced by a computer scientist. I fear my time will come soon.

#### Kevin Buzzard (Feb 26 2019 at 14:04):

I think this is OK for proofs but if you use it for definitions then there will be trouble with unfolding. Or something.

#### Chris Hughes (Feb 26 2019 at 14:06):

I've now resorted to writing the proofs using pattern matching. I think it's quite nice that way:

lemma one_div : ∀ (x : with_zero α), 1 / x = x⁻¹
| 0       := rfl
| (a : α) := show _ * _ = _, by simp


What's the definition of /? Shouldn't this proof be one_mul?

#### Johan Commelin (Feb 26 2019 at 14:06):

Ha, probably it should.

#### Johan Commelin (Feb 26 2019 at 14:07):

@Kevin Buzzard Again, that is us fighting the system... It ought to just work.

#### Johan Commelin (Feb 26 2019 at 14:11):

@Chris Hughes I pushed an update (-;

Last updated: May 13 2021 at 21:12 UTC