Zulip Chat Archive

Stream: new members

Topic: subtype issues


view this post on Zulip Adam Topaz (Dec 19 2019 at 21:45):

Hi,
I'm having some issues working with propositions involving terms in a subtype.

For example, I've been playing around with subsets of fields, and I came across the following goal:

F : Type u_1,
_inst_1 : discrete_field F,
S : set F,
a_val : F,
a_property : a_val  S,
h : a_val, a_property = 0
 a_val = 0

This should be a tautology, but the assumption tactic doesn't work.
If I understand correctly the issue stems from the fact that ⟨a_val, a_property⟩ is of type { x : F // x ∈ S }. There must be some really simple way to rewrite h as a_val = 0. Any help would me much appreciated!

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 21:48):

I wonder what that 0 is on the RHS of h?

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 21:48):

There's some coercion going on?

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 21:51):

It's difficult for me to figure out the type of both sides of h. In theory that zero could be defined in a completely wacky way and have nothing to do with F's zero, although this is unlikely unless you did it maliciously or by accident. Can you post the code which generated this?

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 21:54):

I guess you could do unfold zero at h to find out what's going on. Does cases h help?

view this post on Zulip Adam Topaz (Dec 19 2019 at 22:00):

Sure! I'm playing around trying to define the typeclass of multiplicative subgroups of a field, and define a group instance given something in that typeclass.
The code is below.
unfold zero at h doesn't work, and cases h doesn't work either...

While I'm at it, it's unclear to me why tactic.unfreeze_local_instances is needed. I just followed lean's suggestion here as the first step...
Also, I suppose there is a much more efficient way to go about doing this, so please forgive my naivety -- I'm still very much a beginner at this.

import ring_theory.subring

variables {F : Type*} [discrete_field F] (S : set F)

class is_mult_subgroup : Prop :=
(mul_closed :  { x y : F}, x  S  y  S  x * y  S)
(one_mem : (1 : F)  S)
(inv_mem :  {x : F}, x  S  x⁻¹  S)
(zero_nmem : (0 : F)  S)


instance is_mult_subgroup.group [ms : is_mult_subgroup S] : group S :=
begin
tactic.unfreeze_local_instances,
cases ms,
split,
intro,
cases a,
rw division_ring.inv_mul_cancel,
intro h,
sorry
end

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:04):

You're constructing data so you don't really want to be using tactic mode. You probably want to be doing something like this:

instance is_mult_subgroup.group [ms : is_mult_subgroup S] : group S :=
{ mul := _,
  mul_assoc := _,
  one := _,
  one_mul := _,
  mul_one := _,
  inv := _,
  mul_left_inv := _ }

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:06):

instance is_mult_subgroup.group [is_mult_subgroup S] : group S :=
{ mul := λ x y, x.1 * y.1, mul_closed x.2 y.2,
  mul_assoc := _,
  one := _,
  one_mul := _,
  mul_one := _,
  inv := _,
  mul_left_inv := _ }

view this post on Zulip Adam Topaz (Dec 19 2019 at 22:14):

I agree... But suppose I want to do the following:

def foo := {x : F // x  S}
example (x y : foo S) : (x = y)  (x.val = y.val) := sorry

Wouldn't similar issues pop up here?

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:14):

That's subtype.ext.2

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:14):

no, it's subtype.ext.1

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:14):

but I agree that this is trivial. Cases on x and y should do this.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:16):

example (x y : foo S) : (x = y)  (x.val = y.val) :=
begin
  intro h,
  rw h,
end

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:17):

def foo := {x : F // x  S}
example (x y : foo S) : (x = y)  (x.val = y.val) :=
begin
  exact subtype.ext.1
end

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:19):

example (x y : foo S) : (x = y)  (x.val = y.val) := by cases x; cases y; simp

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:21):

But this is a different question to your earlier question, because x is not definitionally equal to ⟨x.1, x.2⟩

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:21):

They're equal because of a theorem.

view this post on Zulip Adam Topaz (Dec 19 2019 at 22:23):

Right... I'm trying to concoct a similar example to illustrate the coercion issue using has_zero.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:24):

With your has_zero example you didn't have x and x.val, you had <a_val,a_property> and a_val which is different

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:25):

