How exactly do I do self-referential definitions?

Stream: new members

[Abhimanyu Pallavi Sudhir]

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]

trans_gen

[Kevin Buzzard]

Take the transitive closure of your original relation

[Mario Carneiro]

isn't this just <?

[Kenny Lau]

import logic.relation

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

def R := relation.trans_gen original

[Kenny Lau]

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

[Kenny Lau]

alternatively:

[Kenny Lau]

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

[Kevin Buzzard]

Now you can prove things about R by induction

[Kevin Buzzard]

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

[Abhimanyu Pallavi Sudhir]

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

[Kenny Lau]

not anything.

[Kevin Buzzard]

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]

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

[Kenny Lau]

to emphasize that it is decidable

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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]

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

[Abhimanyu Pallavi Sudhir]

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

[Kenny Lau]

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

[Kevin Buzzard]

I think it's fine.

[Kenny Lau]

Prop is a strange thing

[Kenny Lau]

you can have non-decidable propositions

[Kenny Lau]

that doesn't make it noncomputable

[Abhimanyu Pallavi Sudhir]

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

[Kenny Lau]

it isn't

[Kenny Lau]

you're just defining a proposition

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

you just can't evaluate that statement

[Abhimanyu Pallavi Sudhir]

Yeah, you're right, I got confused.