noncomputable

Stream: new members

[Paul van Wamelen]

I'm trying

def to_complex (x : ℤ[ω]) : ℂ := x.re + x.im * (1 + I * real.sqrt 3) / 2

but getting definition 'to_complex' is noncomputable, it depends on 'complex.discrete_field'.
Is there some import or open that will "deal" with this? What are the consequences of ignoring the noncomputability of sqrt?
It looks like an interesting exercise to make real.sqrt computable (looks like there is a proof sketch in the comments of real.sqrt's definition). Is that worth trying? Is it just a matter of constructing the Cauchy sequence that converges to sqrt(n)?

[Reid Barton]

The real numbers as implemented in mathlib have no useful computational structure anyways (they are Cauchy sequences without any explicit rate of convergence). You should just put noncomputable theory at the top of your file if you are going to use the reals a lot.

[Paul van Wamelen]

Thanks!
Are you saying that even if we complete the proof of sqrt_aux_converges sqrt would still be "uncomputable"?

[Chris Hughes]

It would be computable in the sense that Lean wouldn't have the noncomputable tag, but it would not be computable in any practical sense. There is no computable function real -> bool for example, so there's basically nothing you can do with a "computable" function on the current implementation of the reals.

[Paul van Wamelen]

I think I see :)
Thanks again! (I must say I'm blown away by the support here...)

[Kevin Buzzard]

I tend to not put noncomputable theory at the top of my files, and then every time Lean complains something is noncomputable I just write noncomputable in front of it, so e.g. noncomputable def to_complex ... would also remove the error.

[Alexandre Rademaker]

Why for such simple theorems I need the noncomputable in front of the theorems?

constant Class : Type

-- SUMO immediateSubclass
constant subClass : Class → Class → Type

-- SUMO subclass
constant Inherits : Class → Class → Type

constant inhz (c : Class) : Inherits c c
constant inhs (c1 c2 c3 : Class) : subClass c1 c2 → Inherits c2 c3 → Inherits c1 c3

constants Human Hominid Entity : Class

constant human_hominid : subClass Human Hominid
constant hominid_entity : subClass Hominid Entity

noncomputable theorem test1 : Inherits Human Hominid :=
 inhs Human Hominid Hominid human_hominid (inhz Hominid)

noncomputable theorem test2 : Inherits Human Entity :=
 inhs Human Hominid Entity human_hominid (inhs Hominid Entity Entity hominid_entity (inhz Entity))

Is it possible, using some tactics, to let Lean come up of the proof terms automatically? That is, to synthesize the proof term?

[Mario Carneiro]

noncomputable has nothing to do with computation in this sense

[Mario Carneiro]

it's noncomputable because you can't directly execute the proofs because they use undefined constants

[Alexandre Rademaker]

undefined constants? but in my example, they are all defined.

[Mario Carneiro]

noncomputable theorem is an indication that you have incorrectly marked a def as a theorem, or you have a type where you wanted a prop. Are subClass and Inherits supposed to be propositions? They are named like such

[Mario Carneiro]

constant is the same as axiom

[Alexandre Rademaker]

No, subClass is supposed to be a dependent type and Inherits a function.

[Mario Carneiro]

You may want to consider using variable or parameter here

[Alexandre Rademaker]

actually, I would like to be able to have a term like inhs Human Hominid Hominid human_hominid (inhz Hominid) produced automatically for a type Inherits Human Hominid

[Mario Carneiro]

you can probably do that using typeclass inference

[Alexandre Rademaker]

Wow! Thank you Mario. Can you give me any reference to understand it better? Probably I have to read https://leanprover.github.io/theorem_proving_in_lean/type_classes.html, right?

[Alexandre Rademaker]

BTW, nice, I don't need the noncomputable with variables

constant Class : Type

-- SUMO immediateSubclass
constant subClass : Class → Class → Type

-- SUMO subclass
constant Inherits : Class → Class → Type

variable inhz (c : Class) : Inherits c c
variable inhs (c1 c2 c3 : Class) : subClass c1 c2 → Inherits c2 c3 → Inherits c1 c3

variables Human Hominid Entity : Class

variable human_hominid : subClass Human Hominid
variable hominid_entity : subClass Hominid Entity

theorem test1 : Inherits Human Hominid :=
 inhs Human Hominid Hominid human_hominid (inhz Hominid)

theorem test2 : Inherits Human Entity :=
 inhs Human Hominid Entity human_hominid (inhs Hominid Entity Entity hominid_entity (inhz Entity))

[Mario Carneiro]

constant Class : Type

-- SUMO immediateSubclass
@[class] constant subClass : Class → Class → Type

-- SUMO subclass
@[class] constant Inherits : Class → Class → Type

@[instance] constant inhz (c : Class) : Inherits c c
@[instance] constant inhs (c1 c2 c3 : Class) [Inherits c2 c3] [subClass c1 c2] : Inherits c1 c3

constants Human Hominid Entity : Class

@[instance] constant human_hominid : subClass Human Hominid
@[instance] constant hominid_entity : subClass Hominid Entity

noncomputable def test1 : Inherits Human Hominid := by apply_instance

noncomputable def test2 : Inherits Human Entity := by apply_instance

[Alexandre Rademaker]

thank you. I am getting two errors

.…    19  19 warning         definition 'test1' was incorrectly marked as noncomputable (lean-checker)
.…    19  27 error           maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
 state:
 ⊢ Inherits Human Hominid (lean-checker)

[Mario Carneiro]

You won't be able to use a variable for typeclass inference here. Instances have to be defs or constants

[Mario Carneiro]

The error is because you missed that I swapped the arguments to inhs

[Mario Carneiro]

I make no guarantees about the behavior of this typeclass search, and there are issues with infinite searches if it follows the wrong path

[Mario Carneiro]

but it works in a pinch

[Alexandre Rademaker]

I see. But I copied and pasted your code. So I didn't understand your point about the swapping of the arguments of inhs...

[Mario Carneiro]

Are you sure? What version of lean are you running

[Mario Carneiro]

I guessed that you modified your code to look like mine

[Alexandre Rademaker]

Oh, I got. Now I have just green marks

[Mario Carneiro]

but I don't know any version of lean where the noncomputable mark on the def is unnecessary

[Alexandre Rademaker]

Hum, I see. So I guess that I can't expect too much from Lean to synthesize proof terms as I was expecting with this approach I was investigating.

[Mario Carneiro]

there are other ways to do it but they are more complicated

[Mario Carneiro]

constant Class : Type

-- SUMO immediateSubclass
constant subClass : Class → Class → Type

-- SUMO subclass
constant Inherits : Class → Class → Type

constant inhz (c : Class) : Inherits c c
constant inhs (c1 c2 c3 : Class) : subClass c1 c2 → Inherits c2 c3 → Inherits c1 c3

constants Human Hominid Entity : Class

constant human_hominid : subClass Human Hominid
constant hominid_entity : subClass Hominid Entity

meta def prove_subclass : tactic unit :=
`[apply human_hominid] <|> `[apply hominid_entity]

meta def prove_inherits : tactic unit :=
`[apply inhz] <|> (`[apply inhs] >> prove_subclass >> prove_inherits)

