## Stream: new members

### Topic: Definitions

#### Ashvni Narayanan (Jun 28 2020 at 00:37):

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 (Jun 28 2020 at 00:42):

Does \alpha.2 work?

No..

it should

#### Adam Topaz (Jun 28 2020 at 00:49):

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

#### Reid Barton (Jun 28 2020 at 00:49):

What is the error?

#### Ashvni Narayanan (Jun 28 2020 at 00:49):

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 (Jun 28 2020 at 00:49):

Can you share an #mwe ?

#### Adam Topaz (Jun 28 2020 at 00:50):

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

#### Ashvni Narayanan (Jun 28 2020 at 00:50):

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


I'm skeptical.

#### Adam Topaz (Jun 28 2020 at 00:54):

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

Typo sorry

#### Ashvni Narayanan (Jun 28 2020 at 00:54):

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,
{
cases f,
exact f_left,
},
{
sorry,
},
{
sorry,
},
}
end
end discrete_valuation_field


#### Ashvni Narayanan (Jun 28 2020 at 00:55):

I am trying to prove the second to last sorry.

#### Ashvni Narayanan (Jun 28 2020 at 00:57):

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 (Jun 28 2020 at 00:57):

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

#### Adam Topaz (Jun 28 2020 at 00:57):

Ok so exact alpha.2 should work

#### Ashvni Narayanan (Jun 28 2020 at 00:58):

Ok so exact alpha.2 should work

Yes it does!

#### Ashvni Narayanan (Jun 28 2020 at 00:59):

Reid Barton said:

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

Apologies, must have been a typing mistake.

#### Reid Barton (Jun 28 2020 at 01:00):

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

#### Ashvni Narayanan (Jun 28 2020 at 01:01):

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

#### Ashvni Narayanan (Jun 28 2020 at 01:06):

What does \alpha.2 do?

#### Adam Topaz (Jun 28 2020 at 01:06):

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

#### Adam Topaz (Jun 28 2020 at 01:07):

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

#### Ashvni Narayanan (Jun 28 2020 at 01:10):

Oh alright, that makes sense. Thank you!

#### Adam Topaz (Jun 28 2020 at 01:33):

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 (Jul 25 2020 at 21:41):

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 (Jul 25 2020 at 21:54):

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

#### Mario Carneiro (Jul 25 2020 at 21:55):

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

#### Alexandre Rademaker (Jul 25 2020 at 21:58):

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

#### Mario Carneiro (Jul 25 2020 at 21:59):

That's let?

#### Mario Carneiro (Jul 25 2020 at 22:00):

lean doesn't have where aka let written backwards

#### Alexandre Rademaker (Jul 25 2020 at 22:06):

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 !

Last updated: May 08 2021 at 19:11 UTC