not a structure

Stream: general

[Kenny Lau]

import algebra.ordered_group

set_option old_structure_cmd true

/-- Extend `nonneg_add_comm_group` to support ordered rings
  specified by their nonnegative elements -/
class nonneg_ring (α : Type*) extends ring α, nonneg_add_comm_group α :=
(mul_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a * b))
(mul_pos : ∀ {a b}, pos a → pos b → pos (a * b))
(zero_ne_one : (0 : α) ≠ 1)

/-- Extend `nonneg_add_comm_group` to support linearly ordered rings
  specified by their nonnegative elements -/
class linear_nonneg_ring (α : Type*) extends domain α, nonneg_add_comm_group α :=
(mul_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a * b))
(nonneg_total : ∀ a, nonneg a ∨ nonneg (-a))

namespace nonneg_ring
variables {α : Type*} [nonneg_ring α]

def to_linear_nonneg_ring
  (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
  : linear_nonneg_ring α :=
{ nonneg_total := nonneg_total,
  eq_zero_or_eq_zero_of_mul_eq_zero := sorry,
  ..‹nonneg_ring α› }

end nonneg_ring

[Kenny Lau]

invalid structure value {...}, expected type is known, but it is not a structure
  linear_nonneg_ring α

[Kenny Lau]

the error is in the last declaration

[Kenny Lau]

somehow Lean decided that I can't use { for linear_nonneg_ring

[Mario Carneiro]

I get no errors on master

[Mario Carneiro]

you could also try

{ linear_nonneg_ring .
  nonneg_total := nonneg_total,
  eq_zero_or_eq_zero_of_mul_eq_zero := sorry,
  ..‹nonneg_ring α› }

[Kenny Lau]

invalid structure instance, 'linear_nonneg_ring' is not the name of a structure type

[Mario Carneiro]

#print linear_nonneg_ring?

[Kenny Lau]

also for some reason the definition of linear_nonneg_ring is a bit slow to elaborate

[Kenny Lau]

@[class, priority 100]
inductive linear_nonneg_ring : Type u_1 → Type u_1
constructors:
linear_nonneg_ring.mk : Π {α : Type u_1} [_to_ring : ring α] [_to_no_zero_divisors : no_zero_divisors α] [_to_nonzero : nonzero α]
(add : α → α → α) (add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)) (zero : α)
(zero_add : ∀ (a : α), 0 + a = a) (add_zero : ∀ (a : α), a + 0 = a) (neg : α → α)
(add_left_neg : ∀ (a : α), -a + a = 0) (add_comm : ∀ (a b : α), a + b = b + a) (nonneg pos : α → Prop)
(pos_iff :
  auto_param (∀ (a : α), pos a ↔ nonneg a ∧ ¬nonneg (-a)) (name.mk_string "order_laws_tac" name.anonymous))
(zero_nonneg : nonneg 0) (add_nonneg : ∀ {a b : α}, nonneg a → nonneg b → nonneg (a + b))
(nonneg_antisymm : ∀ {a : α}, nonneg a → nonneg (-a) → a = 0),
  (∀ {a b : α}, nonneg a → nonneg b → nonneg (a * b)) →
  (∀ (a : α), nonneg a ∨ nonneg (-a)) → linear_nonneg_ring α

[Mario Carneiro]

aha

[Kenny Lau]

wait where's my nonneg_total

[Mario Carneiro]

#print linear_nonneg_ring

@[class]
structure linear_nonneg_ring : Type u_1 → Type u_1
fields:
linear_nonneg_ring.add : Π {α : Type u_1} [c : linear_nonneg_ring α], α → α → α
linear_nonneg_ring.add_assoc : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
linear_nonneg_ring.zero : Π {α : Type u_1} [c : linear_nonneg_ring α], α
linear_nonneg_ring.zero_add : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a : α), 0 + a = a
linear_nonneg_ring.add_zero : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a : α), a + 0 = a
linear_nonneg_ring.neg : Π {α : Type u_1} [c : linear_nonneg_ring α], α → α
linear_nonneg_ring.add_left_neg : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a : α), -a + a = 0
linear_nonneg_ring.add_comm : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a b : α), a + b = b + a
linear_nonneg_ring.mul : Π {α : Type u_1} [c : linear_nonneg_ring α], α → α → α
linear_nonneg_ring.mul_assoc : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
linear_nonneg_ring.one : Π {α : Type u_1} [c : linear_nonneg_ring α], α
linear_nonneg_ring.one_mul : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a : α), 1 * a = a
linear_nonneg_ring.mul_one : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a : α), a * 1 = a
linear_nonneg_ring.left_distrib : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
linear_nonneg_ring.right_distrib : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
linear_nonneg_ring.eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a b : α), a * b = 0 → a = 0 ∨ b = 0
linear_nonneg_ring.zero_ne_one : ∀ {α : Type u_1} [c : linear_nonneg_ring α], 0 ≠ 1
linear_nonneg_ring.nonneg : Π {α : Type u_1} [c : linear_nonneg_ring α], α → Prop
linear_nonneg_ring.pos : Π {α : Type u_1} [c : linear_nonneg_ring α], α → Prop
linear_nonneg_ring.pos_iff : ∀ {α : Type u_1} [c : linear_nonneg_ring α],
  auto_param
    (∀ (a : α), linear_nonneg_ring.pos a ↔ linear_nonneg_ring.nonneg a ∧ ¬linear_nonneg_ring.nonneg (-a))
    (name.mk_string "order_laws_tac" name.anonymous)
