cases on wrapper type

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

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]

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]

cases doesn't have using

[Mario Carneiro]

induction has it though

[Mario Carneiro]

it basically never works, but try it anyway

[Patrick Massot]

induction has it, but will not let you using it

[Johan Commelin]

It does!

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

I just use refine

[Johan Commelin]

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

[Chris Hughes]

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]

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]

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]

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]

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]

Ha, probably it should.

[Johan Commelin]

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

[Johan Commelin]

@Chris Hughes I pushed an update (-;