If you have x you can rewrite with it

view this post on Zulip Adam Topaz (Dec 19 2019 at 22:27):

Suppose I have foo = { x : F // x \in S } and an assumption h : (0 : F) \in S which can then be used to create an instance of has_zero for foo as (0 : foo) := < (0 : F), h >, I should then be able to prove example (x : foo) : (x = 0) \to x.val = 0. Wouldn't this cause similar issues?

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:29):

Again this is just subtype.ext.1

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:29):

variables {F : Type*} [discrete_field F] (S : set F)

def foo := {x : F // x  S}

example (x y : F) (hx : x  S) (hy : y  S) (h : (x,hx : foo S) = y,hy) : x = y :=
begin
  exact subtype.ext.1 h,
end

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:30):

which boils down to congr_arg

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:32):

example (x y : F) (hx : x  S) (hy : y  S) (h : (x,hx : foo S) = y,hy) : x = y :=
 congr_arg subtype.val h

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:37):

I agree that somehow it looks like it should be "more tautological". I guess a simpler example would just be products. If (x1,y1)=(x2,y2) then why does x1=x2? This feels like it should be true by definition but somehow the proof relies on a case analysis, you do need to apply the recursor, which is an axiom.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:38):

congr_arg is the same, it looks like it should be true by definition but the proof involves induction on =

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:38):

For stuff like this it's all just beyond my comprehension in some sense; this is foundational sludge and you just learn your way around it.

view this post on Zulip Adam Topaz (Dec 19 2019 at 22:40):

Yes, I completely understand now.

Perhaps a more general (but related) question is the following: If T is a structure type, for example of the following form:

structure T :=
(t1 : T1)
(t2 : T2)
(t3 : T3)

And I have a hypotheses of the form

x y : T
h : x = y

Is there a tactic which automatically extracts the following?

h1 : x.t1 = y.t1
h2 : x.t2 = y.t2
h3 : x.t3 = y.t3

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:42):

All of those can be proved with rw h

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:43):

Or by congr_arg.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:44):

Usually tactics prove one thing not three. The way this is dealt with usually is that this sort of thing is proved very quickly after defining the structure

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:49):

Check out the beginning of data.complex.basic:

structure complex : Type :=
(re : ) (im : )

notation `` := complex

namespace complex

@[simp] theorem eta :  z : , complex.mk z.re z.im = z
| a, b := rfl

theorem ext :  {z w : }, z.re = w.re  z.im = w.im  z = w
| zr, zi ⟨_, _⟩ rfl rfl := rfl

theorem ext_iff {z w : } : z = w  z.re = w.re  z.im = w.im :=
⟨λ H, by simp [H], and.rec ext

view this post on Zulip Adam Topaz (Dec 19 2019 at 22:49):

I see... I tried rw h in such an example with no luck, but of course congr_arg works. It might be nice to have some automation here, like how cases x can automatically provide

x_t1 : T1
x_t2 : T2
x_t3 : T3
h : { t1 := x_t1, t2 := x_t2, t3 := x_t3 } = y

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:50):

It's difficult to know exactly what you want.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:50):

There are several similar fiddly things. If you're making your own structure it's your job to make a good interface to it.

view this post on Zulip Adam Topaz (Dec 19 2019 at 22:51):

Gotcha! Thanks very much for the help! I'll keep playing around :)

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:51):

Note the first three theorems of data.complex.basic -- all completely trivial but you need them a lot.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:52):

When I was learning this stuff, making the complex numbers taught me a lot.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:52):

I might have some teaching materials about this stuff lying around somewhere...

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:53):

https://github.com/kbuzzard/xena/blob/master/lean_together/complex.lean

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:55):

My definition of conj in that file is bad, I think: it should send z to \<z.1,-z.2\>

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:55):

Slightly different but probably easier to use.

view this post on Zulip Mario Carneiro (Dec 20 2019 at 00:42):

I think cases x, cases y, congr does what you want

view this post on Zulip Mario Carneiro (Dec 20 2019 at 00:43):

ext will often provide lemmas of the form you are looking for, but it relies on theorems you have to write yourself and mark with @[extensionality]


Last updated: May 10 2021 at 00:31 UTC