Zulip Chat Archive

Stream: general

Topic: cases on wrapper type


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:36):

cases doesn't have using

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:36):

induction has it though

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:36):

it basically never works, but try it anyway

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:36):

induction has it, but will not let you using it

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:37):

It does!

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:37):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:37):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:37):

I just use refine

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 26 2019 at 14:06):

Ha, probably it should.

view this post on Zulip Johan Commelin (Feb 26 2019 at 14:07):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 14:11):

@Chris Hughes I pushed an update (-;


Last updated: May 13 2021 at 21:12 UTC