## Stream: new members

### Topic: How exactly do I do self-referential definitions?

#### Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:34):

I'm trying to define a relation R such that for all x, x R (x + 1) and transitive R. Now I know I could probably do this inductively, but I don't want to (because I want the method to apply even if I had, e.g. symmetric R). My instinct was to use a non-constructive definition, like this (I know this is nonsense, but it's just a sketch of what I want to do):

local attribute [instance] classical.prop_decidable
noncomputable def double_cosets (x y : ℤ): ℤ → ℤ → Prop :=
if y = x + 1 then true
transitivity double_cosets


But that doesn't work because

1. true becomes the value of a relation, when I really want that to be the proposition it maps to.
2. Lean doesn't understand the self-reference.

How do I define it?

#### Kenny Lau (Oct 14 2018 at 20:35):

trans_gen

#### Kevin Buzzard (Oct 14 2018 at 20:35):

Take the transitive closure of your original relation

#### Mario Carneiro (Oct 14 2018 at 20:36):

isn't this just <?

#### Kenny Lau (Oct 14 2018 at 20:36):

import logic.relation

inductive original : ℕ → ℕ → Prop
| r : ∀ n, original n (n+1)

def R := relation.trans_gen original


#### Kenny Lau (Oct 14 2018 at 20:37):

@Mario Carneiro I think he wants to experiment instead of creating new things

alternatively:

#### Kenny Lau (Oct 14 2018 at 20:37):

inductive R : ℕ → ℕ → Prop
| basic : ∀ n, R n (n+1)
| trans : ∀ a b c, R a b → R b c → R a c


#### Kevin Buzzard (Oct 14 2018 at 20:38):

Now you can prove things about R by induction

#### Kevin Buzzard (Oct 14 2018 at 20:38):

It might be interesting to look at the definition of < on the natural numbers at this point

#### Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:39):

Huh, that makes sense. So induction can be used for anything self-referential?

not anything.

#### Kevin Buzzard (Oct 14 2018 at 20:39):

and to tie this up with an earlier conversation, you could even look at the proof that < on nat is decidable, which is an algorithm which, given two nats, spits out which is the smallest.

#### Kenny Lau (Oct 14 2018 at 20:40):

and I would define a function N -> N -> bool instead

#### Kenny Lau (Oct 14 2018 at 20:40):

to emphasize that it is decidable

#### Mario Carneiro (Oct 14 2018 at 20:41):

Whenever you want the "least relation satisfying some properties" that's an inductive predicate

#### Kenny Lau (Oct 14 2018 at 20:41):

and "smallest type closed under some operations" is an inductive type

#### Mario Carneiro (Oct 14 2018 at 20:41):

the relation doesn't have to be decidable, and the proof that it is usually goes by rather different methods than the original

#### Mario Carneiro (Oct 14 2018 at 20:42):

There are interesting examples of nondecidable predicates like "in the span of s" in a group

#### Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:43):

So what is the noncomputable kind of definition for? Isn't my definition non-constructive?

#### Kenny Lau (Oct 14 2018 at 20:44):

inductive things are always computable, it's definition that is noncomputable

#### Kevin Buzzard (Oct 14 2018 at 20:44):

I think it's fine.

#### Kenny Lau (Oct 14 2018 at 20:44):

Prop is a strange thing

#### Kenny Lau (Oct 14 2018 at 20:44):

you can have non-decidable propositions

#### Kenny Lau (Oct 14 2018 at 20:44):

that doesn't make it noncomputable

#### Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:44):

No, I get that -- my point is that the definition is non-constructive, isn't it?

it isn't

#### Kenny Lau (Oct 14 2018 at 20:45):

you're just defining a proposition

#### Mario Carneiro (Oct 14 2018 at 20:45):

it is not nonconstructive because you aren't actually constructing anything

#### Kenny Lau (Oct 14 2018 at 20:45):

it's like you can write down what it means for a program to halt

#### Kenny Lau (Oct 14 2018 at 20:45):

you just can't evaluate that statement

#### Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:47):

Yeah, you're right, I got confused.

Last updated: May 13 2021 at 20:13 UTC