Making codependent functions

Stream: lean4

[Hannah Santos]

Is there a way I can do this?

open Nat

def even : Nat → Bool
  | 0 => true
  | succ n => odd n

def odd : Nat → Bool
  | 0 => false
  | succ n => even n

/-Exemple_even_odd.lean:5:19
Messages (1)
Exemple_even_odd.lean:5:14
unknown identifier 'odd'
All Messages (1)-/

[Patrick Massot]

mutual
def even : Nat → Bool
  | 0 => true
  | succ n => odd n

def odd : Nat → Bool
  | 0 => false
  | succ n => even n
end

[Hannah Santos]

Thank you!

[Patrick Massot]

However my understanding is that those mutual definitions are not so easy to work with (I don’t know for sure because they never seem to show up in math), so you would probably be happier with a less fancy way.

[Patrick Massot]

Let me add one trick: you don’t really need that open Nat, you can replace succ by .succ is your patterns. I’m not saying that opening Nat is bad, I’m only telling you this in case you don’t know you can use this dot notation when Lean knows what type to expect.

[Floris van Doorn]

I believe mutual defs are perfectly fine (though I'm not sure, I never worked with any). Mutual inductives don't have great support in Lean (yet?).

[Patrick Massot]

I guess the question is whether the equations generated automatically will be nice to work with.

[Hannah Santos]

I just wanted to write a proof with them, so that's actually fine.

[Hannah Santos]

(About how there's only one function that could be the one I'm looking for)

[Henrik Böving]

Floris van Doorn said:

I believe mutual defs are perfectly fine (though I'm not sure, I never worked with any). Mutual inductives don't have great support in Lean (yet?).

The mutual recursion that you are seeing above is already using well founded recursion under the hood so it can (but does not necessarily have to) get quite annoying quite quickly

[Floris van Doorn]

What can get annoying? Proving termination?
Once you have defined the mutual defs (including termination proof), then Lean generates equation lemmas exactly as you wrote them, so it should be fine to prove stuff about these functions, right?

[Joachim Breitner]

No (or rather unreliable) definitional equality, and sometimes slow elaboration/type checking if lean tries to start unfolding things are two annoyances that I know of.

[Henrik Böving]

Floris van Doorn said:

What can get annoying? Proving termination?
Once you have defined the mutual defs (including termination proof), then Lean generates equation lemmas exactly as you wrote them, so it should be fine to prove stuff about these functions, right?

(Lean only generates the equational theorems on demand, hence why i prove a theorem with them before printing them, but thats besides the point)

consider:

mutual
def even : Nat → Bool
  | 0 => true
  | n + 1 => odd n

def odd : Nat → Bool
  | 0 => false
  | n + 1 => even n
end

theorem test : even 0 = true := by rw [even]

#print test
#print even._eq_1

that's not really a "nicely" proven theorem (though automation is good enough to work with it quite often). In
general once well founded stuff shows up terms like this are present quite often which can make our automation struggle.

If you compare to a direct definition:

def even' (n : Nat) : Bool :=
  match n with
  | 0 => true
  | 1 => false
  | n + 2 => even' n


theorem test' : even' 0 = true := by rw [even']

#print test'
#print even'._eq_1

that one is much more harmless as you can see.

[Joachim Breitner]

(and the point that's besides the point won't be necessary in the next lean release, then even.eq_1 will just exist)