Object not being a structure

Stream: lean4

[Gareth Ma]

Hi, how do I express (and prove) that an object is not a particular structure via a counterexample?
For example,

import Mathlib.Tactic

open Nat

structure Idempotent (α : Type*) [AddGroup α] where
  f : ∀ a : α, a = a + a

theorem NotIdempotent : ¬(∀ a : ℤ, a = a + a) := by
  push_neg
  use 1
  linarith

/- If ℤ is Idempotent, then it has a .f field, contradicting NotIdempotent -/
example : ¬(Idempotent ℤ) := by sorry

[Kevin Buzzard]

import Mathlib.Tactic

open Nat

structure Idempotent (α : Type*) [AddGroup α] : Prop where -- working around Lean 4 bug
  f : ∀ a : α, a = a + a

theorem NotIdempotent : ¬(∀ a : ℤ, a = a + a) := by
  push_neg
  use 1
  linarith

/- If ℤ is Idempotent, then it has a .f field, contradicting NotIdempotent -/
example : ¬(Idempotent ℤ) := by
  rintro ⟨f⟩
  exact NotIdempotent f

[Kevin Buzzard]

Is there an open Lean 4 issue for the "structure will sometimes be a Type when it should be a Prop" bug?

[Gareth Ma]

Ah, I didn't know it's supposed to be a Prop, thanks.

[Gareth Ma]

Kevin Buzzard said:

Is there an open Lean 4 issue for the "structure will sometimes be a Type when it should be a Prop" bug?

I can't find any. Also, this bug has been there since version Lean (version 4.0.0, commit ec941735c80d, Release)

[Yaël Dillies]

It was also there in Lean 3. It never worked, really. Maybe that's a performance concern? as in checking whether something can live in Prop could be expensive? or maybe it would unexpectedly unify universe metavariables?

[Mario Carneiro]

no, I think it's just not a feature that has been suggested

[Mario Carneiro]

I think we got as far as writing a linter for it though

[Kevin Buzzard]

lean4#2690

[Kevin Buzzard]

(let me know if you'd rather this were closed for some reason)