subtype issues

Stream: new members

[Adam Topaz]

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]

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

[Kevin Buzzard]

There's some coercion going on?

[Kevin Buzzard]

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]

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

[Adam Topaz]

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]

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]

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]

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]

That's subtype.ext.2

[Kevin Buzzard]

no, it's subtype.ext.1

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

They're equal because of a theorem.

[Adam Topaz]

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

[Kevin Buzzard]

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]

If you have x you can rewrite with it

[Adam Topaz]

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]

Again this is just subtype.ext.1

[Kevin Buzzard]

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]

which boils down to congr_arg

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

All of those can be proved with rw h

[Kevin Buzzard]

Or by congr_arg.

[Kevin Buzzard]

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]

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]

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]

It's difficult to know exactly what you want.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Slightly different but probably easier to use.

[Mario Carneiro]

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

[Mario Carneiro]

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]