Stream: math-comp users

Topic: LeanSSR


view this post on Zulip Bas Spitters (Mar 22 2024 at 17:36):

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

view this post on Zulip 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)?

view this post on Zulip Cyril Cohen (Mar 22 2024 at 19:51):

I do believe canonical structures are orthogonal to ssreflect

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 22 2024 at 20:09):

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

view this post on Zulip 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

view this post on Zulip 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 bools as a tool for performing proof, where previously you "only" had Props and ad-hoc lemmas connecting them to bools in special cases. But in Lean, bool could/can already be used in proofs anywhere and anyhow (in principle).

view this post on Zulip 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 Reflextypeclass provided by the user.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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