pp hack for `#eval` on Props

Stream: general

[Eric Rodriguez]

I understand that Prop can't have is_repr, because it's a Type typeclass. However, it's slowly getting frustrating to have to write #eval if (prop) then 123 else 0; is there some chance that there could be a hack built-into the pretty-printer itself? or is it a lot of work?

[Anne Baanen]

Is there a reason that docs#has_repr (EDIT: that's the correct name, right?) can't be generalized to Sort?

[Eric Rodriguez]

(yep, oopsie!)

[Eric Rodriguez]

I assume there's a good reason, because there seems to always be a good reason to avoid Sort...

[Eric Rodriguez]

oh although reading more, it seems to be docs#has_to_string instead of docs#has_repr, but that's still Type-only

[Anne Baanen]

I'm not sure I understand: do you want an instance along the lines of:

instance : has_to_string Prop := ⟨λ p, if p then "true" else "false"⟩

[Eric Rodriguez]

yeah essentially

[Anne Baanen]

Because this typechecks, apart from the issue that p does not have [decidable p]

[Anne Baanen]

Prop : Type after all

[Eric Rodriguez]

hmph yes; essentially my issue is that when I do something like #eval 23121 \| 2342345235, the output is #0 (and a warning)

[Eric Rodriguez]

Now that you say this though, I'm not sure how to fix that though

[Anne Baanen]

Well, the real issue here is that there is no definable map f : Prop → string that is not constant! Let's say WLOG that f true = "true" and f false = "false", then propext implies that f p = "true" iff p is true and f p = "false" otherwise. So f decides propositions correctly.

[Anne Baanen]

So the only way you can define a has_repr instance like you want is using partial maps, i.e.

meta instance : has_repr Prop := ⟨λ p, _⟩

[Gabriel Ebner]

You realize that every proposition is represented as 0 in the VM, no matter whether it is true or false? meta doesn't let you get around that.

[Eric Rodriguez]

I understand why it outputs what it does, but if there's some non-classical decidable instance it could be a lot more helpful to just use that implicitly, is my point. But it seems a lot harder than I envisioned it when I first posted this, with what you guys are saying

[Anne Baanen]

Gabriel Ebner said:

You realize that every proposition is represented as 0 in the VM, no matter whether it is true or false? meta doesn't let you get around that.

I was just about to argue that Lean should not allow you to pattern-match on Props, so I am not surprised that all Props have the same representation :)

[Gabriel Ebner]

Eric Rodriguez said:

I understand why it outputs what it does, but if there's some non-classical decidable instance it could be a lot more helpful to just use that implicitly, is my point. But it seems a lot harder than I envisioned it when I first posted this, with what you guys are saying

The proper hack is to check whether the term is a Prop in eval_cmd, and then add to_bool in that case.

[Anne Baanen]

(If I understand the source correctly, all Sorts have the same representation in the VM, right? Which makes sense for the same reason that all Props are the same.)

[Yakov Pechersky]

Eric, what would you want #eval to show?

[Eric Rodriguez]

some form of true/false, I'm currently trying to learn some meta-code so I can code up the fix that Gabriel suggestsed

[Yakov Pechersky]

Then I would do example : 5 \mid 25 := dec_trivial, and check if it compiles

[Yakov Pechersky]

Or, for some other Props, by slim_check

[Eric Rodriguez]

kernel computation is way slower though

[Yakov Pechersky]

The first would use the decidable instance available, or if it can't, one can write a norm_num plugin to do so

[Yakov Pechersky]

You can take a look at Mario's recent gcd, lcm, and coprime norm_num plugin PR, to see how to use VM computation to speed up proof construction