Zulip Chat Archive

Stream: general

Topic: the most pointless construction


Kenny Lau (Feb 23 2019 at 01:15):

I constructed the left adjoint of the forgetful functor from (the category of fields with 0^-1 = 0) to (the category of nonzero comm rings where every element is a unit)

Johan Commelin (Feb 23 2019 at 05:30):

Awesome... ...

Johan Commelin (Feb 23 2019 at 05:31):

That's an equivalence. But not constructively so? I don't know. Whatever :grinning:

Kenny Lau (Feb 23 2019 at 09:23):

Sneak peak:

inductive pre_to_field : Type u
| of : α  pre_to_field
| add : pre_to_field  pre_to_field  pre_to_field
| mul : pre_to_field  pre_to_field  pre_to_field
| inv : pre_to_field  pre_to_field

def mk (x : α) : to_field α :=
pre_to_field.of x

theorem mk.bijective : function.bijective (@mk α _ _) :=
⟨λ x y H, let z, hxz, hyz := quotient.exact H in eq.trans hxz hyz.symm,
λ x, quotient.induction_on x $ λ p, let z, hz := pre_to_field.unique_rel p in
z, quotient.sound z, rfl, hz.1⟩⟩⟩

def eval {β : Type v} [field' β] (f : α  β) [is_ring_hom f] (p : to_field α) : β :=
quotient.lift_on p (pre_to_field.eval f) $ λ p q x, hpx, hqx,
by rw [pre_to_field.eval_of_rel f hpx, pre_to_field.eval_of_rel f hqx]

Mario Carneiro (Feb 23 2019 at 09:36):

is this the free meadow?

Johan Commelin (Feb 23 2019 at 09:37):

I never understood why "champ algebrique" was translated into English as "algebraic stack" instead of "algebraic acre".

Kenny Lau (Feb 23 2019 at 10:27):

@Mario Carneiro does this have its place in mathlib?

Kenny Lau (Feb 23 2019 at 10:27):

we can redefine the reals to have "computable" inverse :P

Mario Carneiro (Feb 23 2019 at 11:39):

what's field'?

Kenny Lau (Feb 23 2019 at 11:39):

good question

Kenny Lau (Feb 23 2019 at 11:40):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/field'

Kenny Lau (Feb 23 2019 at 11:40):

see this thread :P

Mario Carneiro (Feb 23 2019 at 11:40):

what's to_field?

Kenny Lau (Feb 23 2019 at 11:40):

def to_field [ring α] [is_division_ring α] : Type u :=
quotient (pre_to_field.setoid α)

Mario Carneiro (Feb 23 2019 at 11:43):

I think field' should be discrete_field

Kenny Lau (Feb 23 2019 at 11:44):

I don't think so

Kenny Lau (Feb 23 2019 at 11:44):

because we don't assume modules, abelian groups, rings, semirings, etc, to have decidable equality

Mario Carneiro (Feb 23 2019 at 11:50):

that's true, but decidability is sort of part of a field - it's basically impossible to define a field structure without decidable equality

Kenny Lau (Feb 23 2019 at 11:51):

I just did it :P

Mario Carneiro (Feb 23 2019 at 11:52):

what about 0 != 1? What's pre_to_field.setoid?

Kenny Lau (Feb 23 2019 at 11:53):

import algebra.ring

universes u v

variables (α : Type u)

class is_division_ring [ring α] : Prop :=
(exists_inv :  {x : α}, x  0   y, x * y = 1)

section
set_option old_structure_cmd true
class field' (α : Type u) extends division_ring α, comm_ring α :=
(inv_zero : (0:α)⁻¹ = 0)
end

theorem inv_zero' [field' α] : (0:α)⁻¹ = 0 :=
field'.inv_zero α

theorem mul_eq_one_comm {α} [ring α] [is_division_ring α] {x y : α} (hxy : x * y = 1) : y * x = 1 :=
classical.by_cases
  (assume hy0 : y = 0, by rw [ hxy, hy0, zero_mul, mul_zero])
  (assume hy0 : y  0, let z, hz := is_division_ring.exists_inv hy0 in
    by rw [ mul_one x,  hz,  mul_assoc x, hxy, one_mul])

inductive pre_to_field : Type u
| of : α  pre_to_field
| add : pre_to_field  pre_to_field  pre_to_field
| mul : pre_to_field  pre_to_field  pre_to_field
| inv : pre_to_field  pre_to_field

namespace pre_to_field

variables {α}

