Definitions

Stream: new members

[Ashvni Narayanan]

I am having trouble in unravelling definitions. The definition of val_ring K is { x : K | 0 ≤ v x } . I want to show

α b : ↥(val_ring K),
⊢ 0 ≤ v ↑α

How do I show this? Unfold does not seem to work.
Any help is appreciated. Thank you!

[Alex J. Best]

Does \alpha.2 work?

[Ashvni Narayanan]

No..

[Reid Barton]

it should

[Adam Topaz]

Is it a problem with the coersion on alpha? Did you define the restriction of v to the valuation ring?

[Reid Barton]

What is the error?

[Ashvni Narayanan]

Adam Topaz said:

Is it a problem with the coersion on alpha? Did you define the restriction of v to the valuation ring?

No, I did not

[Bryan Gin-ge Chen]

Can you share an #mwe ?

[Adam Topaz]

Sorry I'm wrong. I guess the coersion goes back to K so it should work

[Ashvni Narayanan]

Reid Barton said:

What is the error?

invalid field notation, type is not of the form (C ...) where C is a constant
  ⁇
has type
  ?m_1

[Reid Barton]

I'm skeptical.

[Adam Topaz]

Does change _ ≤ v \alpha.1 change the goal?

[Adam Topaz]

Typo sorry

[Ashvni Narayanan]

Bryan Gin-ge Chen said:

Can you share an #mwe ?

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

import tactic

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

namespace discrete_valuation_field

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

variables {K : Type*} [field K] [discrete_valuation_field K]
def val_ring (K : Type*) [field K] [discrete_valuation_field K] := { x : K | 0 ≤ v x }

lemma unit_iff_val_zero (K:Type*) [field K] [discrete_valuation_field K] [α : (val_ring K)] : v (α : K) = 0 ↔ is_unit α :=
begin
split,
{ sorry,
}
{
  rintros,
  rw is_unit_iff_exists_inv at a,
  cases a with b a,
  have f : v((α:K)*(b:K)) = v(1:K),
  {
    norm_cast,
    rw a,
    simp,
  },
  rw mul at f,
  rw val_one_is_zero at f,
  rw add_eq_zero_iff' at f,
  {
    cases f,
    exact f_left,
  },
  {
    sorry,
  },
  {
    sorry,
  },
}
end
end discrete_valuation_field

[Ashvni Narayanan]

I am trying to prove the second to last sorry.

[Ashvni Narayanan]

Adam Topaz said:

Does change _ ≤ v \alpha.1 change the goal?

It does, yes.

K : Type u_1,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K,
α b : ↥(val_ring K),
a : α * b = 1,
f : v ↑α + v ↑b = 0
⊢ 0 ≤ v α.val

[Reid Barton]

I get various other errors. For example there is a , missing.

[Adam Topaz]

Ok so exact alpha.2 should work

[Ashvni Narayanan]

Adam Topaz said:

Ok so exact alpha.2 should work

Yes it does!

[Ashvni Narayanan]

Reid Barton said:

I get various other errors. For example there is a , missing.

Apologies, must have been a typing mistake.

[Reid Barton]

Then it would have worked originally too (before change or anything).

[Ashvni Narayanan]

I got a little confused, I did not know I have to put exact. Apologies.

[Ashvni Narayanan]

What does \alpha.2 do?

[Adam Topaz]

Alpha is in the subtype associated to the set, so alpha.2 is the proof that alpha.1 is in the set

[Adam Topaz]

The coersion on alpha in your goal was the map sending alpha to alpha.1, so the goal was exactly alpha.2

[Ashvni Narayanan]

Oh alright, that makes sense. Thank you!

[Adam Topaz]

No problem. In case it comes up later, it's worthwhile to mention that another name for alpha.1 is alpha.val and another name for alpha.2 is alpha.prop. I would take a look at how subtype is defined.

[Alexandre Rademaker]

Sorry for the possible silly question. In Haskell, definitions using pattern matching can have guards and the where clause for local declarations. Does Lean have something similar? If not, do we lose anything or these can be somehow emulated without any loss of expressivity?

[Mario Carneiro]

No, lean doesn't have guards. You can mimic them using if then else

[Mario Carneiro]

Even if the equation compiler supported guards they would have to be compiled to if then else anyway

[Alexandre Rademaker]

Thanks. I am assuming that local declarations are not available too, right? But this is clearly a convenience.

[Mario Carneiro]

That's let?

[Mario Carneiro]

lean doesn't have where aka let written backwards

[Alexandre Rademaker]

Ah, yes. I just didn't figure out how the syntax of let could be used in combination with the pattern matching during function definitions. I will try again. thank you @Mario Carneiro !