Introduction: Rado Kirov

Stream: new members

[Rado Kirov]

In leau of introduction, I wrote up a quick blog post about my experience finishing Theorem Proving in Lean4 - https://rkirov.github.io/posts/lean1 and has more info about my background.

[Kyle Miller]

Re Decidable, here's another way the class could have been written:

class Decidable' (p : Prop) where
  eval : Bool
  eval_eq_true_iff : (eval = true) ↔ p

It's a structure that records whether or not the given proposition is true. This lets you lift a given proposition to a boolean value that you can compute with. Propositions themselves do not have any computational content on their own (that's to say, there's no algorithm that can automatically prove that p is True or False), so this is a way to "reflect" logical propositions into a computable form.

The actual docs#Decidable is an inductive type with two constructors; I think of as being a "heavy Bool" that also records what is true or false and why.

(I'm hoping in the future Lean will switch to a variant of Decidable'. It will help with some definitional equality issues we run into with BEq.)

[Kyle Miller]

Re #eval vs #reduce, the first takes the expression, compiles it, and evaluates the compiled code (it doesn't build a binary, but it at least runs the IR (intermediate representation) in a VM). If you #eval a proposition, it will try to find a Decidable instance and evaluate the proposition as a Bool (hence why you see true and false rather than True and False as the result!).

The second, #reduce, instead uses the reduction rules of lambda calculus, and symbolically tries to evaluate the expression to normal form. Sometimes #reduce gets stuck on computations that #eval doesn't get stuck on. The main difference is that #eval erases all types and proofs during compilation, essentially simplifying the expression first into an untyped lambda calculus, which is more flexible for computation.

[Kyle Miller]

Re simp: don't confuse it for Simplify[...]. It tends to simplify, but it's not a simplifier per se. It's a rewrite rule engine, with features that handle applying rewrites deep within expressions automatically (while generating proofs of course!) using so-called congruence lemmas.

The Simplify[...] function in Mathematica also is a rewrite rule system, but it is actually trying to simplify the expression, and in contrast to simp it applies its rules nondeterministically (i.e., it explores rewrites along a graph of possibilities). It tries applying a good number of rewrites and then returns the expression it finds that minimizes some complexity measure.

In principle we could (and probably should!) have a Simplify[...] in Lean, especially with some of the congruence closure modules in the cc and/or grind tactics.

[Kyle Miller]

Re rfl and defeq: it's best to use rfl only if you know the definitions, and you know the definitions are supposed to be unfolded. Breaking through the abstraction barriers with rfl and forcing a computation (in the #reduce sense) is sometimes known as a "heavy rfl".

In large library design, we tend to prefer using rewrite lemmas.

[Rado Kirov]

Thanks for all the answers again, it will take me a bit of time to absorb :)

[Rado Kirov]

What’s the simplest non decidable prop with Nats? Since decidable is a class, can it be make decidable with an extra instance ?

[Damiano Testa]