def rel [semiring α] : (pre_to_field α)  α  Prop
| (of p)    z := p = z
| (add p q) z :=  x y, rel p x  rel q y  x + y = z
| (mul p q) z :=  x y, rel p x  rel q y  x * y = z
| (inv p)   z := rel p 0  z = 0   x, rel p x  x * z = 1

def neg [has_neg α] : pre_to_field α  pre_to_field α
| (of p)    := of (-p)
| (add x y) := add (neg x) (neg y)
| (mul x y) := mul (neg x) y
| (inv x)   := inv (neg x)

theorem rel_neg [ring α] : Π {p} {z : α}, rel p z  rel (neg p) (-z)
| (of p)    z hpz                   := congr_arg has_neg.neg hpz
| (add p q) z x, y, hpx, hqy, hxyz := ⟨-x, -y, rel_neg hpx, rel_neg hqy, by rw [ hxyz, neg_add]
| (mul p q) z x, y, hpx, hqy, hxyz := ⟨-x, y, rel_neg hpx, hqy, by rw [ hxyz, neg_mul_eq_neg_mul]
| (inv p)   z (or.inl hp0, hz0)    := or.inl ⟨@neg_zero α _  rel_neg hp0, neg_eq_zero.2 hz0
| (inv p)   z (or.inr x, hpx, hxz) := or.inr ⟨-x, rel_neg hpx, by rw [neg_mul_neg, hxz]

variables [ring α] [is_division_ring α]

lemma unique_rel (p : pre_to_field α) :
  ∃!x, rel p x :=
pre_to_field.rec_on p
  (λ x, x, rfl, λ y hxy, hxy.symm)
  (λ p q x, hpx, hpx2 y, hqy, hqy2, x+y, x, y, hpx, hqy, rfl,
    λ z x', y', hpx', hqy', hxyz, hpx2 x' hpx'  hqy2 y' hqy'  hxyz.symm)
  (λ p q x, hpx, hpx2 y, hqy, hqy2, x*y, x, y, hpx, hqy, rfl,
    λ z x', y', hpx', hqy', hxyz, hpx2 x' hpx'  hqy2 y' hqy'  hxyz.symm)
  (λ p x, hpx, hpx2, classical.by_cases
    (assume hx0 : x = 0, 0, or.inl hx0  hpx, rfl, λ y hy,
      or.cases_on hy and.right $ λ z, hpz, hzy,
      by rw [ one_mul y,  hzy, hpx2 z hpz, hx0, zero_mul, zero_mul])
    (assume hx0 : x  0, let y, hxy := is_division_ring.exists_inv hx0 in
      y, or.inr x, hpx, hxy, λ z hz, or.cases_on hz
        (λ hp0, hz0, by rw [hz0,  one_mul y,  hxy,  hpx2 0 hp0, zero_mul, zero_mul])
        (λ s, hps, hsz, by rw [ mul_one y,  hsz,  mul_assoc, hpx2 s hps, mul_eq_one_comm hxy, one_mul])))

variables {β : Type v}

def eval [division_ring β] (f : α  β) : pre_to_field α  β
| (of p)    := f p
| (add x y) := eval x + eval y
| (mul x y) := eval x * eval y
| (inv p)   := (eval p)⁻¹

