## Stream: new members

### Topic: noncomputable

#### Paul van Wamelen (Feb 17 2020 at 16:08):

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 (Feb 17 2020 at 16:12):

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 (Feb 17 2020 at 16:29):

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

#### Chris Hughes (Feb 17 2020 at 16:31):

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 (Feb 17 2020 at 16:37):

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

#### Kevin Buzzard (Feb 17 2020 at 17:16):

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 (May 07 2020 at 01:42):

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 (May 07 2020 at 01:43):

noncomputable has nothing to do with computation in this sense

#### Mario Carneiro (May 07 2020 at 01:44):

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

#### Alexandre Rademaker (May 07 2020 at 01:45):

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

#### Mario Carneiro (May 07 2020 at 01:45):

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 (May 07 2020 at 01:45):

constant is the same as axiom

#### Alexandre Rademaker (May 07 2020 at 01:46):

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

#### Mario Carneiro (May 07 2020 at 01:47):

You may want to consider using variable or parameter here

#### Alexandre Rademaker (May 07 2020 at 01:47):

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 (May 07 2020 at 01:48):

you can probably do that using typeclass inference

#### Alexandre Rademaker (May 07 2020 at 01:50):

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 (May 07 2020 at 01:51):

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 (May 07 2020 at 01:53):

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 (May 07 2020 at 01:57):

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 (May 07 2020 at 02:05):

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

#### Mario Carneiro (May 07 2020 at 02:06):

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

#### Mario Carneiro (May 07 2020 at 02:07):

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 (May 07 2020 at 02:07):

but it works in a pinch

#### Alexandre Rademaker (May 07 2020 at 02:08):

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 (May 07 2020 at 02:09):

Are you sure? What version of lean are you running

#### Mario Carneiro (May 07 2020 at 02:09):

I guessed that you modified your code to look like mine

#### Alexandre Rademaker (May 07 2020 at 02:10):

Oh, I got. Now I have just green marks

#### Mario Carneiro (May 07 2020 at 02:10):

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

#### Alexandre Rademaker (May 07 2020 at 02:12):

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 (May 07 2020 at 02:13):

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

#### Mario Carneiro (May 07 2020 at 02:16):

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 (May 07 2020 at 02:22):

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 (May 07 2020 at 02:24):

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


#### Mario Carneiro (May 07 2020 at 02:27):

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 (May 07 2020 at 02:28):

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

#### Mario Carneiro (May 07 2020 at 02:33):

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 (May 07 2020 at 02:39):

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 (May 07 2020 at 02:41):

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 (May 07 2020 at 02:42):

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 (May 07 2020 at 02:44):

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 (May 07 2020 at 02:50):

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 (May 07 2020 at 02:53):

Mario Carneiro said:

Are you sure? What version of lean are you running

% lean -v
Lean (version 3.4.2, Release)

#### Mario Carneiro (May 07 2020 at 04:09):

@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 (May 07 2020 at 12:53):

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 (May 09 2020 at 05:44):

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