## Stream: new members

### Topic: subtype issues

#### 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!

#### Kevin Buzzard (Dec 19 2019 at 21:48):

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

#### Kevin Buzzard (Dec 19 2019 at 21:48):

There's some coercion going on?

#### 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?

#### 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?

#### 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


#### 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 := _ }


#### 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 := _ }


#### 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?

#### Kevin Buzzard (Dec 19 2019 at 22:14):

That's subtype.ext.2

#### Kevin Buzzard (Dec 19 2019 at 22:14):

no, it's subtype.ext.1

#### Kevin Buzzard (Dec 19 2019 at 22:14):

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

#### 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


#### 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


#### 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


#### 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⟩

#### Kevin Buzzard (Dec 19 2019 at 22:21):

They're equal because of a theorem.

#### 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.

#### 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

#### Kevin Buzzard (Dec 19 2019 at 22:25):

If you have x you can rewrite with it

#### 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?

#### Kevin Buzzard (Dec 19 2019 at 22:29):

Again this is just subtype.ext.1

#### 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


#### Kevin Buzzard (Dec 19 2019 at 22:30):

which boils down to congr_arg

#### 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


#### 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.

#### 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 =

#### 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.

#### 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


#### Kevin Buzzard (Dec 19 2019 at 22:42):

All of those can be proved with rw h

#### Kevin Buzzard (Dec 19 2019 at 22:43):

Or by congr_arg.

#### 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

#### 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⟩


#### 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


#### Kevin Buzzard (Dec 19 2019 at 22:50):

It's difficult to know exactly what you want.

#### 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.

#### Adam Topaz (Dec 19 2019 at 22:51):

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

#### 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.

#### Kevin Buzzard (Dec 19 2019 at 22:52):

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

#### Kevin Buzzard (Dec 19 2019 at 22:53):

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

#### 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\>

#### Kevin Buzzard (Dec 19 2019 at 22:55):

Slightly different but probably easier to use.

#### Mario Carneiro (Dec 20 2019 at 00:42):

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

#### 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