theorem eval_of_rel [field' β] (f : α  β) [is_ring_hom f] :
  Π {p} {x : α} (hpx : pre_to_field.rel p x), eval f p = f x
| (of p)    z hpz                   := congr_arg f hpz
| (add p q) z x, y, hpx, hqy, hxyz := by rw [eval, eval_of_rel hpx, eval_of_rel hqy,  hxyz, is_ring_hom.map_add f]
| (mul p q) z x, y, hpx, hqy, hxyz := by rw [eval, eval_of_rel hpx, eval_of_rel hqy,  hxyz, is_ring_hom.map_mul f]
| (inv p)   z (or.inl hp0, hz0)    := by rw [eval, eval_of_rel hp0, hz0, is_ring_hom.map_zero f, inv_zero']
| (inv p)   z (or.inr x, hpx, hxz) := by rw [eval, eval_of_rel hpx,  mul_one (f x)⁻¹,  is_ring_hom.map_one f,
     hxz, is_ring_hom.map_mul f,  mul_assoc,
    inv_mul_cancel (assume hfx : f x = 0, @zero_ne_one β _ $
      by rw [ is_ring_hom.map_one f,  hxz, is_ring_hom.map_mul f, hfx, zero_mul]),
    one_mul]

variables (α)

instance : setoid (pre_to_field α) :=
{ r := λ p q,  x, rel p x  rel q x,
  iseqv := ⟨λ p, let x, hx := unique_rel p in x, hx.1, hx.1,
    λ p q x, hpx, hqx, x, hqx, hpx,
    λ p q r x, hpx, hqx y, hqy, hry, x, hpx, unique_of_exists_unique (unique_rel q) hqy hqx  hry⟩⟩ }

end pre_to_field


def to_field [ring α] [is_division_ring α] : Type u :=
quotient (pre_to_field.setoid α)

namespace to_field

variables {α} [ring α] [is_division_ring α]

def mk (x : α) : to_field α :=
pre_to_field.of x

variables (α)

theorem mk.bijective : function.bijective (@mk α _ _) :=
⟨λ x y H, let z, hxz, hyz := quotient.exact H in eq.trans hxz hyz.symm,
λ x, quotient.induction_on x $ λ p, let z, hz := pre_to_field.unique_rel p in
z, quotient.sound z, rfl, hz.1⟩⟩⟩

instance : has_add (to_field α) :=
⟨λ x y, quotient.lift_on₂ x y (λ p q, pre_to_field.add p q) $ λ p q r s x, hpx, hrx y, hqy, hsy, quotient.sound
x + y, x, y, hpx, hqy, rfl, x, y, hrx, hsy, rfl⟩⟩⟩

instance : has_neg (to_field α) :=
⟨λ x, quotient.lift_on x (λ p, pre_to_field.neg p) $ λ p q x, hpx, hqx, quotient.sound
⟨-x, pre_to_field.rel_neg hpx, pre_to_field.rel_neg hqx⟩⟩

instance : has_mul (to_field α) :=
⟨λ x y, quotient.lift_on₂ x y (λ p q, pre_to_field.mul p q) $ λ p q r s x, hpx, hrx y, hqy, hsy, quotient.sound
x * y, x, y, hpx, hqy, rfl, x, y, hrx, hsy, rfl⟩⟩⟩

instance : has_inv (to_field α) :=
⟨λ x, quotient.lift_on x (λ p, pre_to_field.inv p) $ λ p q x, hpx, hqx, quotient.sound $
classical.by_cases
  (assume hx0 : x = 0, 0, or.inl hx0  hpx, rfl, or.inl hx0  hqx, rfl⟩⟩)
  (assume hx0 : x  0, let y, hy := is_division_ring.exists_inv hx0 in y, or.inr x, hpx, hy, or.inr x, hqx, hy⟩⟩)

variables {α}

@[elab_as_eliminator] protected lemma induction_on
  {C : to_field α  Prop} (x : to_field α)
  (ih :  z, C (mk z)) : C x :=
let z, hz := (mk.bijective α).2 x in hz  ih z

@[elab_as_eliminator] protected lemma induction_on₂
  {C : to_field α  to_field α  Prop} (x y : to_field α)
  (ih :  p q, C (mk p) (mk q)) : C x y :=
to_field.induction_on x $ λ p, to_field.induction_on y $ λ q, ih p q

@[elab_as_eliminator] protected lemma induction_on₃
  {C : to_field α  to_field α  to_field α  Prop} (x y z : to_field α)
  (ih :  p q r, C (mk p) (mk q) (mk r)) : C x y z :=
to_field.induction_on x $ λ p, to_field.induction_on y $ λ q, to_field.induction_on z $ λ r, ih p q r

@[simp] lemma mk_add (x y : α) : mk (x + y) = mk x + mk y :=
quotient.sound x + y, rfl, x, y, rfl, rfl, rfl⟩⟩

@[simp] lemma mk_neg (x : α) : mk (-x) = -mk x := rfl

@[simp] lemma mk_mul (x y : α) : mk (x * y) = mk x * mk y :=
quotient.sound x * y, rfl, x, y, rfl, rfl, rfl⟩⟩

lemma mk_inv {x y : α} (hxy : x * y = 1) : (mk x)⁻¹ = mk y :=
quotient.sound y, or.inr x, rfl, hxy, rfl

variables (α)
instance : ring (to_field α) :=
{ zero := mk 0,
  one := mk 1,
  add_assoc := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [ mk_add,  mk_add,  mk_add,  mk_add, add_assoc],
  zero_add := λ x, to_field.induction_on x $ λ p,
    by rw [ mk_add, zero_add],
  add_zero := λ x, to_field.induction_on x $ λ p,
    by rw [ mk_add, add_zero],
  add_left_neg := λ x, to_field.induction_on x $ λ p,
    by rw [ mk_neg,  mk_add, add_left_neg]; refl,
  add_comm := λ x y, to_field.induction_on₂ x y $ λ p q,
    by rw [ mk_add,  mk_add, add_comm],
  mul_assoc := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [ mk_mul,  mk_mul,  mk_mul,  mk_mul, mul_assoc],
  one_mul := λ x, to_field.induction_on x $ λ p,
    by rw [ mk_mul, one_mul],
  mul_one := λ x, to_field.induction_on x $ λ p,
    by rw [ mk_mul, mul_one],
  left_distrib := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [ mk_add,  mk_mul,  mk_mul,  mk_mul,  mk_add, mul_add],
  right_distrib := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [ mk_add,  mk_mul,  mk_mul,  mk_mul,  mk_add, add_mul],
  .. to_field.has_add α,
  .. to_field.has_neg α,
  .. to_field.has_mul α }

@[simp] lemma mk_zero : mk (0 : α) = 0 := rfl
@[simp] lemma mk_one : mk (1 : α) = 1 := rfl

instance mk.is_ring_hom : is_ring_hom (@mk α _ _) :=
mk_one α, mk_mul, mk_add

variables {α}
def eval {β : Type v} [field' β] (f : α  β) [is_ring_hom f] (p : to_field α) : β :=
quotient.lift_on p (pre_to_field.eval f) $ λ p q x, hpx, hqx,
by rw [pre_to_field.eval_of_rel f hpx, pre_to_field.eval_of_rel f hqx]

instance eval.is_ring_hom {β : Type v} [field' β] (f : α  β) [is_ring_hom f] : is_ring_hom (eval f) :=
by convert is_ring_hom.map_one f,
λ p q, quotient.induction_on₂ p q $ λ x y, rfl,
λ p q, quotient.induction_on₂ p q $ λ x y, rfl

end to_field

namespace to_field

instance [comm_ring α] [is_division_ring α] : comm_ring (to_field α) :=
{ mul_comm := λ x y, to_field.induction_on₂ x y $ λ p q,
    by rw [ mk_mul,  mk_mul, mul_comm],
  .. to_field.ring α }

instance [nonzero_comm_ring α] [is_division_ring α] : field (to_field α) :=
{ zero_ne_one := λ H, zero_ne_one $ (mk.bijective α).1 H,
  mul_inv_cancel := λ x, to_field.induction_on x $ λ p hp0,
    let y, hy := is_division_ring.exists_inv (mt (congr_arg mk) hp0) in
    by rw [mk_inv hy,  mk_mul, hy, mk_one],
  inv_mul_cancel := λ x, to_field.induction_on x $ λ p hp0,
    let y, hy := is_division_ring.exists_inv (mt (congr_arg mk) hp0) in
    by rw [mk_inv hy,  mk_mul, mul_eq_one_comm hy, mk_one],
  .. to_field.comm_ring α,
  .. to_field.has_inv α }

end to_field

Kenny Lau (Feb 23 2019 at 11:54):

oh and to give a concrete example: the Cauchy sequence construction of the real numbers allow you to define it as a ring constructively; then to_field real would be an example of a field where the inverse of 0 is 0, but it has no decidable equality.

Chris Hughes (Feb 23 2019 at 11:56):

But you can't do it with computable inverses is the point I think.

Kenny Lau (Feb 23 2019 at 11:56):

to_field real has computable inverse, inv zero = zero, and no decidable equality

Mario Carneiro (Feb 23 2019 at 11:58):

I see a classical.by_cases in there though

Kenny Lau (Feb 23 2019 at 11:58):

classical.by_cases is computable

Mario Carneiro (Feb 23 2019 at 11:58):

In order to work with the axioms of a division ring you don't actually need decidable eq but rather eq LEM

Mario Carneiro (Feb 23 2019 at 11:59):

but we don't have a typeclass for that

Kenny Lau (Feb 23 2019 at 12:00):

I just find it inconvenient that the inverse of zero is left unspecified in field (which makes subfield weird, as seen in #742), and too strict that discrete_field requires decidable equality

Kenny Lau (Feb 23 2019 at 12:01):

I think field' is the correct structure

Mario Carneiro (Feb 23 2019 at 12:02):

I agree that field is stupid, that's why I've been telling everyone to use discrete_field instead

Kenny Lau (Feb 23 2019 at 12:03):

but we don't assume add_comm_group or semiring or module to have decidable equality either, so decidable equality seems too strong

Mario Carneiro (Feb 23 2019 at 12:03):

That's because none of those have case analysis on equaling zero

Mario Carneiro (Feb 23 2019 at 12:04):

I think the proper constructive analogue of field is ring

Mario Carneiro (Feb 23 2019 at 12:06):

Also, we do have plenty of structures that assume decidable equality, specifically the order structures

Mario Carneiro (Feb 23 2019 at 12:06):

decidable_linear_ordered_semigroup and so on

Kenny Lau (Feb 23 2019 at 12:07):

but the category of discrete rings is not closed under direct limit

Mario Carneiro (Feb 23 2019 at 12:08):

is the category of fields?

Kenny Lau (Feb 23 2019 at 12:08):

yes

Mario Carneiro (Feb 23 2019 at 12:08):

in that case, I have no idea what you are talking about

Kenny Lau (Feb 23 2019 at 12:08):

what?

Mario Carneiro (Feb 23 2019 at 12:09):

I don't have any conception of how direct limits work

Mario Carneiro (Feb 23 2019 at 12:09):

or what the issues are

Kenny Lau (Feb 23 2019 at 12:09):

https://github.com/leanprover-community/mathlib/blob/cf8a619bde24d327387dd7321a8da55fd3bbd585/src/algebra/direct_limit.lean#L503-L555

Kenny Lau (Feb 23 2019 at 12:10):

the issue is that to_field works great with direct limit

Kenny Lau (Feb 23 2019 at 12:10):

the category of field is closed under direct limit

Kenny Lau (Feb 23 2019 at 12:10):

and the category of discrete field might also be (I haven't thought about it)

Kenny Lau (Feb 23 2019 at 12:10):

but the category of discrete rings, I'm 50% certain that it must not be closed under direct limit

Mario Carneiro (Feb 23 2019 at 12:11):

I didn't say anything about discrete rings though

Kenny Lau (Feb 23 2019 at 12:11):

so you think that field' should not even exist?

Mario Carneiro (Feb 23 2019 at 12:11):

I'm asserting that all interesting fields are decidable

Kenny Lau (Feb 23 2019 at 12:11):

and I gave you a concrete counter-example

Kenny Lau (Feb 23 2019 at 12:11):

there's no way to make real decidable

Mario Carneiro (Feb 23 2019 at 12:12):

You want a different structure than field'... you want a ring where inverses exist

Mario Carneiro (Feb 23 2019 at 12:12):

exist in the weak sense

Kenny Lau (Feb 23 2019 at 12:12):

well then theorems become a bit clumsy

Kenny Lau (Feb 23 2019 at 12:13):

so no that's not what I want

Mario Carneiro (Feb 23 2019 at 12:14):

to_field gives you a way to explicitly refer to these elements that are only known to exist propositionally

Mario Carneiro (Feb 23 2019 at 12:14):

but the cost is that you "only" get a bijection rather than an equiv

Kenny Lau (Feb 23 2019 at 12:15):

is there a situation where the hypothetical inverse function to_field real -> real is helpful?

Mario Carneiro (Feb 23 2019 at 12:17):

sure... if you want to talk about the inverse of a real number

Kenny Lau (Feb 23 2019 at 12:17):

I mean, let's say we replaced real with to_field real

Kenny Lau (Feb 23 2019 at 12:17):

everywhere in mathlib

Kenny Lau (Feb 23 2019 at 12:17):

so the canonical structure of the real numbers is a field where the inverse of zero is zero, without decidable equality

Kenny Lau (Feb 23 2019 at 12:18):

also I think the category of discrete fields is not closed under direct limit

Mario Carneiro (Feb 23 2019 at 12:19):

The real numbers are a quotient of Cauchy sequences. to_field real is a quotient of field expressions with constants in real... so it's like you just adjoined inverses for everything

Kenny Lau (Feb 23 2019 at 12:19):

you never use the Cauchy sequences anyway

Mario Carneiro (Feb 23 2019 at 12:19):

How do you define the supremum?

Kenny Lau (Feb 23 2019 at 12:19):

ok let's put this in context

Kenny Lau (Feb 23 2019 at 12:19):

what should I replace https://github.com/leanprover-community/mathlib/blob/cf8a619bde24d327387dd7321a8da55fd3bbd585/src/algebra/direct_limit.lean#L503-L555 by?

Kenny Lau (Feb 23 2019 at 12:20):

I definitely want direct limit of fields

Kenny Lau (Feb 23 2019 at 12:20):

so don't tell me replace it with EOF

Mario Carneiro (Feb 23 2019 at 12:20):

go classical, man

Kenny Lau (Feb 23 2019 at 12:20):

classical != noncomputable

Mario Carneiro (Feb 23 2019 at 12:20):

go noncomputable, man

Kenny Lau (Feb 23 2019 at 12:20):

really?

Mario Carneiro (Feb 23 2019 at 12:21):

if it requires you to invent entirely new algebraic structures just to get this theorem, yes it seems like a valid approach

Kenny Lau (Feb 23 2019 at 12:21):

what's wrong with inventing new algebraic structures

Mario Carneiro (Feb 23 2019 at 12:21):

well you have to make sure they play well with everything else

Mario Carneiro (Feb 23 2019 at 12:22):

particularly if you are planning on replacing the original

Mario Carneiro (Feb 23 2019 at 12:23):

I should say that I am actually quite impressed with the whole construction; I didn't know this was possible until you showed me

Kenny Lau (Feb 23 2019 at 12:23):

thanks for your appreciation

Mario Carneiro (Feb 23 2019 at 12:24):

But I'm 110% sure kevin will say you are wasting your time

Kenny Lau (Feb 23 2019 at 12:25):

... on a more related note, does this have its place in mathlib?

Kenny Lau (Feb 23 2019 at 12:25):

class is_division_ring [ring α] : Prop :=
(exists_inv :  {x : α}, x  0   y, x * y = 1)

Mario Carneiro (Feb 23 2019 at 12:27):

This seems a bit easier to deal with. This is what division rings should have been

Mario Carneiro (Feb 23 2019 at 12:28):

IIUC real is a division ring in this sense

Kenny Lau (Feb 23 2019 at 12:31):

so in which file should I put this?

Kevin Buzzard (Feb 23 2019 at 12:42):

(wasting your time) -- I simply do not understand the issues here and with things like this I only attempt to understand the issues when they actually affect my own work (like I never understood why lean treated quotients differently from equivalence classes until it began to matter to me). I'm not sure this will ever matter to me but I can quite believe there is a discussion to be had

Sebastien Gouezel (Feb 23 2019 at 14:30):

Why shouldn't we assume that all our structures have decidable equality? I am sure there are interesting things to be discussed here, but I don't really get them. I think what I would like to see is a concrete example where it creates a problem to assume decidable equality everywhere.

Mario Carneiro (Feb 23 2019 at 15:50):

I think the main problem is that this can make definitions noncomputable when they should be computable, e.g. rational arithmetic

Mario Carneiro (Feb 23 2019 at 15:50):

and this can block some rfl proofs of trivial facts

Mario Carneiro (Feb 23 2019 at 15:51):

(that's the pragmatic answer; there might also be religious reasons)

Sebastien Gouezel (Feb 23 2019 at 16:30):

I am very much interested in pragmatic answers, thanks. And what if general decidable equality is declared with priority 0, and specific computable instances are declared with higher priority, say 50. Would that still block anything?

Mario Carneiro (Feb 23 2019 at 16:32):

The problem isn't so much with finding the wrong instance as it is with intermediate constructions being more classical than they could be with more care

Mario Carneiro (Feb 23 2019 at 16:33):

i.e. if you use that int is a ring then you are depending on the axiom of choice, because an intermediate step decided not to use decidable equality when it was available

Sebastien Gouezel (Feb 23 2019 at 17:02):

I still don't get why it could be important in proofs, since they are irrelevant anyway. In definitions where one might want to compute, sure. But my question is even more pragmatic: if one removed everything about linear_order in mathlib, using only decidable_linear_order everywhere, would that break something? If one assumed in the very definition of ring, and group, and everything, that equality is decidable, would that break something?

Kenny Lau (Feb 23 2019 at 17:08):

"Proofs are irrelevant" -- every Lean user ever

Johannes Hölzl (Feb 23 2019 at 17:54):

Lean 3 users, there is still HoTT Lean

Johannes Hölzl (Feb 23 2019 at 17:56):

But I would also prefer to add decidability to most things: (additive) semigroups, orders etc.

Sebastien Gouezel (Feb 23 2019 at 18:11):

"Proofs are irrelevant" -- every Lean user ever

This quote is crazy, and I can't believe I said it myself. Don't tell that to my fellow mathematicians, please.


Last updated: Dec 20 2023 at 11:08 UTC