Decidability of inductive propositions.

Stream: lean4

[Wrenna Robson]

I think this is a MWE: how do I prove the decidability of isRoot in the following?

inductive PSharedStack (β : Type u) : Type u
  | sngl : β → PSharedStack β
  | bit0 : PSharedStack β → PSharedStack β
  | bit1 : β → PSharedStack β → PSharedStack β
deriving DecidableEq

inductive isRoot : PSharedStack β → Prop
  | protected sngl : (a : β) → isRoot (sngl a)
  | protected bit0 : (p : PSharedStack β) → p.isRoot → isRoot (bit0 p)

instance : Decidable (p.isRoot) := match p with
  | sngl _ => isTrue isRoot_sngl
  | bit0 _ => sorry
  | bit1 _ _ => isFalse not_isRoot_bit1

[Wrenna Robson]

I have these:

@[simp] theorem isRoot_sngl : (sngl a).isRoot := by constructor

@[simp] theorem not_isRoot_bit1 : ¬ (bit1 a p).isRoot := fun h => by contradiction

@[simp] theorem isRoot_bit0_iff : (bit0 p).isRoot ↔ p.isRoot :=
  ⟨fun h => by cases h ; assumption, fun h => by constructor ; assumption⟩

[Wrenna Robson]

What I am essentially doing is I want to recursively construct the decidability - we have Decidable p.bit0.isRoot if and only if Decidable p.isRoot, and so I want to essentially go "OK, proceed by induction", but that doesn't seem to work.

[Kim Morrison]

Often a good approach is to define a Bool valued function.

[Kim Morrison]

Then write a proof that the function returns true iff the inductive predicate holds.

[Kim Morrison]

Then use decidable_of_iff.

[Wrenna Robson]

Right, actually that is what I started with (as in, isRoot was bool-valued), but in some ways it seemed less neat.

[Kim Morrison]

I'm suggesting you have both.

[Wrenna Robson]

Right. Got it. What's the naming convention?

[Wrenna Robson]

i.e. if the Prop is isRoot, what would we call the Bool? bIsRoot?

[Wrenna Robson]

def bIsRoot : PSharedStack β → Bool
  | sngl _ => true
  | bit0 p => p.bIsRoot
  | bit1 _ _ => false

@[simp] theorem bIsRoot_sngl : (sngl a).bIsRoot = true := rfl
@[simp] theorem bIsRoot_bit0 : (bit0 p).bIsRoot = p.bIsRoot := rfl
@[simp] theorem bIsRoot_bit1 : (bit1 a p).bIsRoot = false := rfl

@[simp] theorem bIsRoot_eq_true_iff : p.bIsRoot ↔ p.isRoot := by
  induction p
  · exact iff_of_true bIsRoot_sngl isRoot_sngl
  · rw [bIsRoot_bit0, isRoot_bit0_iff]
    assumption
  · exact iff_of_false (Bool.not_eq_true _ ▸ bIsRoot_bit1) not_isRoot_bit1

instance : Decidable (p.isRoot) := decidable_of_bool _ bIsRoot_eq_true_iff

[Wrenna Robson]

So this sort of thing?

[Kyle Miller]

Looks good.

An idea we've been kicking around is to redefine Decidable as

class Decidable (p : Prop) where
  decide : Bool
  cond_decide : cond decide p (Not p)

Then defining a bool-valued function and proving it represents the truth of the proposition will look like the natural thing to do.

[Wrenna Robson]

Incidentally I actually avoided this because:

theorem isRoot_iff_count_eq_two_pow_lg2 : p.isRoot ↔ p.count = 2^p.lg2 := by
  induction p with | sngl a => _ | bit0 p IH => _ | bit1 a p IH => _
  · simp_rw [isRoot_sngl, count_sngl, lg2_sngl, pow_zero]
  · simp_rw [isRoot_bit0_iff, IH, count_bit0, lg2_bit0, pow_succ', mul_eq_mul_left_iff,
      zero_lt_two.ne', or_false]
  · simp_rw [not_isRoot_bit1, count_bit1, lg2_bit1, false_iff, pow_succ']
    exact (Nat.two_mul_ne_two_mul_add_one).symm

instance : Decidable (p.isRoot) :=
  decidable_of_iff _ isRoot_iff_count_eq_two_pow_lg2.symm

[Wrenna Robson]

i.e. I have some other quantities that are nats and which characterise isRoot. so I can actually just use decidability of nat equality.

[Wrenna Robson]

That is a nice idea though.

[Wrenna Robson]

(Of course this might be less efficient... my way, I mean. There is a distinction between "there is a decision procedure for this prop" and "here is a specific, efficient decision procedure for the prop, which is the one I want Lean to perform when evaluating".)

[Kyle Miller]

What you're doing is the same idea. You're indirectly using the boolean-value function "evaluate p.count == 2^p.lg2"

[Wrenna Robson]

Oh, certainly.

[Wrenna Robson]

And that may not be the best way, actually!

[Wrenna Robson]

I was just musing that sometimes what is most convenient from a "defining and proving things quickly" standpoint is not what is most performant.