Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:35):

trans_gen

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 20:35):

Take the transitive closure of your original relation

view this post on Zulip Mario Carneiro (Oct 14 2018 at 20:36):

isn't this just <?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:37):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:37):

alternatively:

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 20:38):

Now you can prove things about R by induction

view this post on Zulip 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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:39):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:39):

not anything.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:40):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:40):

to emphasize that it is decidable

view this post on Zulip Mario Carneiro (Oct 14 2018 at 20:41):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:41):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 20:42):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:43):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:44):

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

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 20:44):

I think it's fine.

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:44):

Prop is a strange thing

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:44):

you can have non-decidable propositions

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:44):

that doesn't make it noncomputable

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:45):

it isn't

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:45):

you're just defining a proposition

view this post on Zulip Mario Carneiro (Oct 14 2018 at 20:45):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:45):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:45):

you just can't evaluate that statement

view this post on Zulip 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