nonconstructive proofs

Stream: new members

[Lucas Teixeira]

Is it possible to write non constructive proofs in LEAN??

[Mario Carneiro]

yes

[Eric Wieser]

Yes, using docs#classical.choice

[Mario Carneiro]

Most mathematics in mathlib makes no attempt to be constructive

[Kevin Buzzard]

Mathematicians like playing in easy mode. They can get much further on in the quest that way.

[Will Sawin]

What fraction of the results in mathlib, if they were proved constructively, would produce a useful algorithm?

[Kevin Buzzard]

if it were useful it would be in core Lean, right?

[Kevin Buzzard]

The stuff where you can clearly do it constructively is in my experience mostly done constructively. Sometimes this makes it harder to use (or perhaps harder for beginners to use).

[Johan Commelin]

@Will Sawin Sometimes we use constructive results. But running time blows up quickly.

[Johan Commelin]

I think that Chris used it a couple of times when doing computations modulo small $n$, when he formalized quadratic reciprocity and sum of 4 squares

[Johan Commelin]

Because for small n you can just do computations by brute force, and if stuff is done constructively, the algorithm for the brute force is handed to you by Lean.

[Johan Commelin]

But in most cases the definitions that are good for elegant proofs are bad for fast computations.

[Yakov Pechersky]

We do computed proofs often via norm_num =)

[Yakov Pechersky]

But in terms of data structures, or enumerating over inductive data types, yes, a lot of algorithms are very slow.

[Kyle Miller]

Maybe another illustrative example is finite sets. To be as generic as possible, they're defined to be duplicate-free lists up to reordering. The only requirement they have is that there be an algorithm for testing equality. The only possible algorithm for testing set membership in this situation takes $O(n)$ time, since every element of that list must be compared for equality.

If finite sets could require that there be a computable total order, then that could be dropped down to $O(\ln n)$ using a tree representation for the finite set. Practical finite sets use hashing, which have $O(1)$ set membership (for small enough finite sets... so not completely accurate).

So, while finite sets are constructive, and most operations on them are constructive (in that they are backed by algorithms), they're not exactly the algorithms you'd want to use in practice.

There doesn't seem to be a good way to have multiple algorithms and data structures with different characteristics for the same mathematical object, short of redefining the object and proving all its properties multiple times...

It would be cool if there were a way to have the pure math version of an object then provide computational definitions along with hints for how Lean should evaluate something. Maybe even if there were a way to write a typeclass that could give computational meaning to noncomputable definitions, which I don't think is possible with the way noncomputable works.

[Kevin Buzzard]

Isn't this Lean 4's @implementedBy?

[Kevin Buzzard]

Johan Commelin said:

But in most cases the definitions that are good for elegant proofs are bad for fast computations.

A fabulous case in point being the natural numbers. Ever tried to prove multiplication is associative by binary induction (i.e. induction on length of binary representation of number)?

[Kyle Miller]

@Kevin Buzzard That's a bit different -- as far as I understand, it gives just one implementation for something. It would be nice if you could have different implementations depending on which typeclasses are available, since additional structure can allow for faster algorithms. You sort have to go for the lowest common denominator without this.

[Yakov Pechersky]

You could have a version of the function that has more constraints (your typeclass constraints), and that one is implementedBy

[Kevin Buzzard]

Right -- for example matrix multiplication is done very differently for sparse matrices compared with the generic case.

[Yakov Pechersky]

The sparse matrix case is hard, because how do you infer that you have a sparse matrix?

[Kevin Buzzard]

Because the user tells you? This is for people wanting to do computations, right? Don't ask me :-)

[Kevin Buzzard]

That's how it works in computer algebra packages, you just use the matrix multiplication function but give it some added switch to say "please use this algo at this point"

[Kevin Buzzard]

example using Sage

[Kyle Miller]

One way it seems you can work with noncomputable definitions and then provide (multiple) ways to compute them is through a "classicalized" version of a type. Every noncomputable value can be represented as a singleton set:

structure sval (α : Type u) :=
(s : set α)
(singleton : ∃ x, s = {x})

prefix `!`:100 := sval

def sval.incl {α : Type u} (x : α) : !α := ⟨{x}, x, rfl⟩

For example, the infimum of a set of natural numbers in noncomputable, but we can erase this keyword using this type:

def Inf' (s : set ℕ) : !ℕ := ⟨{Inf s}, _, rfl⟩

The next ingredient is a typeclass similar to decidable that provides a computation (when one is available):

class computable {α : Type*} (v : !α) :=
(compute : α)
(compute_spec : compute ∈ v.s)

def sval.compute {α : Type*} (v : !α) [computable v] : α := computable.compute v

