computation vs proving

Stream: general

[Johan Commelin]

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.

[Johan Commelin]

Probably lots of people have thought about this before.

[Johan Commelin]

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

[Johan Commelin]

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?

[Johan Commelin]

Of course we can do that with typeclasses.

[Johan Commelin]

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

[Johan Commelin]

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]

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

Does that even make sense?

[Jalex Stark]

this is the equiv_rw problem, right?

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Johan Commelin]

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

[Jalex Stark]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

So already, there will be quite some headache.

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Floris van Doorn]

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)

[Reid Barton]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Mario Carneiro]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Mario that is_really_ cool :D

[Kevin Buzzard]

Can it prove 617 is prime?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Everything is trivial

[Anne Baanen]

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