linear_nonneg_ring.zero_nonneg : ∀ {α : Type u_1} [c : linear_nonneg_ring α], linear_nonneg_ring.nonneg 0
linear_nonneg_ring.add_nonneg : ∀ {α : Type u_1} [c : linear_nonneg_ring α] {a b : α},
  linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg b → linear_nonneg_ring.nonneg (a + b)
linear_nonneg_ring.nonneg_antisymm : ∀ {α : Type u_1} [c : linear_nonneg_ring α] {a : α},
  linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg (-a) → a = 0
linear_nonneg_ring.mul_nonneg : ∀ {α : Type u_1} [c : linear_nonneg_ring α] {a b : α},
  linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg b → linear_nonneg_ring.nonneg (a * b)
linear_nonneg_ring.nonneg_total : ∀ {α : Type u_1} [c : linear_nonneg_ring α] (a : α), linear_nonneg_ring.nonneg a ∨ linear_nonneg_ring.nonneg (-a)

[Mario Carneiro]

you got an inductive, not a structure

[Kenny Lau]

why?

[Kenny Lau]

I didn't touch old_strcture_command

[Kenny Lau]

this is very strange

[Mario Carneiro]

I wasn't even aware this was a fallback

[Mario Carneiro]

maybe the latest version broke something

[Kenny Lau]

what's even stranger is the thing above it works

[Kenny Lau]