noncomputable def test1 : Inherits Human Hominid := by prove_inherits

noncomputable def test2 : Inherits Human Entity := by prove_inherits

[Alexandre Rademaker]

In this article, https://www.molto-project.eu/sites/default/files/FinalSUMOCNL.pdf, the authors have an interesting idea of mapping a KIF ontology (a knowledge representation language) to dependent type. They used https://www.grammaticalframework.org that implements dependent types too. I am trying to adapt their solution to Lean. The idea is to model the taxonomy of classes. Later, I would expect Lean to automatically construct terms that proof a chain of subclasses like Human < Hominid < CognitiveAgent < Agent < ... < Entity.

[Alexandre Rademaker]

What impressed me was that I was expecting Lean to have a much more powerful type system. But in GF they were able to easily generate a term for a given type. Page 6 of the article. The command mean: give me a term for the type Inherits Human Hominid.

> gt -cat="Inherits Human Hominid"
(inhs Human Hominid Hominid Human_Class (inhz Hominid))

[Alexandre Rademaker]

Oh, sorry I was answering a question that you made in another thread! ;-)

[Mario Carneiro]

Reading the paper, I'm pretty sure you want subClass and Inherits to be props. The reason they use a dependent type is because that's the nearest equivalent to a proposition in a haskell-esque type theory

[Mario Carneiro]

I think gt -cat is doing something similar to lean's typeclass inference

[Mario Carneiro]

pages 5-6 read very much like a description of typeclass inference. I'm pretty sure that gt -cat is a prolog-like search

However, there are some types of axioms which could not be ported to SUMOGF, such as the ones that use quantification over classes, negative type declarations and axioms which use the predicates subclass, range or domain.

...which also predicts that negations in theorems would be problematic to represent this way, because instance search only works with horn clauses (from A , B, ... Y infer Z)

[Alexandre Rademaker]

