Zulip Chat Archive

Stream: general

Topic: computation vs proving


view this post on Zulip Johan Commelin (Jul 20 2020 at 18:24):

In order to avoid continued hijacking https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.233403 (sorry @Yakov Pechersky), I'm starting this thread.

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:25):

Probably lots of people have thought about this before.

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:25):

How hard would it be to have a more formal approach to "specification" and "implementation"?

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:27):

If I could write:

specification natural_number_object := initial semiring blabla

-- and then

implementation natural_number_object nat := some proof

implementation natural_number_object num := some proof

would that help?

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:27):

Of course we can do that with typeclasses.

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:27):

But maybe that abusing a system for something it isn't really designed for/ meant to be used for.

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:28):

I'm not sure if we want to prove lemmas about polynomials by starting

variables (R RX : Type*) [semiring R] [semiring RX] [polynomial_like_type R RX]

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:31):

In particular, what typeclasses currently don't allow, but what I would want to have from this "spec/impl" business, is that if I need to prove that some polynomial of degree 3 is irreducible over zmod 5, then I can just say exact dec_trivial and Lean should automatically figure out that it can translate the question to one of the computational implementations, and run the computation itself.

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:32):

But then, nevertheless, the theorem should be a theorem about all implementations, in other words a theorem that follows from the "spec".

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:32):

Does that even make sense?

view this post on Zulip Jalex Stark (Jul 20 2020 at 18:33):

this is the equiv_rw problem, right?

view this post on Zulip Jalex Stark (Jul 20 2020 at 18:33):

you have two types and you know they satisfy the same sentences in the theory of rings

view this post on Zulip Jalex Stark (Jul 20 2020 at 18:34):

in order to prove some particular thing about theorem-rings, you equiv to a theorem about compute-rings, run the computation, and then come back

view this post on Zulip Jalex Stark (Jul 20 2020 at 18:34):

but we already don't have great machinery for doing this between two proof-y types

view this post on Zulip Jalex Stark (Jul 20 2020 at 18:36):

I guess we need automation for proving that a particular lemma is part of the theory of rings

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:36):

In the special case of computations, maybe it's not so much of an issue

view this post on Zulip Jalex Stark (Jul 20 2020 at 18:37):

why? is it because you want the theory of the computational type to be exactly the theory of the proving type?

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:37):

You could just apply computational_polynomial_equiv.injective, and then simp the equiv through the expression.

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:37):

Whereas for a generic lemma, it is not obvious that you are only multiplying and adding some variables.

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:38):

Otoh, I guess if there is an ite in there, then we might already need some specialized simp-lemmas. And maybe there is a polynomial.map, etc...

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:38):

So already, there will be quite some headache.

view this post on Zulip Mario Carneiro (Jul 21 2020 at 02:52):

Johan Commelin said:

In particular, what typeclasses currently don't allow, but what I would want to have from this "spec/impl" business, is that if I need to prove that some polynomial of degree 3 is irreducible over zmod 5, then I can just say exact dec_trivial and Lean should automatically figure out that it can translate the question to one of the computational implementations, and run the computation itself.

But this is exactly what dec_trivial does

view this post on Zulip Scott Morrison (Jul 21 2020 at 02:53):

(The point being you just need to provide the decidable instances that show how to do the translation.)

view this post on Zulip Mario Carneiro (Jul 21 2020 at 02:53):

The main issue is that we usually use "least common denominator" algorithms with relatively poor asymptotic complexity because we don't assume any extra structure on the classes

view this post on Zulip Mario Carneiro (Jul 21 2020 at 02:54):

but you could easily have multiple decidable instances for the same predicate with different priorities and additional typeclass assumptions for specialized procedures that aren't always applicable

view this post on Zulip Mario Carneiro (Jul 21 2020 at 02:56):

A nice warmup problem for this is to implement a decidable instance for a < b on nat that is O(log n)

view this post on Zulip Johan Commelin (Jul 21 2020 at 04:27):

Somehow, it's not good enough... because the decidable_* instances infect our definitions, and make it hard to prove generic stuff about the definitions.

view this post on Zulip Johan Commelin (Jul 21 2020 at 04:28):

Why are polynomials currently noncomputable? We didn't change any definitions, apart from ripping out decidable_* assumptions. But that's complete nonsense. If decidable_eq R is present, it should manage to compute even though that wasn't an assumption on the definition.

view this post on Zulip Floris van Doorn (Jul 21 2020 at 04:48):

I think using typeclasses for this is perfectly fine. To me it seems analogous to decidable:

  • With a proposition, we cannot construct data depending on whether it is true or false (without choice), so we tag it with a class decidable for the propositions for which we can
  • With a noncomputable def, I cannot compute. So I tag it with a class computable which contains an implementation and a proof that the implementation is equal to the noncomputable def. Now I can compute with the implementation.

I think you can do something like this:

class computes {α : Sort*} (x : α) :=
(val : α)
(certificate : x = val)

def compute {α : Sort*} (x : α) [computes x] : α := computes x.val

def computable_fun {α : Sort*} {β : α  Sort*} (f : Π x, β x) := Π x, computes (f x)

