Zulip Chat Archive

Stream: new members

Topic: Definitions


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

view this post on Zulip Alex J. Best (Jun 28 2020 at 00:42):

Does \alpha.2 work?

view this post on Zulip Ashvni Narayanan (Jun 28 2020 at 00:44):

No..

view this post on Zulip Reid Barton (Jun 28 2020 at 00:47):

it should

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

view this post on Zulip Reid Barton (Jun 28 2020 at 00:49):

What is the error?

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

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

Can you share an #mwe ?

view this post on Zulip Adam Topaz (Jun 28 2020 at 00:50):

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

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

view this post on Zulip Reid Barton (Jun 28 2020 at 00:51):

I'm skeptical.

view this post on Zulip Adam Topaz (Jun 28 2020 at 00:54):

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

view this post on Zulip Adam Topaz (Jun 28 2020 at 00:54):

Typo sorry

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

view this post on Zulip Ashvni Narayanan (Jun 28 2020 at 00:55):

I am trying to prove the second to last sorry.

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

view this post on Zulip Reid Barton (Jun 28 2020 at 00:57):

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

view this post on Zulip Adam Topaz (Jun 28 2020 at 00:57):

Ok so exact alpha.2 should work

view this post on Zulip Ashvni Narayanan (Jun 28 2020 at 00:58):

Adam Topaz said:

Ok so exact alpha.2 should work

Yes it does!

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

view this post on Zulip Reid Barton (Jun 28 2020 at 01:00):

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

view this post on Zulip Ashvni Narayanan (Jun 28 2020 at 01:01):

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

view this post on Zulip Ashvni Narayanan (Jun 28 2020 at 01:06):

What does \alpha.2 do?

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

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

view this post on Zulip Ashvni Narayanan (Jun 28 2020 at 01:10):

Oh alright, that makes sense. Thank you!

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

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

view this post on Zulip Mario Carneiro (Jul 25 2020 at 21:54):

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

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

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

view this post on Zulip Mario Carneiro (Jul 25 2020 at 21:59):

That's let?

view this post on Zulip Mario Carneiro (Jul 25 2020 at 22:00):

lean doesn't have where aka let written backwards

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