redundant definitions/ifndef

Stream: new members

[moenarch]

Hi, I just started trying out lean3, and I'm curious if there is an elegant way to deal with circular/redundant definitions. By that I mean triangles like bachelor/husband/man. You can define

• bachelor as a man who is not a husband,
• husband as a man who is not a bachelor, and
• man as husband or bachelor.
  So in cases like these, were you only need two to get the third, do I have to randomly or intuitively pick two, or is there an advanced way to handle this?

[Patrick Massot]

This is really hard to tell without a more realistic example. In the exact example you described, you could define

inductive man
| husband : man
| bachelor : man

[Patrick Massot]

If you don't understand the above code, which could very well be true if you are at a pretty early stage, then you should read more of #tpil.

[Patrick Massot]

specifically Chapter 7

[moenarch]

In chapter 3 of #tpil we are introduced to and, or, not and implies

constant and : Prop → Prop → Prop
constant or : Prop → Prop → Prop
constant not : Prop → Prop
constant implies : Prop → Prop → Prop

variables p q r : Prop
#check and p q                      -- Prop
#check or (and p q) r               -- Prop
#check implies (and p q) (and q p)  -- Prop

afaik, it is possible to define the implication of a and b as the disjunction of not-a and b.

constant and2 : Prop → Prop → Prop
constant or2 : Prop → Prop → Prop
constant not2 : Prop → Prop

def implies2 (a b : Prop) := (or2 (not2 a) b)

#check implies2

So my question is if

• there is some kind of special way to deal with this,
• I just have to pick one of them which I define in virtue of the others, or
• I just define all 4 and then some kind of transformations.

[Patrick Massot]

This example is again very special because the foundation we use allow to be constructive and then you can't define implication like this. Anyway, there will always be cases where you need to pick a definition as being the official definition and then prove lemmas offering alternative equivalent formulations. In practice this isn't a problem.

[moenarch]

I think I found what I was looking for. It's mutual. Thank you for your help.

[Eric Wieser]

mutual is for when there's actually a loop that can't be broken - if you give an example of how you're using it, someone here can likely comment on whether there's a better way