Thank you, I will think more about the implications of moving to propositions. In the previous example of trying to prove a simple SUMO axiom in Lean, I used untyped FOL mapping to Lean - https://github.com/own-pt/common-sense-lean/blob/master/misc/bs.lean. This makes the simple proof very verbose. I had a single type https://github.com/own-pt/common-sense-lean/blob/master/misc/bs.lean#L21 and guards in the axioms https://github.com/own-pt/common-sense-lean/blob/master/misc/bs.lean#L96. I am trying to better use types and have a way to move from the class hierarchy to types.

Anyway, the use of tactics was interesting, thank you for sharing. Unfortunately, we needed to go back to constants and noncomputable...

[Mario Carneiro]

The reason lean gets lost with the initial version of inhs is because it builds up a stack subclass Human ?a /\ subclass ?a ?b /\ subclass ?b ?c /\ Inherits ?c Hominid -> Inherits Human Hominid that doesn't resolve because it keeps applying inhs to the last Inherits subgoal. It's similar to the left recursion problem in context free grammars

[Mario Carneiro]

I am curious if GF has the same problem if you stated inhs as Inherits c1 c2 → subClass c2 c3 → Inherits c1 c3 instead

[Alexandre Rademaker]

This is interesting. I moved subclass back to the original position and it is working for me

constant Class : Type

-- SUMO immediateSubclass
@[class] constant subClass : Class → Class → Type

-- SUMO subclass
@[class] constant Inherits : Class → Class → Type

@[instance] constant inhz (c : Class) : Inherits c c
@[instance] constant inhs (c1 c2 c3 : Class) [subClass c1 c2] [Inherits c2 c3] : Inherits c1 c3

constants Human Hominid Entity : Class

@[instance] constant human_hominid : subClass Human Hominid
@[instance] constant hominid_entity : subClass Hominid Entity

set_option class.instance_max_depth 100
set_option trace.class_instances true

noncomputable def test1 : Inherits Human Hominid := by apply_instance
noncomputable def test2 : Inherits Human Entity := by apply_instance

[Alexandre Rademaker]

Unfortunately, I can't test the change in GF, the code in https://github.com/GrammaticalFramework/gf-contrib/tree/master/SUMO is incomplete.

[Alexandre Rademaker]

Mario Carneiro said:

Are you sure? What version of lean are you running

% lean -v
Lean (version 3.4.2, Release)

[Mario Carneiro]

@Alexandre Rademaker So I had a go at simplifying your bs.lean, see https://gist.github.com/digama0/16c62d1af34212de2e3fba380d87c043 . You can't quite take care of everything with typeclass inference but almost all the proofs that look like typeclass inference can be done using it

[Alexandre Rademaker]

I see, thank you so much for your attention. I will read it carefully to understand the details. The main issue, I believe, is to understand the limitations of that approach. The comments not provable in the end means not probable with typeclass inference or not provable at all with this way to model classes and instances?

Still, I think the predicates and functions are not really typed, right? I can't say that partition : Class → Class → Class → Prop and 'using it' like:

axiom a67131 {c row0 row1 : Class} :
 (partition3 c row0 row1 ↔ (exhaustiveDecomposition3 c row0 row1 ∧ disjointDecomposition3 c row0 row1))

That is, I can't really internalize the class hierarchy in the types.

In Lean 3.4.2 almost all proofs reached the maximum class-instance resolution depth, and I set it to 1000.

[Mario Carneiro]

Alexandre Rademaker said:

I see, thank you so much for your attention. I will read it carefully to understand the details. The main issue, I believe, is to understand the limitations of that approach. The comments not provable in the end means not probable with typeclass inference or not provable at all with this way to model classes and instances?

Not provable from the axioms that were provided. Presumably you have omitted some axioms that are needed to prove these.

[Mario Carneiro]

Indeed, these predicates and functions are essentially untyped, and typeclass inference is having to solve a harder problem than it normally would because there are so few classes and so many instances. One simple way to improve this is to have one typeclass per property and try to minimize the number of two-argument typeclasses. And things like ins x Class are really calling out for a Class type as you indicate, which would eliminate the need to do any type class search, although you still have to do something about subtyping.

[Alex Zhang]

What is the function of putting noncomputable before instance?

noncomputable instance : inner_product_space ℝ (n → ℝ) :=
inner_product_space.of_core
sorry

[Eric Wieser]

Perhaps it helps to realize that instance is just short for @[instance] def, so this is just like putting noncomputable before a def.

[Alex Zhang]

What will be the difference in practice if I don't put the noncomputable?

[Kevin Buzzard]

It's not you who chooses -- Lean will tell you what's computable and what isn't, and you tag appropriately. Noncomputability is irrelevant if you just want to prove theorems, it just stops you doing things like #eval and #reduce, but there are plenty of other ways to evaluate things eg use theorems

