percent type

Stream: Is there code for X?

[Roman]

Hi, I was wondering what would be the best way to define a percent, I'm a beginner and wondering if there is a better way of the usual private constructor and default constructors/parser that should respect that a percent is between 0 and 100. Could I embed that rule in the definition of a percent directly instead of having a comment (using subtypes ?)
I haven't touched proof yet but I hope I can start soon

[Kenny Lau]

@Roman what are you using it for?

[Kenny Lau]

in some applications i have in mind, the best way would be to write some meta code so that $n:num % elaborates to a term in a char-zero field (default Rat)

[Kenny Lau]

note how e.g. you can already type:

#check (3.24 : Rat)

[Kenny Lau]

which is secretly calling Rat.ofScientific

[Martin Dvořák]

Do you really want a type? I would rather have it as a notation.

[Martin Dvořák]

If you just want numbers between 0 and 100, you can do it easily with a subtype. Do you want them to be integers?

[Kenny Lau]

import Mathlib

notation n "%" => n / 100

#check (30.2% : ℝ)

Actually my idea is easier to implement than I thought

[Kevin Buzzard]

I can have a 300% increase in productivity -- who says percentages are between 0 and 100?

[Kenny Lau]

and 100% is actually 0 in Z/2Z!

[Kenny Lau]

import Mathlib

notation n "%" => n / 100

example : (100% : ZMod 2) = 0 := by
  norm_num; rfl

[Kenny Lau]

(why do i need two tactics?)

[Kenny Lau]

(grind works by itself, also i should probably stay on topic)

[Roman]

Hello, thank you everyone for your input, it is quite interesting to see all the different view point, I do indeed thought a percent was limited to 100 but saying 300% is obviously valid ! I do not know the recommend approach to my use-case then as I have to take a percentage of an open/close position of a motor to drive it to that position, and ideally the percentage value that it take should reflect that it can't overrun it's max course in it's API if possible so that other moving/filling/measuring systems could use the same standard in my application.
I haven't been able to use subtypes properly, from my understanding it require the user of the api to provide a proof that the number given is between 0 and 100 but it induce a lot of boilerplate from what I've been able to do?

[Kenny Lau]

import Mathlib

notation n"%" => (n : Fin 101)

-- this is magic, ignore it
open Qq Lean PrettyPrinter Delaborator in
@[app_delab OfNat.ofNat]
def delabPercent : Delab := whenPPOption Lean.getPPNotation do
  let #[α, n, _] := (← SubExpr.getExpr).getAppArgs | failure
  let .true ← Meta.isDefEq α q(Fin 101) | failure
  let some n := n.rawNatLit? | failure
  `($(quote n)%)

example : 36% < 37% := by decide

example : ∀ x, 0% ≤ x ∧ x ≤ 100% := by decide

[Eric Wieser]

I have to take a percentage of an open/close position of a motor to drive it to that position

Does it take integer positions? Decimal positions with fixed precision? Does your model of it let you set it to an position of precisely $\pi^{-1}$?

[Roman]

Using Fin is tempting and I could get away with it honestly but ideally it should take a Decimal position

[Kenny Lau]

can you give us a full specification of what the "percent type" should contain?

[Roman]

Kenny Lau said:

can you give us a full specification of what the "percent type" should contain?

Well I'm interested in having the "most truthful" models in my application, having things defined after well accepted standards, conventions etc. The solution would just boil down to subtypes, having a constructor returning an Option (subtype percent), and passing that percent along with the proof (which serve as a token of validity in that case if I understand correctly) to any function requiring a subtype.
It was just that I did not want a private constructor holding the strings in making a valid, in range percent type, subtypes can be constructed by different means and each must abide by validating one proposition, the boilerplate can be hidden behind constructors and not touched by the developer when interacting with it so it's all good, I just need to spend more time on the language. Thank you for taking the time for me by the way !

[Kenny Lau]

@Roman you have not answered my question at all. what we were trying to ask you, with those "ridiculous questions" (such as pi^-1), is what type of values are allowed in your percent type, whether it's any rational number, or any real number, or something in between

[Kenny Lau]

"subtype" doesn't answer the question because the follow-up question is, subtype of what?

[Roman]

Well I'm not well versed in math so I can't give the answer you probably expect but I believe it should be any Real number ?

[Roman]

I mean I could go with integer for my use but for a real definition of "a percent" you guys would probably be more up to the task than me haha

[Kevin Buzzard]

Lean's philosophy is not to put guardrails in the definitions or notations, but in the theorems about them. Did you know that $1/0=0$ in Lean, for example? I attempt to explain why here. There are no guardrails about using the division symbol, and so an idiomatic percentage formalization in Lean should probably have no guardrails for the same reasons as explained in the blog post.