Stream: new members

Topic: T

Ashvni Narayanan (Jun 23 2020 at 21:10):

I am trying to show that, in with_top \Z , T \neq 0.

rw <-with_top.coe_zero,
/-apply with_top.top_ne_zero,  does not work out-/
/-apply with_top.none_lt_some, does not work out -/
exfalso,
/-apply with_top.zero_lt_top,  dows not work out-/
apply with_top.top_ne_coe,


does not work. This code gives me 3 goals,

⊢ ⊤ = ↑?m_2
⊢ Type ?
⊢ ?m_1


I don't know how to solve this. Any help is appreciated. Thank you!

Alex J. Best (Jun 23 2020 at 21:14):

This works:

example : (⊤ : with_top ℤ) ≠ 0:=
begin
rintro ⟨⟩,  -- you can do intro h, then cases h, or combine this into the line here
end


Alex J. Best (Jun 23 2020 at 21:16):

The idea is that with_top \Z has two constructors, one from an element of \Z or \top, which are then the two possible (disjoint) cases for what an element of with_top \Z can be. cases splits into the different possibilities for the equality, but in this case there are none, so intro h, cases h does it, using rintro instead is just a fancy lazy (shorter) way of doing the same thing.

Ashvni Narayanan (Jun 23 2020 at 21:23):

Is there a way of making cases for a goal?

Alex J. Best (Jun 23 2020 at 21:25):

Can you give an example?

Anatole Dedecker (Jun 23 2020 at 21:26):

I think what you want is split, but not sure of what you're looking for

Ashvni Narayanan (Jun 23 2020 at 21:27):

That does not seem to be working out :(

#mwe ?

Ashvni Narayanan (Jun 23 2020 at 21:32):

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

universe u

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(val : K -> with_top ℤ )
(mul : ∀ (x y : K), val(x*y) = val(x) + val(y) )
(add : ∀ (x y : K), val(x + y) ≥ min (val(x)) (val(y)) )
(non_zero : ∀ (x : K), val(x) = ⊤ ↔ x = 0 )

namespace discrete_valuation_field

definition discrete_valuation_field.valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top ℤ := discrete_valuation_field.val

variables {K : Type*} [field K] [discrete_valuation_field K]

lemma with_top.cases (a : with_top ℤ) : a = ⊤ ∨ ∃ n : ℤ, a = n :=
begin
cases a with n,
{ -- a = ⊤ case
left,
refl, -- true by definition
},
{ -- ℤ case
right,
use n,
refl, -- true by definition
}
end

lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K),
simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
rw f,
simp,
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K),
apply mul,
rw k at g,
rw g,
cases (with_top.cases (val(1:K))) with h1 h2,
rw h1,
rw h1 at g,
rw <-g,
sorry,
sorry,
end


(deleted)

Jalex Stark (Jun 23 2020 at 21:45):

in your example, this line fails for me

cases (with_top.cases (val(1:K))) with h1 h2,


with error unknown identifier 'with_top.cases'

Edited

Alex J. Best (Jun 23 2020 at 21:49):

I think you need to use non_zero in the first case.

Alex J. Best (Jun 23 2020 at 21:54):

And here is how you could use the built in cases instead of your lemma, its a bit weird though, because it writes none instead of top everywhere, so using the lemma might be nicer.

lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K),
simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
rw f,
simp,
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K),
apply mul,
rw k at g,
rw g,
cases t : val(1:K),
rw with_top.none_eq_top at t,
rw non_zero at t,
exfalso,
exact one_ne_zero t,
sorry,
end


Ashvni Narayanan (Jun 23 2020 at 21:56):

Alex J. Best said:

I think you need to use non_zero in the first case.

Oh yes, I had tried this. But some error kept coming up.

Jalex Stark (Jun 23 2020 at 21:56):

did you read the error?

Ashvni Narayanan (Jun 23 2020 at 21:58):

Well, as soon as I proved 1 \neq 0, I think g disappeared, which was no help.

Jalex Stark (Jun 23 2020 at 21:58):

you'll have less problems with "disappearing lemmas" if you use focusing braces

Jalex Stark (Jun 23 2020 at 21:59):

like this

lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K) := by simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
{ rw f, simp },
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K) := by apply mul,
rw k at g, rw g,
cases (with_top.cases (val(1:K))) with h1 h2,
{ contrapose h1,
rw discrete_valuation_field.non_zero, norm_num },
sorry
end


Ashvni Narayanan (Jun 23 2020 at 22:03):

Oh ok. I will keep that in mind. Thank you!

Ashvni Narayanan (Jun 23 2020 at 22:06):

Alex J. Best said:

And here is how you could use the built in cases instead of your lemma, its a bit weird though, because it writes none instead of top everywhere, so using the lemma might be nicer.

lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K),
simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
rw f,
simp,
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K),
apply mul,
rw k at g,
rw g,
cases t : val(1:K),
rw with_top.none_eq_top at t,
rw non_zero at t,
exfalso,
exact one_ne_zero t,
sorry,
end


Thank you!

Jalex Stark (Jun 23 2020 at 22:15):

here's what I would write. probably the thing of most interest is the use of the lift tactic.

import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization

universe u

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(val : K -> with_top ℤ )
(mul : ∀ (x y : K), val(x*y) = val(x) + val(y) )
(add : ∀ (x y : K), val(x + y) ≥ min (val(x)) (val(y)) )
(non_zero : ∀ (x : K), val(x) = ⊤ ↔ x = 0 )

namespace discrete_valuation_field

def discrete_valuation_field.valuation (K : Type*) [field K] [ discrete_valuation_field K ] :
K -> with_top ℤ := discrete_valuation_field.val

variables {K : Type*} [field K] [discrete_valuation_field K]

instance (α : Type*) : has_coe α (with_top α) := {coe := some}

instance (α : Type*) : can_lift (with_top α) α :=
begin
refine {coe := coe, cond := λ x, x ≠ ⊤, prf := _},
intros, cases x, { contrapose! a, refl },
use x, refl,
end

lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K) := by simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
{ rw f, simp },
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K) := by apply mul,
rw k at g, rw g,
lift val(1:K) to ℤ with d,
swap, { norm_num [non_zero] },
norm_cast, norm_cast at g, linarith,
end


Last updated: Dec 20 2023 at 11:08 UTC