T

Stream: new members

[Ashvni Narayanan]

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]

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]

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]

Is there a way of making cases for a goal?

[Alex J. Best]

Can you give an example?

[Anatole Dedecker]

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

[Ashvni Narayanan]

That does not seem to be working out :(

[Bryan Gin-ge Chen]

#mwe ?

[Ashvni Narayanan]

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

[Alex J. Best]

(deleted)

[Jalex Stark]

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'

[Ashvni Narayanan]

Edited

[Alex J. Best]

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

[Alex J. Best]

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]

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]

did you read the error?

[Ashvni Narayanan]

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

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Ashvni Narayanan]

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]

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