I do not know if the example below is undecidable in the technical sense (and probably it isn't), but the statement "there are odd perfect numbers" is something for which it would be interesting to have a Decidable instance!

[Damiano Testa]

For an actually undecidable statement, you can look at Hilbert's Tenth Problem.

[Rado Kirov]

Yeah that’s what I am struggling with - separating proven to be non decidable in all systems and practically non-decidable because something is missing an type class instance

[Kyle Miller]

Along those lines, given an arbitrary function f : Nat -> Nat, you can't generally decide forall n, f n = 0. Hilbert's 10th problem is a special case of this, where we restrict the possibilities of f to be multivariable polynomials (one can encode multivariables polynomials as such an f).

[Kyle Miller]

What would the algorithm be? We could semidecide it by evaluating f at successive integers, returning false as soon as we find an n where f n != 0. But we can't know for sure that f is always zero.

[Kyle Miller]

For specific examples of f, of course one can decide whether it's true without needing to fall back on evaluating it over its whole domain. Here's one:

instance : Decidable (∀ n, n * (n - 1) * (n - 2) = 0) :=
  isFalse <| by
    push_neg
    use 3
    norm_num

[Kyle Miller]

That one would have been semidecided, so here another

instance : Decidable (∀ n, 0 * n = 0) :=
  isTrue <| by simp

[Rado Kirov]

Perfect that’s helpful, now I wonder for which of the proved props one has to write that instance vs it gets automatically generated because of some type class magic ?

[Kyle Miller]

(Complicating things, in Lean every proposition is technically decidable via docs#Classical.propDecidable, but that is noncomputable and can't be used with #eval. It uses the docs#Classical.choice to "construct" a decision. There's no code backing that up however, hence the need for the noncomputable modifier to tell Lean to not try to compile it.)

[Kyle Miller]

The typeclass magic consists of a whole library of instances like docs#instDecidableAnd, which can decide p ∧ q by deciding p and q.

[Kyle Miller]

The instances syntactically match on the proposition, which is how it can be broken apart and "compiled" into a decision procedure for it.

[Rado Kirov]

So if I start building more complicated props when do they stop being decidable - x=y is decidable, adding propositional logic basic ops is too, but is it at first order - existential and universal quantifiers when props stop being decidable or when one uses LEM?

[Kyle Miller]

x = y isn't actually decidable by default -- there's the abbreviation docs#DecidableEq to bring in forall (x y : T), Decidable (x = y)

[Aaron Liu]

Actually, x = y is not always decidable, even for fairly simple constructs. In contrast, every formula in a decidable theory is decidable.

Once you start being able to encode turing machines in your propositions, is when it stops being decidable

[suhr]

My main critique is that sometimes it starts using concepts or syntax that was not introduced earlier (the curse of knowledge for the authors).

I would argue this is not because of the curse of knowledge but because authors wanted relatively short and "practical" tutorial. So a lot of essential background is missing.

[Kyle Miller]

Rado Kirov said:

existential and universal quantifiers

Yeah, this is a way nondecidability creeps in. Also inductively defined Props in general (Eq is such an example).

For what it's worth, there are Decidable instances for quantifiers when the domain is finite (via docs#Fintype).

[Rado Kirov]

Ok that is starting to make sense on decidability and gives me enough pointers to look more into it. I see newcomers get tripped on prop vs bool. Funny enough coming from typescript I am very comfortable with that - types are checked and erased, there is no reification at runtime, the whole type language is separately evolved and bolted on a Js runtime. But decidable makes lean not only have that separation but also allow one to bridge it when needed, which is wild :)

[Rado Kirov]

suhr said:

My main critique is that sometimes it starts using concepts or syntax that was not introduced earlier (the curse of knowledge for the authors).

I would argue this is not because of the curse of knowledge but because authors wanted relatively short and "practical" tutorial. So a lot of essential background is missing.

I have some concrete example where for example “class … extend …” was used for the first time in a section for another concept and had me “ah type classes can extend like structures” but that wasn’t said directly just used in a fancier example. So not really background. Anyways I will file GitHub issues for those and can discuss them there.

[Rado Kirov]

It’s hard to capture how “alien tech” lean feels even for someone that has done programming and math for awhile

[suhr]

Yeah, constructive logic turned into a programming language with some extras (like type classes) borrowed from other functional programming languages is not that a classical mathematician or an ordinary programmer is used to see. Though, programmers sometimes play with a lot of weird stuff.

[Chris Wong]

Aaron Liu said:

Actually, x = y is not always decidable, even for fairly simple constructs. In contrast, every formula in a decidable theory is decidable.

Once you start being able to encode turing machines in your propositions, is when it stops being decidable

To give a concrete example:

Equality on real numbers is undecidable. You could have 0.000..., and without inspecting infinitely many digits, you wouldn't know if it's all zeros (hence equal to 0), or it actually ends in ...0001.

[Rado Kirov]

Wrote up some more random notes on Lean as I finished first half of MIL - https://rkirov.github.io/posts/lean2/ . It's been lots of fun so far and I have learned a lot from all the conversations happening on here.

[Kevin Buzzard]

The links to the puzzle games didn't work for me

[Aaron Liu]

It's https://rkirov.github.io/posts/puzzles2024/

[Rado Kirov]

ops, fixed the links, thanks for catching that. Speaking of puzzles, I have been wondering how would an even more gamified version of the number game look like - like visually represent inductive types and their reductions though something like moving boxes, etc. Patrick's Parabox is an example of a puzzle game that has non-trivial math content (though not matching any real math theory) as it reifies infinity paradoxes.

[suhr]

Theorem proving always reminds me of Baba Is You.