Countability of inductive type

Stream: maths

[Violeta Hernández]

I'm working with the following definition:

inductive PreCantor : Type
  /-- The ordinal `0` -/
  | zero : PreCantor
  /-- The ordinal `oadd e n a = ω ^ e * n + a` -/
  | oadd : PreCantor → ℕ+ → PreCantor → PreCantor

It seems clear to me that this type must be countable. Specifically, one can subdivide the type into "layers" based on the number of applications of the constructor oadd. The cardinality c (n + 1) of layer n + 1 is equal to c n * ℵ₀ * c n, which through a simple induction implies c n = ℵ₀ and thus that the entire type is countable.

It seems like this argument should follow in more generality, however. Specifically, any inductive type α whose constructors β₁ → β₂ → ... → α refer only to α and other countable types should be countable. Is there some sort of machinery already in Mathlib formalizing these sorts of arguments?

[Violeta Hernández]

I'm reminded of the docs#WType API, but I don't understand WType enough to know whether this is an instance of it or not

[Violeta Hernández]

I think this can be injected into a WType where the possible labels are in Option ℕ, with 0 representing zero, other natural numbers representing themselves, and none representing the oadd constructor

[Kyle Miller]

Ideally we would have deriving Countable for this.

An idea I've played around with before is to define a type simpler than WType specifically for doing Countable arguments. Basically, once you have that S is Countable in the following, it becomes fairly easy to implement the deriving Countable handler.

inductive PreCantor : Type
  /-- The ordinal `0` -/
  | zero : PreCantor
  /-- The ordinal `oadd e n a = ω ^ e * n + a` -/
  | oadd : PreCantor → ℕ+ → PreCantor → PreCantor

inductive S : Type where
  | nat (n : ℕ)
  | cons (a b : S)

instance : Coe ℕ S := ⟨S.nat⟩
instance (n : Nat) : OfNat S n := ⟨n⟩

def PNat.toS (n : ℕ+) : S := (n : ℕ)
theorem PNat.toS_injective : Function.Injective PNat.toS := by
  intro; simp (config := {contextual := true}) [toS]

def PreCantor.toS : PreCantor → S
  | .zero => .cons 0 0
  | .oadd x n y => .cons 1 (.cons x.toS (.cons n.toS y.toS))

theorem PreCantor.toS_injective : Function.Injective PreCantor.toS := by
  intro x
  induction x with
  | zero => rintro (_|_) <;> simp [toS]
  | oadd x n y ihx ihy =>
    rintro (_|_)
    · simp [toS]
    simp [toS]
    intro h1 h2 h3
    cases ihx h1
    cases ihy h3
    cases PNat.toS_injective h2
    simp

[Kyle Miller]

You don't need a toS function for each type that appears inside the inductive definition, like I did for PNat here. Instead, you use choice to extract an injective function to Nat from the Countable proof.

[Kyle Miller]

Proving S is countable should be easy. You can construct a function to Nat directly, using that Nat pairing function in mathlib

[Kyle Miller]

I'd be happy to help make this Countable deriving handler :-) If you write the Countable proof for S, I'll look into the next steps.

[Violeta Hernández]

Kyle Miller said:

I'd be happy to help make this Countable deriving handler :-) If you write the Countable proof for S, I'll look into the next steps.

Easy!

inductive S : Type where
  | nat (n : ℕ)
  | cons (a b : S)

def S.toNat : S → ℕ
  | nat n => Nat.pair 0 n
  | cons a b => Nat.pair (a.toNat + 1) b.toNat

theorem S.toNat_injective : Function.Injective S.toNat
  | nat m, nat n
  | cons a b, nat n
  | nat m, cons a b => by simp [S.toNat]
  | cons a b, cons c d => by
    simp_rw [toNat, Nat.pair_eq_pair, add_left_inj, cons.injEq]
    exact fun ⟨h₁, h₂⟩ ↦ ⟨S.toNat_injective h₁, S.toNat_injective h₂⟩

instance : Countable S :=
  S.toNat_injective.countable

[Violeta Hernández]

You idea to use Nat.pair was really clever, my own idea was trying to inject S into a WType

[Chris Hughes]

Have you looked at Data.W.Basic? There's an encodableinstance there. You could prove it's isomorphic to the corresponding WTypeand use the instance.

[Violeta Hernández]

Violeta Hernández said:

I think this can be injected into a WType where the possible labels are in Option ℕ, with 0 representing zero, other natural numbers representing themselves, and none representing the oadd constructor

