# Zulip Chat Archive

## 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?

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

No..

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

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):

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 (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
```

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

I'm skeptical.

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

Does `change _ ≤ v \alpha.1`

change the goal?

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

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,
rw add_eq_zero_iff' 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):

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 (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):

Adam Topaz said:

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