Computable equivalence of types

Stream: new members

[Jair Taylor]

Hello! As an exercise for myself, I am trying to prove some facts about binary trees, namely that they are counted by Catalan numbers. I was hoping to show that the type of trees with n leaves is a Fintype, so that I could do an #eval and actually list off the trees with n leaves. Unfortunately, Lean warns me this definition is noncomputable, and I was wondering if anyone could give me tips on how to fix that.

I have the definitions

inductive BT where -- A binary tree is either
  | leaf : BT -- a leaf or
  | node : BT → BT → BT -- a pair of binary trees.

open BT

def NumLeaves (T : BT) : ℕ :=
  match T with
  | leaf => 1
  | node T2 T3 => NumLeaves T2 + NumLeaves T3

def HasNumLeaves (T: BT) (n: ℕ) : Prop := NumLeaves T = n
def BTWithNumLeaves (n : ℕ) : Type := {T : BT // (HasNumLeaves T n)}

and I was able to prove the equivalence

def TreeEq (n: ℕ) (nz: n > 1): BTWithNumLeaves n ≃ Σ (k : Fin (n-1)), ( (BTWithNumLeaves (k+1)) × (BTWithNumLeaves (n-k-1)))

and used this with strong induction to show

def Treefin (n: ℕ) (nz: n > 0): Fintype (BTWithNumLeaves n)

but Lean warns me this is noncomputable. The problem seems to be with the base case

def LeafFinite: Fintype (BTWithNumLeaves 1)

which is also noncomputable. My proof of LeafFinite is here.

I wonder if the problem is this lemma where I use contradiction:

lemma SingletonLeaf (T: BT) (h: NumLeaves T = 1): T = leaf := by {
  induction T with
  | leaf => {
    rfl
   }
  | node T2 T3 _ => {
    have h3: NumLeaves T2 + NumLeaves T3 ≥ 2 := Nat.add_le_add (BTsPosLeaves1 T2) (BTsPosLeaves1 T3)
    have h4: NumLeaves T2 + NumLeaves T3 ≠ 1 :=  Nat.ne_of_lt' h3
    exact (h4 h).elim
  }
}

and if so if there's a way to prove this in a computable way.

[Kevin Buzzard]

If you're just trying to prove a theorem then you typically don't need to worry about whether things are computable or not.

[Jair Taylor]

That's true. I just find it more aesthetically pleasing if things are computable.

[Mario Carneiro]

no I think that's not the issue, usage of classical logic is independent of whether things are noncomputable

[Mario Carneiro]

the way in which you prove a theorem will not impact noncomputable

[Mario Carneiro]

The problem is that you marked an Equiv as a lemma (LeafEquiv is data, it also needs to be computable), and the reason this is noncomputable is because you used Equiv.equivOfUnique which skips the construction of an inverse function

[Mario Carneiro]

oh no, actually everything you used is computable already. You just mistakenly marked LeafInhabited, LeafUnique, and LeafEquiv as lemma instead of def

[Mario Carneiro]

#lint will tell you about this

[Jair Taylor]

oh, nice! OK, that's a simple fix. Thanks so much.

[Jair Taylor]

Ah, but now another issue: in my proof of Fintype (BTWithNumLeaves n) I am seeing

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Nat.strongInductionOn', and it does not have executable code

So is there an alternative to Nat.strongInductionOn that is computable?

[Mario Carneiro]

usually you can rewrite it as a well founded recursion, where the termination arguments correspond to uses of the inductive hypothesis

[Jair Taylor]

OK, I will look into well founded recursion. Thank you!

[Eric Wieser]

Jair Taylor said:

Ah, but now another issue: in my proof of Fintype (BTWithNumLeaves n) I am seeing

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Nat.strongInductionOn', and it does not have executable code

Am I right in thinking this is a bug?

[Joachim Breitner]

Maybe more a missing feature, I'd say.

[Matt Diamond]

kinda weird that docs#IsWellFounded.fix is computable while docs#WellFounded.fix isn't

[Matt Diamond]

in fact, the former appears to be defined in terms of the latter so I'm not sure how that's possible

[Joachim Breitner]

There is some trickery in Std to define a computable fix and then set

@[csimp] private theorem fix_eq_fixC : @fix = @fixC := rfl

Full details at https://github.com/leanprover/std4/blob/975b766b35f07e81fc34d66d026ad5bb2c1dbf45/Std/WF.lean#L10-L39

[Matt Diamond]

I'm curious if @Jair Taylor's computability problem would be fixed by switching from docs#Nat.strongInductionOn to docs#Nat.strong_induction_on

unless the fundamental problem is that it's a theorem and therefore can't be used to create data

[Jair Taylor]

No, it's a definition.

def Treefin (n: ℕ) (nz: n > 0): Fintype (BTWithNumLeaves n) := by {
  induction n using Nat.strongInductionOn with
  | ind n ih => { ... }

I wasn't familiar with strong_induction_on but I think I can't use it here since it's only for Prop. I get

type mismatch when assigning motive
  fun n => ℕ
has type
  ℕ → Type : Type 1
but is expected to have type
  ℕ → Prop : TypeLean 4

[Matt Diamond]

Sorry, I meant the issue being that Nat.strongInductionOn and Nat.strong_induction_on are theorems. But you're right about Nat.strong_induction_on only working for Prop... I didn't notice that difference, so I don't think it will help after all.

[Matt Diamond]

I'll just add that creating data in tactic mode is generally a bad idea anyway (or at least it was in Lean 3)

[Jair Taylor]

Oh I see. Actually, if I just copy the definition of strongInductionOn but change it from theorem to def, that seems to resolve the issue!

[Joachim Breitner]

Matt Diamond said:

I'll just add that creating data in tactic mode is generally a bad idea anyway (or at least it was in Lean 3)

Is that so? Depends on what you do; I'd expect some set of tactics (apply, cases, induction etc.) to be fairly innocent

[Joachim Breitner]

Often a recursive definition is easier to work with than strong_induction_on. (As Mario already said earlier)

[Eric Wieser]

It's often very handy to assemble large terms with refine in tactic mode; in Lean 3, sometimes it was ever necessary for better performance

[Matt Diamond]

ah, I see