I did think about this, but Kyle's approach seems simpler

[Eric Wieser]

Is Kyle's approach above sensible for implementing docs#Encodable too?

[Violeta Hernández]

It should be, I think. The explicit encoding would look something like x.toS.toNat, and building the inverse should be easy as long as we can show S itself is encodable.

[Kyle Miller]

@Violeta Hernández, it is done: #18557

[Kyle Miller]

It turned out to be a easier to not go through any auxiliary types. I spent time looking at your S.toNat_injective and figured out how to generalize it for automation. If you want to see the details, there's an example expansion in a module docstring in the DeriveCountable file.

[Kyle Miller]

I tried working out the theory of how to go about making an Encodable deriving handler. It was really painful (and I failed) trying to use Nat.pair directly, and the intermediate S type was helpful.

It seems like it's a promising approach though

import Mathlib

inductive S : Type where
  | nat (n : ℕ)
  | cons (a b : S)

instance : Coe ℕ S := ⟨S.nat⟩
instance (n : Nat) : OfNat S n := ⟨n⟩

def S.encode : S → ℕ
  | nat n => Nat.pair 0 n
  | cons a b => Nat.pair (a.encode + 1) b.encode

lemma Nat.unpair_lt_2 {n : ℕ} (n1 : 1 ≤ (Nat.unpair n).1) : (Nat.unpair n).2 < n := by
  obtain ⟨⟨a, b⟩, rfl⟩ := Nat.pairEquiv.surjective n
  simp only [pairEquiv_apply, Function.uncurry_apply_pair, unpair_pair] at *
  simp [pair]
  split <;> nlinarith

def S.decode (n : ℕ) : S :=
  let p := Nat.unpair n
  if h : p.1 = 0 then
    S.nat p.2
  else
    have : p.1 ≤ n := Nat.unpair_left_le n
    have := Nat.unpair_lt (by omega : 1 ≤ n)
    have := Nat.unpair_lt_2 (by omega : 1 ≤ p.1)
    S.cons (S.decode (p.1 - 1)) (S.decode p.2)

theorem S.decode_encode (s : S) : S.decode (S.encode s) = s := by
  unfold S.decode
  dsimp only
  cases s with
  | nat n =>
    unfold S.encode
    simp
  | cons a b =>
    unfold S.encode
    simp [S.decode_encode a, S.decode_encode b]

instance : Encodable S where
  encode := S.encode
  decode := fun s => some (S.decode s)
  encodek := by simp [S.decode_encode]

-- Example:

inductive T (α : Type) where
  | a (x : α) (y : Bool) (z : T α)
  | b

def T.encode {α : Type} [Encodable α] : T α → S
  | a x y z =>
    .cons 0 (.cons (Encodable.encode x) (.cons (Encodable.encode y) (T.encode z)))
  | b => .cons 1 0

def T.decode {α : Type} [Encodable α] : S → Option (T α)
  | .cons 0 (.cons (.nat x) (.cons (.nat y) z)) =>
    match Encodable.decode x, Encodable.decode y, T.decode z with
    | some x, some y, some z => some <| T.a x y z
    | _, _, _ => none
  | .cons 1 0 => some <| T.b
  | _ => none

lemma T.decode_encode {α : Type} [Encodable α] (t : T α) : T.decode (T.encode t) = some t := by
  cases t <;> simp [T.encode, T.decode, T.decode_encode]

instance {α : Type} [Encodable α] : Encodable (T α) where
  encode t := Encodable.encode (T.encode t)
  decode n := Encodable.decode n >>= T.decode
  encodek := by simp [T.decode_encode]

[Eric Wieser]

S is FreeMagma Nat, right?

[Eric Wieser]

