Proper way to implement conditional decidability

Stream: lean4

[Mario Weitzer]

Let's say I have a type α for which there is a predicate isFinite which is decidable and another predicate p which is decidable if isFinite holds. What is the best way to implement this such that type class inference works without much overhead?

[Edward van de Meent]

i don't know about overhead, but that sounds to me like you want an assumption [Decidable (IsFinite α)] to your instance?

[Floris van Doorn]

Do you mean something like this?

variable {α : Type}
def isFinite : α → Prop := sorry

instance : DecidablePred (isFinite : α → Prop) := sorry

def anotherPred : α → Prop := sorry

instance [DecidablePred (isFinite : α → Prop)] : DecidablePred (anotherPred : α → Prop) := sorry

If not, it is useful if you provide a #mwe with what you want.

[Mario Weitzer]

Yes, I think that's exactly what I am looking for. Thanks to both of you!

[Eric Wieser]

That says that anotherPred is globally decidable if isFinite is globally decidable, not that one is decidable only where the other is

[Mario Weitzer]

No wait, sorry, that's not what I want. I want to say that anotherPred is only decidable for those elements of α for which isFinite is true.

[Aaron Liu]

How is typeclass supposed to know at compile-time that your element of α is finite?

[Eric Wieser]

I think there are hacks to make typeclass search run decide

[Mario Weitzer]

Here is a toy example:

import Mathlib.Data.ENat.Basic

structure Sequence.{u} (α : Type u) where
  length : ℕ∞
  entries : ℕ → α

----------------------------------------------------------------------------------------------------

universe u

variable {α : Type u}

namespace Sequence

def isFinite (S : Sequence α) : Prop :=
  S.length ≠ ⊤

class IsFinite (S : Sequence α) : Prop where
  out : isFinite S

instance isFinite_DecPred : DecidablePred (@isFinite α) :=
  λ S =>
  match decEq S.length ⊤ with
  | isTrue hi  => isFalse (λ hni => hni hi)
  | isFalse hni => isTrue (λ hi => hni hi)

def S : Sequence ℕ := ⟨5, λ i => i⟩
def T : Sequence ℕ := ⟨⊤, λ i => i⟩

example : isFinite S := by decide
example : ¬(isFinite T) := by decide

def contains (a : α) (S : Sequence α) : Prop :=
  ∃ i, i < S.length → S.entries i.toNat = a

--What I want:
instance contains_DecPred (a : α) : DecidablePred (@contains α a) "if isFinite S" :=
  sorry

--The clumsy solution I found so far:
instance contains_DecPred' (a : α) :
  DecidablePred (λ S : { S : Sequence α | isFinite S } => @contains α a S) := by
  sorry

What is considered best practice in such a situation?

[Robin Arnez]

just

instance (a : α) (S : Sequence α) [IsFinite S] : Decidable (contains a S) :=

that's basically how DecidablePred is defined

[Mario Weitzer]

Yes, I added this instance in my case but in some situations (when using decide for example) Lean complains that "failed to synthesize Decidable (contains a S)" even if I explicitly add a proof of IsFinite S to the context (which I shouldn't even need since IsFinite is a decidable predicate). In other situations Lean complains that contains is not a decidable predicate. The solution I found so far is

instance (a : α) : DecidablePred (λ S : Sequence α => IsFinite S → contains a S) := sorry

lemma IsFinite_imp {S : Sequence α} {p : Sequence α → Prop} (hf : IsFinite S) (hp : IsFinite S → p S) :
  p S := hp hf

lemma not_IsFinite_imp {S : Sequence α} {p : Sequence α → Prop} (hp : ¬(IsFinite S → p S)) :
  ¬p S := λ hps => hp (λ _ => hps)

def x := some finite sequence which contains some a
def y := some finite sequence which doesn't contain some a

example : contains a x := @IsFinite_imp _ _ _ (by decide) (by decide)

example : ¬contains a y := not_IsFinite_imp (by decide)

interestingly

example : contains a x := IsFinite_imp (by decide) (by decide)

doesn't work even though I don't give any additional information in

example : contains a x := @IsFinite_imp _ _ _ (by decide) (by decide)

[Robin Arnez]

Mario Weitzer schrieb:

which I shouldn't even need since IsFinite is a decidable predicate

Lean won't do any computational effort to figure out whether it could be a finite sequence when you synthezize IsFinite and in particular, defs are opaque to instance synthesis. So what you'd need is an instance and to declare your sequences as abbrevs:

class EqInst (a : α) (b : outParam α) where
  out : a = b

instance : EqInst a a := ⟨rfl⟩

instance (y : Nat) [h : EqInst x.1 (y : ENat)] : IsFinite x := by
  rcases x with ⟨l, _⟩
  rcases h with ⟨rfl⟩
  constructor
  simp [isFinite]

def contains (a : α) (S : Sequence α) : Prop :=
  ∃ i, i < S.length ∧ S.entries i.toNat = a

--What I want:
instance [DecidableEq α] (a : α) (S : Sequence α) [h : IsFinite S] : Decidable (contains a S) :=
  decidable_of_iff (∃ i, i < S.length.toNat ∧ S.entries i = a) sorry

abbrev x : Sequence Nat := { length := 3, entries | 0 => 25 | 1 => 17 | _ + 2 => 99 }
abbrev y : Sequence Nat := { length := 5, entries | 0 => 19 | 1 => 24 | 2 => 54 | 3 => 9 | _ + 4 => 88 }

example : contains 17 x := by decide
example : ¬contains 17 y := by decide

(something similar to EqInst might be in mathlib, not sure)

[Robin Arnez]

An alternative would be to use Classical.propDecidable in the branches where it isn't possible otherwise:

noncomputable instance contains_DecPred [DecidableEq α] (a : α) (S : Sequence α) : Decidable (contains a S) :=
  if h : S.length = ⊤ then
    Classical.propDecidable _
  else
    decidable_of_iff (∃ i, i < S.length.toNat ∧ S.entries i = a) sorry

(this solution actually also works without abbrev)

[Mario Weitzer]

These are great solutions, thank you!