ordered_ring.lean:826:0: information print result
@[class, priority 100]
structure nonneg_ring : Type u_1 → Type u_1
fields:
nonneg_ring.add : Π {α : Type u_1} [c : nonneg_ring α], α → α → α
nonneg_ring.add_assoc : ∀ {α : Type u_1} [c : nonneg_ring α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
nonneg_ring.zero : Π {α : Type u_1} [c : nonneg_ring α], α
nonneg_ring.zero_add : ∀ {α : Type u_1} [c : nonneg_ring α] (a : α), 0 + a = a
nonneg_ring.add_zero : ∀ {α : Type u_1} [c : nonneg_ring α] (a : α), a + 0 = a
nonneg_ring.neg : Π {α : Type u_1} [c : nonneg_ring α], α → α
nonneg_ring.add_left_neg : ∀ {α : Type u_1} [c : nonneg_ring α] (a : α), -a + a = 0
nonneg_ring.add_comm : ∀ {α : Type u_1} [c : nonneg_ring α] (a b : α), a + b = b + a
nonneg_ring.mul : Π {α : Type u_1} [c : nonneg_ring α], α → α → α
nonneg_ring.mul_assoc : ∀ {α : Type u_1} [c : nonneg_ring α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
nonneg_ring.one : Π {α : Type u_1} [c : nonneg_ring α], α
nonneg_ring.one_mul : ∀ {α : Type u_1} [c : nonneg_ring α] (a : α), 1 * a = a
nonneg_ring.mul_one : ∀ {α : Type u_1} [c : nonneg_ring α] (a : α), a * 1 = a
nonneg_ring.left_distrib : ∀ {α : Type u_1} [c : nonneg_ring α] (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
nonneg_ring.right_distrib : ∀ {α : Type u_1} [c : nonneg_ring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
nonneg_ring.nonneg : Π {α : Type u_1} [c : nonneg_ring α], α → Prop
nonneg_ring.pos : Π {α : Type u_1} [c : nonneg_ring α], α → Prop
nonneg_ring.pos_iff : ∀ {α : Type u_1} [c : nonneg_ring α],
  auto_param (∀ (a : α), nonneg_ring.pos a ↔ nonneg_ring.nonneg a ∧ ¬nonneg_ring.nonneg (-a))
    (name.mk_string "order_laws_tac" name.anonymous)
nonneg_ring.zero_nonneg : ∀ {α : Type u_1} [c : nonneg_ring α], nonneg_ring.nonneg 0
nonneg_ring.add_nonneg : ∀ {α : Type u_1} [c : nonneg_ring α] {a b : α},
  nonneg_ring.nonneg a → nonneg_ring.nonneg b → nonneg_ring.nonneg (a + b)
nonneg_ring.nonneg_antisymm : ∀ {α : Type u_1} [c : nonneg_ring α] {a : α}, nonneg_ring.nonneg a → nonneg_ring.nonneg (-a) → a = 0
nonneg_ring.mul_nonneg : ∀ {α : Type u_1} [c : nonneg_ring α] {a b : α},
  nonneg_ring.nonneg a → nonneg_ring.nonneg b → nonneg_ring.nonneg (a * b)
nonneg_ring.mul_pos : ∀ {α : Type u_1} [c : nonneg_ring α] {a b : α}, nonneg_ring.pos a → nonneg_ring.pos b → nonneg_ring.pos (a * b)
nonneg_ring.zero_ne_one : ∀ {α : Type u_1} [c : nonneg_ring α], 0 ≠ 1

[Kenny Lau]

what's the difference

[Kenny Lau]

aha!

[Kenny Lau]

I used "false" to define domain

[Kenny Lau]

set_option old_structure_cmd false

/-- A domain is a ring with no zero divisors, i.e. satisfying
  the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. Alternatively, a domain
  is an integral domain without assuming commutativity of multiplication. -/
class domain (α : Type u) extends ring α, no_zero_divisors α, nonzero α

[Kenny Lau]

oh no

[Mario Carneiro]

no that means unit

[Mario Carneiro]

oh you mean old_structure_cmd false

[Kenny Lau]

looks like I cannot use any "false" ever

[Kenny Lau]

but otherwise I get this error:

type mismatch at application
  @ring.to_semiring α right_distrib
term
  right_distrib
has type
  ∀ (a b c : α), (a + b) * c = a * c + b * c
but is expected to have type
  ring α

[Mario Carneiro]

what's an mwe of creating a class that is registered as an inductive?

[Kenny Lau]

so my workaround is to declare the Props as parameters

[Kenny Lau]

boom

[Kenny Lau]

universe u

set_option old_structure_cmd true

class A (α : Type u) extends has_zero α.
class B (α : Type u) [has_zero α] : Prop.

set_option old_structure_cmd false

class C (α : Type u) extends A α, B α.

set_option old_structure_cmd true

class D (α : Type u) extends C α.

#print D

[Kenny Lau]

@[class]
inductive D : Type u → Type u
constructors:
D.mk : Π {α : Type u} [_to_A : A α] [_to_B : B α], D α

[Mario Carneiro]

hm, I get that too

[Kenny Lau]

class A (α : Type).
#print A

[Kenny Lau]

@[class]
inductive A : Type → Type
constructors:
A.mk : Π {α : Type}, A α

[Kenny Lau]

boom, guaranteed MWE

[Kenny Lau]

class A : Type.
#print A

[Kenny Lau]

@[class]
inductive A : Type
constructors:
A.mk : A

[Kenny Lau]

this is more minimal

[Mario Carneiro]

that's nuts

[Mario Carneiro]

one would think this is in the test suite

[Kenny Lau]

but:

class A : Type.
class C extends A.
#print C

[Kenny Lau]

@[class]
structure C : Type
fields:
C.to_A : Π [c : C], A

[Mario Carneiro]

maybe it's just the 0-arity?

[Mario Carneiro]

If you give the class a field it probably works too

[Kenny Lau]

class A : Type :=
(B : true)

class C extends A :=
(D : true)

set_option old_structure_cmd true
class E extends C :=
(F : true)

#print E

[Kenny Lau]

@[class]
inductive E : Type
constructors:
E.mk : Π [_to_A : A], true → true → E

[Kenny Lau]

this is minimal

[Kenny Lau]

modulo each class having a parameter

[Kenny Lau]

@Mario Carneiro

[Kenny Lau]

and finally, the glorious error:

class A : Type :=
(B : true)

class C extends A :=
(D : true)

set_option old_structure_cmd true
class E extends C :=
(F : true)

def G : E :=
{ B := trivial,
  D := trivial,
  F := trivial }

[Kenny Lau]

invalid structure value {...}, expected type is known, but it is not a structure
  E

[Kenny Lau]

so A and C are both structures

[Kenny Lau]

but E is inductive

[Kenny Lau]

lean#285

[Gabriel Ebner]

I don't think it was ever supported to extend new-style structures using old-style structures. Is it possible to just not do it here?

[Kenny Lau]

@Gabriel Ebner it would be, if not for this bug:

set_option old_structure_cmd true
class A (α : Type).
class B (α : Type) extends A α :=
(BB : ℕ)
class C (α : Type) [A α].
class D (α : Type) extends B α, C α.

[Kenny Lau]

failed to add declaration to environment, it contains local constants

[Kenny Lau]

which can be fixed by using old_structure_cmd false