(though maybe that's not a helpful tool to use!)

[Kyle Miller]

Here are Encodable derived handlers too: #18564

[Kyle Miller]

It doesn't support indexed inductive types. That'll be some extra work; the issue is in the decoding function. I think what you'd do is have it use DecidableEq to do equality tests with the indices, and use those successful tests to rewrite the indices.

[Kyle Miller]

(I'm not sure how observing that binary trees of natural numbers is the same as FreeMagma Nat helps here @Eric Wieser, sorry)

[Violeta Hernández]

Nice!

[Violeta Hernández]

Doesn't this subsume the Countable handler, though?

[Violeta Hernández]

If you have e.g. Encodable a -> Encodable (List a) then you can derive Countable a -> Countable (List a) by nonconstructively building an Encodable instance, which then gives you the Countable instance you want

[Kyle Miller]

No, because this needs Encodable instances for its parameters

[Kyle Miller]

You can derive that, but it's not automatic with typeclass synthesis

[Violeta Hernández]

Yeah, that's what I mean

[Kyle Miller]

This is why it doesn't subsume it

[Violeta Hernández]

Perhaps "simplify" is the correct word then

[Kyle Miller]

The stronger reason at the moment is that the Countable handler can deal with indexed inductive types

[Violeta Hernández]

Oh, alright

[Kyle Miller]

The Countable handler is also simpler and quicker-to-elaborate

[Violeta Hernández]

Perhaps this can be left as a TODO then? or maybe not if the difference in performance is significant

[Violeta Hernández]

Hope I'm not coming off as nitpicky, this is really cool in any case

[Kyle Miller]

I don't think it's really necessary, it's not like in the math library where generalization is good, where everything can be type-checked for mathematical correctness. Meta code is only as correct as the testing we do. I feel that some of the automation in the Encoding handler for the proofs is sketchier than the Countable one.

I think making the Countable handler be in terms of the Encodable handler would make it more complicated and harder-to-maintain overall. This also frees us from needing to design it with any consideration for computability.

[Kyle Miller]

It would be neat to re-use some of the Countable handler code for a Finite handler though. The idea would be to use the fact that if you have an injection to Nat from a Finite type, the function is bounded, and then in all the Nat.pair constructions, we can deduce that the constructed function is bounded as well.

Or there's reusing the Fintype deriving handler machinery, which would work fine too, though that doesn't handle indexed inductives.

[Violeta Hernández]

Fair enough. I think these were just my math instincts kicking in :stuck_out_tongue:

[Kyle Miller]

In another direction, it might be interesting having an Infinite derive handler that creates one or more instances that would prove the type is infinite, like

structure Pair (α β : Type*) where
  fst : α
  snd : β
  deriving Infinite

-- creates
instance [Infinite α] : Infinite (Pair α β) := ...
instance [Infinite β] : Infinite (Pair α β) := ...

[Violeta Hernández]

Would be nice. I think this handler is perhaps lower priority, since it's usually not too difficult to build something like an injection from N.

[Violeta Hernández]

(in fact, many types have a preferred injection!)

[Edward van de Meent]

You'd also need assumptions about Nonempty for this example, but that does seem like an interesting idea

[Edward van de Meent]

Btw, is there a good resource for writing derive handlers? I think I'd like to get more familiar with this part of lean...

[Edward van de Meent]

also, does it make sense to adapt this to derive Primcodable instances?

[Edward van de Meent]

(because from what i can tell, this should be doable)

[Edward van de Meent]

from the looks of it, we'd need a variant of docs#Enumerable.ofLeftInjective for docs#Primcodable ...

[Kyle Miller]

@Edward van de Meent Hints:

• Most deriving handlers are basically macros. They construct command syntax using knowledge of the inductive types and then ask the command elaborator to do the rest. A minority create definitions from scratch and add them to the environment directly.
• The Deriving namespace has some functions that are convenient for certain types of deriving handlers, but don't expect them to do everything you want. You may need to copy functions into your deriving handler and modify them to suit your needs. (The Countable deriving handler had to do this with the instance-creation function for example.)
• There's no documentation about any of this really. You can try to find a pre-existing deriving handler that is similar to what you want to do. You'll need to read some core source code in this Deriving namespace and try to figure out what it does and what it's for.
• Don't try writing a handler from scratch, start with a related one. With Countable, I copy/pasted relevant bits from the DecidableEq and Repr handlers, probably some others too, and then hammered it into shape. For this one, I needed to generate additional names for auxiliary declarations and thread these around since the Deriving.Context assumes you only need a single kind of aux declaration. (It would probably be cleaner to abandon the Deriving namespace at this point and make something custom for Countable!)

[Kim Morrison]

Kyle Miller said:

In another direction, it might be interesting having an Infinite derive handler that creates one or more instances that would prove the type is infinite, like

structure Pair (α β : Type*) where
  fst : α
  snd : β
  deriving Infinite

-- creates
instance [Infinite α] : Infinite (Pair α β) := ...
instance [Infinite β] : Infinite (Pair α β) := ...

Just noting the existing PR #3610 from @Timothy Gu.