For example, the infimum is computable if the set has decidable membership and if nonemptiness is decidable:

instance nat.Inf'_computable (s : set ℕ) [decidable_pred (∈ s)] [h : decidable s.nonempty] : computable (Inf' s) :=
... something involving nat.find ...

It can also be computable if you know exactly what the set is:

instance nat.Inf'_interval (a : ℕ) : computable (Inf' (set.Ici a)) := ⟨a, by simp [Inf']⟩

#eval (Inf' (set.Ici 100)).compute
-- 100

[Mario Carneiro]

By the way, sval is also known as docs#erased

[Kyle Miller]

It's not the most convenient to work with, but there are a few interesting Lean-computable equivalences.

• set (!α) ≃ set α
• !set α ≃ set α
• !(Π (x : α), β x) ≃ (Π (x : α), !β x) and !(α → β) ≃ (α → !β)

It's also a monad, so at least that's something.

[Kyle Miller]

@Mario Carneiro Thanks, I knew there had to be something like this already.

[Kyle Miller]

Here's a gist https://gist.github.com/kmill/a67dae0e6cdf8ff8897d37a0563f8d4b with the experiment

[Kyle Miller]

(I'd wanted to try making some computable classes that would demonstrate you could use ordset as an intermediate representation when taking some unions of finsets, but I didn't get to it, if it's even possible.)

[Kyle Miller]

That's nice that erased erases its data -- I'd worried about whether sval would develop enormous symbolic representations.

[Kyle Miller]

One more example of computable, for noncomputable finite sets (showing only some illustrative definitions and lemmas):

abbreviation finset' (α : Type*) := !finset α

instance : has_union (finset' α) :=
⟨λ s t, ⟨{u | by { classical, exact u = s.val ∪ t.val }}, _, rfl⟩⟩

lemma mem_union {s t : finset' α} (x : α) : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t :=
by { change x ∈ sval.incl _ ↔ _,  simp }

instance (s t : finset' α) [computable s] [computable t] [decidable_eq α] : computable (s ∪ t) := ...

abbreviation a : finset' ℕ := sval.incl {1,2}
abbreviation b : finset' ℕ := sval.incl {2,3,4}

#eval (a ∪ b).compute
-- {1, 2, 3, 4}

(This needs a and b to be reducible since it's relying on another instance that says anything created with sval.incl is computable.)

[Reid Barton]

This is pretty neat but it's worth considering the trade-off compared to something in the style of norm_num (or even simp). As an extreme example, in order to prove that a given number is composite, norm_num could invoke an external program to factor the number.

[Mario Carneiro]

Also, norm_num is allowed to fail sometimes, while decidability instances generally can't, unless you do the bulk of the computation in the typeclass inference search itself

[Reid Barton]

The biggest advantage of something like computable is that you get a meta-level proof that there is an algorithm to compute the thing... but if you only really care about actually computing it then this isn't really necessary.

[Reid Barton]

(this is basically the same as Mario's point that norm_num is allowed to fail)

[Kyle Miller]

Yeah, I don't think this is very useful for compile-time (the likes of norm_num and simp). It seems like it could be useful for when you want to compile programs and want to be able to automatically select good-ish algorithms.

[Kyle Miller]

while also being able to use the standard mathematical definitions, which come with a whole library of lemmas

[Reid Barton]

It's definitely an improvement over trying to make your algorithm be the definition, I think.

[Mario Carneiro]

For example, for interval arithmetic computations on real numbers it is convenient to make the calculation blow up if you divide by zero, but that means that the space of successfully evaluating terms is very complicated and depends on the output of previous computations

[Kyle Miller]

Reid Barton said:

The biggest advantage of something like computable is that you get a meta-level proof that there is an algorithm to compute the thing... but if you only really care about actually computing it then this isn't really necessary.

This all applies to decidable too, right?

One reason I was looking into this was to see whether decidable could feasibly be removed from all the mathematical definitions, and whether it could be relegated to computable instances.

[Mario Carneiro]

Yes, decidable has roughly the same characteristics as computable here

[Mario Carneiro]

decidable can't be removed from definitions with computational content, whether it is spelled decidable or computable

[Mario Carneiro]

Note that your finset' definition does not make finset obsolete, because it depends on finset

[Mario Carneiro]

the theorems about finset would continue to have all the same decidability assumptions

[Kyle Miller]

I designed computable to be the Type-level version of decidable -- I meant the question rhetorically.

And sure, I used finset to implement finset', but I didn't have to. The point of the example is that finset can be used as a computational backend to the classical notion of a finite set. finset certainly needs its decidability assumptions.

[Mario Carneiro]

It's not clear that we gain that much by having finset' though, compared to open_locale classical + finset

[Mario Carneiro]

It's certainly possible to have a version of finset with no computational content; finite does basically that

[Mario Carneiro]

explicitly erasing computational content isn't usually that productive, since it just removes some noncomputable markings

[Kyle Miller]

Based on your saying "whether it is spelled decidable or computable" I'm thinking what I said isn't clear:
Kyle Miller said:

One reason I was looking into this was to see whether decidable could feasibly be removed from all the mathematical definitions, and whether it could be relegated to computable instances.

This is what I'm referring to specifically:

instance (s t : finset' α) [computable s] [computable t] [decidable_eq α] : computable (s ∪ t) := ...

It's moving any trace of decidable from definitions and lemmas about mathematical definitions to descriptions of how you might compute them.

[Kyle Miller]

This is also a much more precise way to give computational meaning to expressions, since you can make use of any additional typeclasses the types might satisfy.

[Mario Carneiro]

It's still not good enough for e.g. selecting sparse matrix vs dense matrix representation, but sure, this works alright for decidable

[Reid Barton]

so for example, get rid of ite with its decidable argument, and instead write a computable instance for it which carries the decidable hypothesis

[Kyle Miller]

/-- ite, but without decidability -/
def ite' {α : Type*} (c : Prop) (x y : !α) : !α :=
⟨{v | (c → v ∈ x.s) ∧ (¬c → v ∈ y.s)},
begin
  by_cases c,
  { use x.val, simp [h], },
  { use y.val, simp [h], },
end⟩

/-- When the proposition is decidable, compute the ite' with ite. -/
instance ite'.compute {α : Type*} (c : Prop) [decidable c] (x y : !α) [computable x] [computable y] : computable (ite' c x y) :=
⟨ite c x.compute y.compute,
begin
  unfold ite',
  dsimp,
  simp {contextual:=tt},
end⟩

[Kyle Miller]

This is using the ! type, which is annoying -- I wish it were more seamless -- but in principle it seems to work.

[Reid Barton]

I was thinking of a noncomputable version

[Mario Carneiro]

You can write ite' more simply as launder (by classical; exact ite c x y) where launder is an identity function on !α that makes any term computable

[Mario Carneiro]

Proving these things can be annoying for recursive functions though

[Mario Carneiro]

I would rather come at this from the other direction: introduce ite' and use it only when the decidability argument gets in the way

[Mario Carneiro]

(and it would be defined simply as by classical; exact ite c x y, noncomputable notwithstanding)

[Kyle Miller]

It would be nice if there were a way to coerce noncomputable terms to !α. It's not clear to me how you'd do it without the coercion itself being noncomputable.

[Kyle Miller]

I didn't fully understand what launder was about -- did you mean it would be this coercion?

[Mario Carneiro]

import data.erased

axiom magic : erased ℕ

noncomputable def magic' : erased ℕ := magic -- if we use it directly, it is noncomputable

def magic'' : erased ℕ := ⟨magic.1, magic.2⟩ -- laundering it makes it computable

def launder {α} (s : erased α) : erased α := ⟨s.1, s.2⟩

-- Using launder directly doesn't work, because lean doesn't unfold it
noncomputable def magic''' : erased ℕ := launder magic

notation `launder` s := ⟨s.1, s.2⟩

-- @[inline] also doesn't work (and lean 3 doesn't have macroInline), but a notation does
def magic'''' : erased ℕ := launder magic

[Mario Carneiro]

Oh, looks like abbreviation works, wasn't expecting that

[Jake Levinson]

Hi @Mario Carneiro and @Kyle Miller , I found this thread by searching for "nonconstructive ite". Did anything like this end up getting added to mathlib? (I hope it's ok to respond to an old thread)

Mario Carneiro said:

It's not clear that we gain that much by having finset' though, compared to open_locale classical + finset

Quick comment -- I ran into problems a few weeks ago from trying to use open_locale classical + finset, problems coming from decidability diamonds. Basically the solution I was told was to explicitly provide decidability instances rather than using open_locale classical.

I don't really understand decidability, but (now that I'm trying to use it appropriately) I just ran into a similar kind of problem with two superficially identical ite expressions with different decidability instances. It would definitely be very nice to have a way to do this that doesn't involve any decidability at all.

[Kevin Buzzard]

Yes, open_locale classical was an attempt to fix some decidability issues but now there are better ways (the rule of thumb is that if the statement of a declaration needs one then add it as an assumption, and if a proof needs one then use the classical tactic). This is what you do in the other thread but you still seem to get into problems :-/

[Jake Levinson]

I do appreciate your help :smile: