Proving a simple Denumerable instance

Stream: new members

[Graham Leach-Krouse]

Is there a preferred/idiomatic way to prove denumerability for a simple inductive type, like:

inductive Form : Type
  | atom : Nat → Form
  | neg  : Form → Form
  | and  : Form → Form → Form
  | or   : Form → Form → Form
  | impl : Form → Form → Form

for example?

What I'm considering is proving countability and infinity, then using Encodable.ofCountable and Denumerable.ofEncodableOfInfinite. This feels sort of indirect, and ends up requiring a not of noncomputable annotations. But the only alternative that's leaping out at me right now (to build decode : Nat->Form) is to futz around with Nat.mkpair and Nat.evenOddRec or something, which seems likely to be a mess.

[Kevin Buzzard]

It would be cool if @[derive Denumerable] could be made to work. I guess you could build an explicit injection i into Nat by sending atom n to 2^(n+1), neg f to 3^(1 + i f), and f g to 5^(1 + b (i f) (i g)) where b is some fixed bijection Nat^2->Nat etc; injectivity should hopefully be a simple induction (modulo the necessary arithmetic lemmas)

[Eric Wieser]

You could also use docs#nat.div_mod_equiv to split the type into the 5 constructors, and then use mkpair on the binary constructors

[Eric Wieser]

Do we have an n-ary version of mkpair?

[Eric Wieser]

I guess you can just iterate it

[Kyle Miller]

It seems like you could get a lot done if you have that the following type is Encodable:

inductive ConsExp : Type
  | nat : Nat → ConsExp
  | cons  : Nat → List ConsExp → ConsExp

It's easy to create an injective map to this from Form:

inductive Form : Type
  | atom : Nat → Form
  | neg  : Form → Form
  | and  : Form → Form → Form
  | or   : Form → Form → Form
  | impl : Form → Form → Form

def Form.toConsExp : Form → ConsExp
  | atom n => .cons 0 [.nat n]
  | neg f => .cons 1 [f.toConsExp]
  | and f g => .cons 2 [f.toConsExp, g.toConsExp]
  | or f g => .cons 3 [f.toConsExp, g.toConsExp]
  | impl f g => .cons 4 [f.toConsExp, g.toConsExp]

theorem Form.toConsExp_injective : Function.Injective Form.toConsExp := by
  intros f1 f2
  induction f1 generalizing f2 <;> cases f2 <;> simp! <;> aesop

[Kyle Miller]

It's also easy to construct a left inverse:

/-- Interpret a `ConsExp` as a `Form`, returning `atom 0` if the input is malformed. -/
def ConsExp.toForm : ConsExp → Form
  | .cons 0 [.nat n] => .atom n
  | .cons 1 [f] => .neg f.toForm
  | .cons 2 [f, g] => .and f.toForm g.toForm
  | .cons 3 [f, g] => .or f.toForm g.toForm
  | .cons 4 [f, g] => .impl f.toForm g.toForm
  | _ => .atom 0

theorem toForm_toConsExp_eq (f : Form) : f.toConsExp.toForm = f := by
  induction f <;> simp! <;> unfold ConsExp.toForm <;> simp [*]

[Graham Leach-Krouse]

Thanks all! I went the countability/infinity route this morning. The injection goes first into a sum of products of Nat, using the Encodable instance for that to recur:

abbrev tupleEquiv := Nat⊕ Nat⊕ (Nat × Nat)⊕ (Nat × Nat)⊕ (Nat×Nat)

def Form.toSumEncoding : Form → Nat⊕ Nat⊕ (Nat × Nat)⊕ (Nat × Nat)⊕ (Nat×Nat)
  | #n => Sum.inl n
  | ~f => Sum.inr $ Sum.inl (Encodable.encode $ toSumEncoding f)
  | f & g => Sum.inr $ Sum.inr $ Sum.inl ⟨Encodable.encode $ toSumEncoding f, Encodable.encode $ toSumEncoding g⟩
  | f ¦ g => Sum.inr $ Sum.inr $ Sum.inr $ Sum.inl ⟨Encodable.encode $ toSumEncoding f, Encodable.encode $ toSumEncoding g⟩
  | Form.impl f g => Sum.inr $ Sum.inr $ Sum.inr $ Sum.inr ⟨Encodable.encode $ toSumEncoding f, Encodable.encode $ toSumEncoding g⟩

Derivable denumberance instances would be cool. But short of that, the ConsExp idea or something similar seems pretty elegant. When I clean this up, I'll see if I can work something like that out.

[Kyle Miller]

@Graham Leach-Krouse As an exercise for myself, I created an Encodable instance for a variant of ConsExpr and used it to create one for Form:

code

import Mathlib.Logic.Denumerable

inductive ConsExp : Type
  | nat : Nat → ConsExp
  | cons : ConsExp → ConsExp → ConsExp

def ConsExp.encode : ConsExp → Nat
  | nat n => 2 * n
  | cons f g => 2 * Nat.mkpair f.encode g.encode + 1

def ConsExp.decode (n : ℕ) : ConsExp :=
  match hn : Nat.boddDiv2 n with
  | (false, m) => nat m
  | (true, m) =>
    match hm : Nat.unpair m with
    | (f, g) =>
      -- Some proofs to show termination:
      have hn' : 1 ≤ n := by
        cases n
        · simp at hn
        · simp [Nat.succ_eq_add_one]
      have : m < n := by
        have := congr_arg Prod.snd hn
        simp at this
        cases this
        apply Nat.binaryRec_decreasing
        rwa [Nat.one_le_iff_ne_zero] at hn'
      have : f < n := by
        apply Nat.lt_of_le_of_lt _ this
        have := congr_arg Prod.fst hm
        simp at this
        cases this
        cases m
        · simp
        next m =>
          apply (Nat.unpair_lt _).le
          simp [Nat.succ_eq_add_one]
      have : g < n := by
        have := congr_arg Prod.snd hm
        simp at this
        cases this
        have := Nat.unpair_right_le m
        apply Nat.lt_of_le_of_lt this
        assumption
      -- With those out of the way:
      cons (decode f) (decode g)
termination_by _ => n

theorem ConsExp.decode_encode (c : ConsExp) : ConsExp.decode c.encode = c := by
  induction c
  · rw [encode, decode]
    split
    next h =>
      simp [Nat.div2_val] at h
      simp [*]
    next h => simp at h
  next hf hg =>
    rw [encode, decode]
    split
    next h => simp at h
    next h =>
      simp [Nat.div2_val] at h
      cases h
      simp [*]

instance : Encodable ConsExp where
  encode := ConsExp.encode
  decode := fun v => some (ConsExp.decode v)
  encodek := fun a => by simp [ConsExp.decode_encode]

inductive Form : Type
  | atom : Nat → Form
  | neg  : Form → Form
  | and  : Form → Form → Form
  | or   : Form → Form → Form
  | impl : Form → Form → Form
  deriving Repr

def Form.toConsExp : Form → ConsExp
  | atom n => .cons (.nat 0) (.nat n)
  | neg f => .cons (.nat 1) f.toConsExp
  | and f g => .cons (.nat 2) (.cons f.toConsExp g.toConsExp)
  | or f g => .cons (.nat 3) (.cons f.toConsExp g.toConsExp)
  | impl f g => .cons (.nat 4) (.cons f.toConsExp g.toConsExp)

/-- Interpret a `ConsExp` as a `Form`, returning `atom 0` if the input is malformed. -/
def ConsExp.toForm : ConsExp → Form
  | .cons (.nat 0) (.nat n) => .atom n
  | .cons (.nat 1) f => .neg f.toForm
  | .cons (.nat 2) (.cons f g) => .and f.toForm g.toForm
  | .cons (.nat 3) (.cons f g) => .or f.toForm g.toForm
  | .cons (.nat 4) (.cons f g) => .impl f.toForm g.toForm
  | _ => .atom 0

theorem toForm_toConsExp_eq (f : Form) : f.toConsExp.toForm = f := by
  induction f <;> simp! [*]

instance : Encodable Form where
  encode f := Encodable.encode f.toConsExp
  decode n := (Encodable.decode n).map ConsExp.toForm
  encodek := by
    intro f
    simp [toForm_toConsExp_eq]

[Kyle Miller]

The intermediate type is the simpler

inductive ConsExp : Type
  | nat : Nat → ConsExp
  | cons : ConsExp → ConsExp → ConsExp

[Eric Wieser]

I think the fintype derive handler alread builds this type of equivalence for you

[Eric Wieser]

So we should be able to extend it to encodable quite easily

[Kevin Buzzard]

Is it possible to @derive this?

[Graham Leach-Krouse]

Trivial tweak: here's a revision using Option.none rather than .atom 0 for the junk case:

def ConsExp.toForm : ConsExp → Option Form
  | .cons (.nat 0) (.nat n) => .some (.atom n)
  | .cons (.nat 1) f => .neg <$> f.toForm
  | .cons (.nat 2) (.cons f g) => .and <$> f.toForm <*> g.toForm
  | .cons (.nat 3) (.cons f g) => .or <$> f.toForm <*> g.toForm
  | .cons (.nat 4) (.cons f g) => .impl <$> f.toForm <*> g.toForm
  | _ => .none

theorem toForm_toConsExp_eq (f : Form) : f.toConsExp.toForm = some f := by
  induction f <;> simp! [*]

instance : Encodable Form where
  encode f := Encodable.encode f.toConsExp
  decode n := Option.bind (Encodable.decode n) ConsExp.toForm
  encodek := by
    intro f
    simp [toForm_toConsExp_eq]