## Stream: math-comp users

### Topic: LeanSSR

#### Bas Spitters (Mar 22 2024 at 17:36):

A port of SSR to lean...
https://arxiv.org/pdf/2403.12733.pdf

#### Karl Palmskog (Mar 22 2024 at 18:42):

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)?

#### Cyril Cohen (Mar 22 2024 at 19:51):

I do believe canonical structures are orthogonal to ssreflect

#### Karl Palmskog (Mar 22 2024 at 20:08):

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.

#### Karl Palmskog (Mar 22 2024 at 20:09):

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

#### Shreyas Srinivas (Mar 23 2024 at 07:04):

1. 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
2. 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

#### Karl Palmskog (Mar 23 2024 at 08:35):

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).

#### Shreyas Srinivas (Mar 23 2024 at 09:09):

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.

#### Karl Palmskog (Mar 23 2024 at 09:14):

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.

#### Shreyas Srinivas (Mar 23 2024 at 09:20):

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.

#### Shreyas Srinivas (Mar 23 2024 at 09:22):

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