# Zulip Chat Archive

## Stream: general

### Topic: computation vs proving

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

#### Johan Commelin (Jul 20 2020 at 18:25):

Probably lots of people have thought about this before.

#### Johan Commelin (Jul 20 2020 at 18:25):

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

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

#### Johan Commelin (Jul 20 2020 at 18:27):

Of course we *can* do that with typeclasses.

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

#### 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]
```

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

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

#### Johan Commelin (Jul 20 2020 at 18:32):

Does that even make sense?

#### Jalex Stark (Jul 20 2020 at 18:33):

this is the `equiv_rw`

problem, right?

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

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

#### Jalex Stark (Jul 20 2020 at 18:34):

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

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

#### Johan Commelin (Jul 20 2020 at 18:36):

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

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

#### Johan Commelin (Jul 20 2020 at 18:37):

You could just apply `computational_polynomial_equiv.injective`

, and then simp the equiv through the expression.

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

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

#### Johan Commelin (Jul 20 2020 at 18:38):

So already, there will be quite some headache.

#### Mario Carneiro (Jul 21 2020 at 02:52):

Johan Commelin said:

In particular, what typeclasses currently don't allow, but what I

would wantto 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 (Jul 21 2020 at 02:53):

(The point being you just need to provide the `decidable`

instances that show how to do the translation.)

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

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

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

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

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

#### 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)
```

#### Reid Barton (Jul 21 2020 at 20:58):

This only supports "heavy `rfl`

"-style computation though, right?

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

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

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

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

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

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

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

#### 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
```

#### 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`

#### Kevin Buzzard (Jul 22 2020 at 10:00):

Mario that is_really_ cool :D

#### Kevin Buzzard (Jul 22 2020 at 10:00):

Can it prove 617 is prime?

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

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

#### 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
```

#### Kevin Buzzard (Jul 23 2020 at 06:55):

Everything is trivial

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