A port of SSR to lean...

https://arxiv.org/pdf/2403.12733.pdf

somewhat strange to me: no mention of canonical structures, although I believe they are available. Or maybe it's because switching between `Prop`

and `bool`

is not necessary (so no benefits without a bunch of library development)?

I do believe canonical structures are orthogonal to ssreflect

in principle, sure. But if your system conflates `Prop`

/`bool`

, it's not even obvious why the "reflect" part matters. On the other hand, having similar proof language syntax and packed classes would allow replicating MathComp stuff in Lean directly.

I guess it would be like all those HOL-Light-to-other-HOL exercises people do

- I guess this discussion thread on the lean zulip provides more context: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Small.20Scale.20Reflection.20for.20the.20Working.20Lean.20user/near/429056031
- I don't understand the part where lean conflates Bool with Prop. I only occasionally use coq, so I would like to ask where the difference lies

in any system which uses classical logic, using or calling something a proposition or boolean is a stylistic choice, since you can convert between them at any time in both directions. For example, in HOL, propositions *are* the type `bool`

. In Coq without axioms, `bool`

signifies something computable/decidable, while `Prop`

does not, and the distinction is fundamental.

In Coq, SSReflect can be viewed as rehabilitating `bool`

s as a tool for performing proof, where previously you "only" had `Prop`

s and ad-hoc lemmas connecting them to `bool`

s in special cases. But in Lean, `bool`

could/can already be used in proofs anywhere and anyhow (in principle).

In lean, we tend to use Prop with a `Decidable`

instance instead of bool (the use of bool is brushed under the carpet of the `Decidable`

typeclass). The authors suggest that reflection in this context simplifies linking a functional spec of a Prop (which needs to be computable) to an equivalent inductive spec. It generates the relevant typeclass instances as well as API lemmas from an instance of their `Reflex`

typeclass provided by the user.

but there is no guarantee that a `Decidable`

instance in Lean is actually decidable, right? And if `bool`

is seldom used in Lean, then the benefits of the reflection part of LeanSSR (distinct from the nice succinct proof syntax) are even harder to assess. With that said, if I were to write Lean proofs, I would probably use LeanSSR just to get something familiar.

The Decidable class instance has a function `decide`

defined on it that turns the Prop into bool :https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Decidable.decide

Basically the typeclass takes a proof of the proposition and converts it to bool. I am guessing this isn't computational.

Anyway, I guess this question is best posed to the authors. One of their original motivation appears to have been to get the ssreflect experience in lean. And they say they ended up getting something better UX wise.

Last updated: Jul 23 2024 at 19:02 UTC