Zulip Chat Archive

Stream: new members

Topic: T


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ashvni Narayanan (Jun 23 2020 at 21:23):

Is there a way of making cases for a goal?

view this post on Zulip Alex J. Best (Jun 23 2020 at 21:25):

Can you give an example?

view this post on Zulip Anatole Dedecker (Jun 23 2020 at 21:26):

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

view this post on Zulip Ashvni Narayanan (Jun 23 2020 at 21:27):

That does not seem to be working out :(

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2020 at 21:28):

#mwe ?

view this post on Zulip 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

view this post on Zulip Alex J. Best (Jun 23 2020 at 21:33):

(deleted)

view this post on Zulip 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'

view this post on Zulip Ashvni Narayanan (Jun 23 2020 at 21:47):

Edited

view this post on Zulip Alex J. Best (Jun 23 2020 at 21:49):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jun 23 2020 at 21:56):

did you read the error?

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jun 23 2020 at 21:58):

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

view this post on Zulip 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

view this post on Zulip Ashvni Narayanan (Jun 23 2020 at 22:03):

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

view this post on Zulip 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!

view this post on Zulip 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: May 12 2021 at 23:13 UTC