# Zulip Chat Archive

## 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:52):

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

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