[Eric Wieser]

Lean will give an error if you put noncomputable on something that is computable, or don't put it on something that isn't. Lean is trying to make you tell the human reader what is and is not computable, even though lean itself knows without you telling it

[Eric Wieser]

If you think your readers don't care, you can start your file with noncomputable theory and lean will stop complaining.

[Alex Zhang]

Why is this def noncomputable?

noncomputable def of_bijective {α β} (f : α → β) (hf : bijective f) : α ≃ β :=
(of_injective f hf.1).trans $ (set_congr hf.2.range_eq).trans $ equiv.set.univ β

[Yakov Pechersky]

Because it does not actually provide an explicit inverse function to f

[Alex Zhang]

Is it possible to make this computable by another proof?
def of_bijective {α β} (f : α → β) (hf : bijective f) : α ≃ β := sorry

[Kevin Buzzard]

No.

[Alex Zhang]

Oh, I see

[Alex Zhang]

I depends on axiom of choice.

[Kevin Buzzard]

https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/

[Yakov Pechersky]

If you see the other thread, you'll see that you don't actually care about the computability of that iso, because you need it solely in the context of a proof.

[Alex Zhang]

Currently, for the purpose of my work, I actually don't need to care about the computability of anything at all :)

[Alex Zhang]

Is it possible to make a computable instance? F is a finite field.

import field_theory.finite.basic

variables {F : Type*} [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]

def is_quad_residue (a : F) : Prop := ∃ b, a = b^2

noncomputable
instance (a : F) : decidable (is_quad_residue a) := by {simp[is_quad_residue], exact classical.dec (∃ (b : F), a = _)}

[Adam Topaz]

import field_theory.finite.basic

variables {F : Type*} [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]

@[derive decidable]
def is_quad_residue (a : F) : Prop := ∃ b, a = b^2

example (a : F) : decidable (is_quad_residue a) := by apply_instance

[Anne Baanen]

Similarly:

import field_theory.finite.basic

variables {F : Type*} [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]

def is_quad_residue (a : F) : Prop := ∃ b, a = b^2

instance (a : F) : decidable (is_quad_residue a) := by { unfold is_quad_residue, apply_instance }

[Yakov Pechersky]

Just know that the decidable instance it generates is a brute force search over the entirety of F.

[Adam Topaz]

Yakov Pechersky said:

Just know that the decidable instance it generates is a brute force search over the entirety of F.

As it should be!

[Adam Topaz]

It would be fun to make a decidable instance based on quadratic reciprocity :wink:

[David Wärn]

Euler's criterion and exponentiation by squaring might be easier

[Kevin Buzzard]

My instinct is that the QR proof is faster?

[Kevin Buzzard]

Am I wrong?

[Yakov Pechersky]

One would have to be careful to use a binary_rec pow definition and not the unary one.

[Kevin Buzzard]

I guess the repeated squaring would work for finite fields other than Z/p

[David Wärn]

Euler's criterion is easier to prove correct, but mathlib probably has all the theory needed to prove correctness of the QR algorithm. Both algorithms are very fast (polynomial in number of digits), but I would also guess that QR is faster by some constant factor

[Kevin Buzzard]

One reason for doing this would be that there are fast primality tests which use this stuff -- they fail quickly for non-primes.

[Bjørn Kjos-Hanssen]

What exactly is the meaning of noncomputable in Lean?

[Mario Carneiro]

not executable by the lean VM

[Bjørn Kjos-Hanssen]

That makes it sound like one day it may become executable...

[Bjørn Kjos-Hanssen]

And therefore become computable

[Mario Carneiro]

well sure, depending on what kind of evolution you have in mind

[Mario Carneiro]

you can rewrite a function to become computable

[Mario Carneiro]

#12301 is a recent example of exactly that

[Mario Carneiro]

in particular, just because a function is marked noncomputable does not mean there is not an equal function which is computable

[Mario Carneiro]

noncomputable def foo : nat := classical.some (⟨37, rfl⟩ : ∃ x : nat, x = 37)
def bar : nat := 37

example : foo = bar := classical.some_spec (⟨37, rfl⟩ : ∃ x : nat, x = 37)

[Mario Carneiro]

Using noncomputable! you can even force a computable definition to be noncomputable

def bar : nat := 37
noncomputable! def baz : nat := 37
example : bar = baz := rfl

[Bjørn Kjos-Hanssen]

Hmm so in particular, noncomputable means "Lean, don't try to compute a representation for this, just check whether it's logically correct"?

[Eric Wieser]

Usually it means "lean has told me it is unable to compute this"

[Reid Barton]

In practice it means that your function can't be run from a tactic