Bundling a decidability instance with a structure/object?

Stream: new members

[Jake Levinson]

I've been working on something the last few months and running into two problems that might be interrelated. I've tried to distill to a #mwe but haven't succeeded -- sorry, this thread doesn't have a #mwe (but maybe with help I can generate one). Maybe I can get some help anyway.

(1) I have defined various structures and Lean sometimes asks for decidability instances. Mostly I have gone the route of "add the requested instance as an assumption [decidable ...] or [decidable_pred ...] wherever requested".

The first problem is that this has led to a proliferation of assumptions -- now (towards the later stages of the construction) I think I am up to six running decidability assumptions. Maybe some of these could be deduced from each other, but I've just been blindly adding whatever Lean asks for. They are things pretty similar to the following:

structure myobj :=
  (f : ℕ → Prop)
  (g : ℕ → ℕ)

variables
  [∀ (X : myobj) (n : ℕ), decidable (X.f n)]
  [∀ (X : myobj) m, decidable (∀ n, X.f n → X.g n < m)]
  [∀ (X : myobj) m, decidable_pred (λ i, X.f i → m < X.g i)]
  [∀ (X : myobj) m, decidable_pred (λ i, X.f 0 → m < X.g i)]
  -- etc, 2-3 more variations like these

Question 1. Is there a simple "smallest possible" decidability assumption from which to deduce the examples listed above? The parameters are mostly about inequalities involving functions of the form f : ℕ → Prop and g : ℕ → ℕ above. Actually technically f : ℕ → ℕ → Prop and g : ℕ → ℕ → ℕ.
Question 2. Should I bundle such decidability assumption(s) into myobj? The thing is, I definitely want two otherwise-equal objects with different decidability instances to still be equal.

Anyway there is a second more serious problem.

(2) The structures I'm defining are similar to fin (n : ℕ) in that they depend on auxiliary parameters.

structure myobj2 (X : myobj) := sorry
structure myobj3 {X : myobj} (Y : myobj2 X) := sorry

I have been (to the best of my ability) intentional about what to bundle and what to leave out, since it's relevant to the construction to have various objects from the same underlying parameters. I tried bundling everything at one point and it seemed to make things much more complicated -- not least because there were no longer shared decidability instances.

Well, I am encountering more and more difficult motive is not type correct errors.

• Sometimes this is because two parameters are only propositionally-equal (like 3+3 and 6 for fin n, only instead of nats as parameters it's myobj or myobj2).

I can resolve this mostly by using copy patterns (https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/dependent.20structures). Though, I also have to re-assume, or else transfer, decidability instances on the copied object. Sometimes this seems to cause a diamond.

• The more serious problem is that even when things are definitionally equal, sometimes I can't seem to rewrite them without getting a motive is not type correct error. The main thing will be a definition like

def f x := if (p x) then (f1 x) else (f2 x)

and then later, I will get motive is not type correct errors when trying to rewrite f x to whichever of f1 x or f2 x it is. Sometimes simp_rw fixes it but not always.

In some cases I can't even rewrite/unfold f x to ite (p x) (f1 x) (f2 x)!
(Or, it might be something to do with recursion -- my actual f is defined using well-founded recursion...)

I think this is because, in context, there might be other objects that depend on "f x" that might need to be rewritten simultaneously (e.g. I have X : my_complicated_object (f x). Or, it might be something about not being able to rw on the decidability assumptions?

Question 3. How do I diagnose / understand a motive is not type correct error? I think this is sometimes about rewriting under binders, and simp_rw can fix it. But the error messages I get are very complicated and I am not able to even identify where the error is generated.

[Patrick Johnson]

You may want to add this to your file:

noncomputable theory
open_locale classical

In another thread, Keving suggested you to remove open_locale classical and use explicit decidability instances to avoid diamonds. I think it makes sense only if you have a small number of decidability instances and you want your decidability algorithms to be computable. But in your case using convert instead of exact in some places is easier than having so many decidability instances flying around.

[Kyle Miller]

Given the examples, it looks like [∀ (X : myobj) (n : ℕ), decidable (X.f n)] and [∀ (X : myobj) m, decidable (∀ n, X.f n → X.g n < m)] are the only ones you need. Numbers 3 and 4 are consequences of the first one.

[Kyle Miller]

Another thing you might do is, rather than have f : ℕ → Prop, use f : ℕ → bool, which is a way to bake-in the decidability of the the predicate. It's hard to say whether this is appropriate given just the example though.

For ∀ n, X.f n → X.g n < m, what does this being true or false represent?

[Jake Levinson]

Patrick Johnson said:

You may want to add this to your file:

noncomputable theory
open_locale classical

In another thread, Kevin suggested you to remove open_locale classical and use explicit decidability instances to avoid diamonds. I think it makes sense only if you have a small number of decidability instances and you want your decidability algorithms to be computable. But in your case using convert instead of exact in some places is easier than having so many decidability instances flying around.

It does seem worth trying, yes. I just wasn't sure if the statements I listed actually are decidable already or something -- like I think a < b for natural numbers might be decidable (?), so maybe something like a < g m is too?

[Jake Levinson]

Kyle Miller said:

Given the examples, it looks like [∀ (X : myobj) (n : ℕ), decidable (X.f n)] and [∀ (X : myobj) m, decidable (∀ n, X.f n → X.g n < m)] are the only ones you need. Numbers 3 and 4 are consequences of the first one.

Hmm. Should Lean be able to fill in 3 and 4 automatically, given the first one? This might well be a place where I blindly copied a request from the infoview (for the more complicated statement 3 or 4), then later on added in statement 1 for something else simpler.

[Kyle Miller]

Yes, that is a decidable proposition already given any pair of natural numbers m and n.

variables (m n : ℕ)

#check (infer_instance : decidable (m < n)) -- doesn't throw an error

[Kyle Miller]

Jake Levinson said:

Should Lean be able to fill in 3 and 4 automatically, given the first one?

Yes, that's what I mean.

variables (p q : Prop) [decidable q]
--variables [decidable p] -- fails if this line is commented out

#check (infer_instance : decidable (p → q))

[Jake Levinson]

Kyle Miller said:

Another thing you might do is, rather than have f : ℕ → Prop, use f : ℕ → bool, which is a way to bake-in the decidability of the the predicate. It's hard to say whether this is appropriate given just the example though.

Oh I see. Interesting, I could try it. Separately, maybe I should just make a separate thread about what I'm trying to do. I'd hoped to avoid posting about it until it was done...

For ∀ n, X.f n → X.g n < m, what does this being true or false represent?

Just something like "X.g is (or isn't) bounded by m in the region where X.f is true".