Prop-typed defs?

Stream: mathlib4

[Thomas Murrills]

Should there ever be Prop-valued EDIT: Prop-typed defs?

I can imagine "sometimes Prop" defs (i.e. whose type is a Sort u), but I'm not sure why we would ever want to avoid (or be unable to use) theorem if the type of the decl was a Prop.

I'm asking to see if (1) I ought to consider this edge case in a particular setting (2) to see if we ought to lint against Prop-typed defs. :)

[Bhavik Mehta]

Just to be clear, you mean defs whose type is itself a Prop, rather than a def whose type is Prop, right?

[Kevin Buzzard]

like docs#RiemannHypothesis ? (edit: apparently not!)

[Aaron Liu]

you means defs whose value is a proof?

[Thomas Murrills]

Bhavik Mehta said:

Just to be clear, you mean defs whose type is itself a Prop, rather than a def whose type is Prop, right?

Correct! :grinning_face_with_smiling_eyes: defs which you could, presumably, replace with theorem.

[Thomas Murrills]

(I should, in fact, not have said "Prop-valued"; I think all readings of that are not what I wanted to mean. :sweat_smile:)

[Yury G. Kudryashov]

Currently, instances are defs even if they can be theorems.

[Thomas Murrills]

I don't believe that's true (anymore?): :)

import Lean.Environment
import Lean.Elab.Command

instance foo {α} : Nonempty α := sorry
def bar {α} : Nonempty α := sorry

open Lean

run_cmd do
  let some foo := (← getEnv).findAsync? ``foo | throwError "no foo"
  let some bar := (← getEnv).findAsync? ``bar | throwError "no bar"
  logInfo m!"foo kind: {repr foo.kind}\nbar kind: {repr bar.kind}"
  /-
  foo kind: Lean.ConstantKind.thm
  bar kind: Lean.ConstantKind.defn
  -/

[Robin Arnez]

theorems can't be match patterns, so you get things like def rfl (docs#rfl) and def HEq.rfl (docs#HEq.rfl). Actually, I don't think there's a single other declaration where there's a reason for it being a def and not a theorem, although there are still some others, e.g. from aliases using abbrevs in core (since core doesn't have the alias command), or from instances using delta deriving. In total there are actually 256 such defs that could be theorems:

import Mathlib

open Lean
run_meta
  let mut reports := #[]
  for (n, c) in (← getEnv).constants do
    if ← n.isBlackListed then
      continue
    let .defnInfo _ := c | continue
    let ty := c.type
    if ← Meta.isProp ty then
      reports := reports.push n
  reports := reports.qsort (fun a b => a.toString < b.toString)
  logInfo m!"{.joinSep (reports.map MessageData.ofConstName).toList (.ofFormat .line)}"
  logInfo m!"{reports.size} reports"

[Thomas Murrills]

Ah, okay! So some instances are indeed defs when they could be theorems. :)

I suppose it might be reasonable to exclude declarations marked with match_pattern on principle, even if it's basically just the two; out of curiosity, filtering by declarations marked @[match_pattern] reveals this other family of match_pattern proofs:

Hindman.FP.cons
Hindman.FP.head
Hindman.FP.tail
Hindman.FS.cons
Hindman.FS.head
Hindman.FS.tail

[Thomas Murrills]

About those instances: "should" they be theorems, or is there a reason why delta-deriving somehow means that making them defs is the right choice...? (I can't think of anything, but just in case...)

[Chris Henson]

I may be missing a subtlety of what you want to lint against, is this different from the docs#Batteries.Tactic.Lint.defLemma environment linter?

[Thomas Murrills]

Nope, that's what I was looking for, great (at least by semantics)! :)

But, do we run it in CI? Seems as though we don't if there are all these exceptions, right? It seems like it was last touched a couple of years ago, when some things were different (e.g. lean4#2575 is fixed now, and instances are (sometimes) handled differently.)