view this post on Zulip Reid Barton (Jul 21 2020 at 20:58):

This only supports "heavy rfl"-style computation though, right?

view this post on Zulip Reid Barton (Jul 21 2020 at 21:05):

For me norm_num is the model here--norm_str was a joke but there's no reason not to have a norm_poly that can compute things like degrees and whether polynomials are irreducible, regardless of whether polynomial is itself computable or not.

view this post on Zulip Reid Barton (Jul 21 2020 at 21:08):

The question in my mind is how to design this in a coherent way where norm_poly knows to invoke norm_num to decide whether a coefficient is zero if that makes sense, but maybe to invoke norm_poly if the coefficient is actually another polynomial, etc.

view this post on Zulip Reid Barton (Jul 21 2020 at 21:10):

This is not the same as decidable_eq--that one is an internal notion of decidability (which is classically trivial) but here we want an algorithm to (attempt to) decide whether two terms are provably equal.

view this post on Zulip Mario Carneiro (Jul 22 2020 at 08:54):

Reid Barton said:

The question in my mind is how to design this in a coherent way where norm_poly knows to invoke norm_num to decide whether a coefficient is zero if that makes sense, but maybe to invoke norm_poly if the coefficient is actually another polynomial, etc.

The way I would like this to be implemented is as plugins for norm_num, so that it can handle things other than simple numeric computations but can also do basic beta reduction and definition expansion for unknown functions, as well as decision procedures for things like matrix and polynomial computation. At that point it becomes more of a general purpose evaluator so the name norm_num will not fit anymore, but that's how I imagine it evolving.

view this post on Zulip Mario Carneiro (Jul 22 2020 at 08:56):

By the way, I sort of hinted at this above but it's actually possible to compute on terms using well crafted typeclass instances

view this post on Zulip Mario Carneiro (Jul 22 2020 at 09:02):

Since no one solved the puzzle, here's the solution:

import data.num.lemmas

class to_num (n : ) := (x : num) (eq : x = n)

instance to_num.zero : to_num 0 := 0, rfl
instance to_num.one : to_num 1 := 1, rfl
instance to_num.bit0 {a} [to_num a] : to_num (bit0 a) := bit0 (to_num.x a), by simp [to_num.eq]
instance to_num.bit1 {a} [to_num a] : to_num (bit1 a) := bit1 (to_num.x a), by simp [to_num.eq]

instance decidable_lt {a b : } [to_num a] [to_num b] : decidable (a < b) :=
decidable_of_iff (to_num.x a < to_num.x b) $ by simp [to_num.eq]

set_option class.instance_max_depth 1000
example : 345813045810345183 < 2351384051340513405 := dec_trivial

This is pretty fast even though it does only kernel computation

view this post on Zulip Mario Carneiro (Jul 22 2020 at 09:03):

The instance max depth only needs to be raised because the depth is proportional to the size of the numbers, and those numbers are not 32 bit

view this post on Zulip Mario Carneiro (Jul 22 2020 at 09:07):

With a simple extension we can get fast kernel addition and multiplication on nat as well:

instance to_num.add {a b : } [to_num a] [to_num b] : to_num (a + b) :=
to_num.x a + to_num.x b, by simp [to_num.eq]
instance to_num.mul {a b : } [to_num a] [to_num b] : to_num (a * b) :=
to_num.x a * to_num.x b, by simp [to_num.eq]

set_option class.instance_max_depth 1000
example : 500 * 500 * 500 * 39 < 235138405 * 134051340 + 12 := dec_trivial

view this post on Zulip Mario Carneiro (Jul 22 2020 at 09:15):

Also notice that this can also easily be adapted to prove things like (3 * 4 : real) < 17

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 10:00):

Mario that is_really_ cool :D

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 10:00):

Can it prove 617 is prime?

view this post on Zulip Mario Carneiro (Jul 23 2020 at 02:03):

The limitation of this technique is that it can't do "nondeterministic" computation like tactics can, so you don't get short certificate proofs (for example to prove non-primality). Also the best environment for this uses the semidecidable class instead of decidable (which I think still has yet to be defined because of bikeshedding over the name, but is basically option p), because many kinds of proof methods aren't actually decision procedures, for example proving that numerals are equal in a possibly nonzero characteristic ring

view this post on Zulip Mario Carneiro (Jul 23 2020 at 02:04):

But for proving primality, you aren't really doing any short circuiting anyway for a proof by trial division, so you could do something similar there. I would have to write the num.prime decision procedure first though

view this post on Zulip Mario Carneiro (Jul 23 2020 at 05:11):

Using #3525, this method also extends to primality proofs:

import data.num.prime

instance decidable_prime {a : } [to_num a] : decidable (nat.prime a) :=
decidable_of_iff (num.prime (to_num.x a)) $ by simp [to_num.eq]

example : nat.prime 617 := dec_trivial -- takes about 200 ms

view this post on Zulip Kevin Buzzard (Jul 23 2020 at 06:55):

Everything is trivial

view this post on Zulip Anne Baanen (Jul 23 2020 at 09:15):

Relevant link: https://aphyr.com/posts/342-typing-the-technical-interview


Last updated: May 10 2021 at 18:22 UTC