bad Decidable instances

Stream: mathlib4

[Kim Morrison]

Consider:

import Mathlib

set_option autoImplicit true

structure Vec (n : Nat) (α : Type _) where
  toArray : Array α
  size : toArray.size = n

namespace Vec

instance : GetElem (Vec n α) Nat α (fun _ i => i < n) where
  getElem v i h := v.1[i]'(Nat.lt_of_lt_of_eq h v.2.symm)

@[simp] theorem getElem_mk (data : Array α) (size : data.size = n) (i : Nat) (h : i < n) :
    (Vec.mk data size)[i] = data[i] := rfl

@[ext] theorem ext {v w : Vec n α} (h : ∀ i : Fin n, v[i] = w[i]) : v = w := by
  cases v; cases w; congr
  ext i
  · simp_all
  · simp at h
    specialize h ⟨i, by omega⟩
    simpa using h

def pop (v : Vec (n + 1) α) : Vec n α :=
  ⟨v.toArray.pop, by simp [v.size]⟩

end Vec

def Equiv.vecEquivFin (n : Nat) (α : Type _) : Vec n α ≃ (Fin n → α) where
  toFun v i := v[i]
  invFun f := ⟨.ofFn f, by simp⟩
  left_inv v := by ext; simp
  right_inv f := by ext; simp

instance [Fintype α] : Fintype (Vec n α) :=
  Fintype.ofEquiv (Fin n → α) (Equiv.vecEquivFin n α).symm

inductive Gate : Nat → Type
| const : Bool → Gate 0
| if : ∀ {n}, Gate n → Gate n → Gate (n + 1)

namespace Gate

def and : Gate 2 := .if (.if (.const true) (.const false)) (.if (.const false) (.const false))

def eval (g : Gate n) (v : Vec n Bool) : Bool :=
  match g, v with
  | .const b, _ => b
  | .if g₁ g₂, v => if v.1.back then eval g₁ v.pop else eval g₂ v.pop

example : ∀ v, and.eval v = (v[0] && v[1]) := by decide

end Gate

which fails with:

tactic 'decide' failed for proposition
  ∀ (v : Vec 2 Bool), and.eval v = (v[0] && v[1])
since its 'Decidable' instance
  Fintype.decidableForallFintype
did not reduce to 'isTrue' or 'isFalse'.

After unfolding the instances 'decidable_of_decidable_of_iff', 'decidable_of_iff', 'instDecidableEqBool', 'Bool.decEq', 'Finset.decidableDforallFinset', 'Fintype.decidableForallFintype', 'List.decidableBAll', 'Multiset.decidableDforallMultiset', 'Multiset.decidableForallMultiset', 'Nat.decLe' and 'Nat.decLt', reduction got stuck at the 'Decidable' instance
  match
    and.eval
      ↑⟨{ toFun := ⇑(Equiv.vecEquivFin 2 Bool).symm, inj' := ⋯ }
            ({ toFun := fun f a ↦ f a ⋯, inj' := ⋯ }
              (Multiset.Pi.cons ⟦List.pmap Fin.mk [1] ⋯⟧ ⟨0, ⋯⟩ true
                (Multiset.Pi.cons ⟦List.pmap Fin.mk [] ⋯⟧ ⟨1, ⋯⟩ true (Multiset.Pi.empty fun a ↦ Bool)))),
          ⋯⟩,
    (↑⟨{ toFun := ⇑(Equiv.vecEquivFin 2 Bool).symm, inj' := ⋯ }
              ({ toFun := fun f a ↦ f a ⋯, inj' := ⋯ }
                (Multiset.Pi.cons ⟦List.pmap Fin.mk [1] ⋯⟧ ⟨0, ⋯⟩ true
                  (Multiset.Pi.cons ⟦List.pmap Fin.mk [] ⋯⟧ ⟨1, ⋯⟩ true (Multiset.Pi.empty fun a ↦ Bool)))),
            ⋯⟩)[0] &&
      (↑⟨{ toFun := ⇑(Equiv.vecEquivFin 2 Bool).symm, inj' := ⋯ }
              ({ toFun := fun f a ↦ f a ⋯, inj' := ⋯ }
                (Multiset.Pi.cons ⟦List.pmap Fin.mk [1] ⋯⟧ ⟨0, ⋯⟩ true
                  (Multiset.Pi.cons ⟦List.pmap Fin.mk [] ⋯⟧ ⟨1, ⋯⟩ true (Multiset.Pi.empty fun a ↦ Bool)))),
            ⋯⟩)[1] with
  | false, false => isTrue ⋯
  | false, true => isFalse ⋯
  | true, false => isFalse ⋯
  | true, true => isTrue ⋯

Would anyone be interested in finding the bad instances? If they can't be fixed, they should simply be removed --- there is no point providing Decidable instances that don't reduce.

[Mario Carneiro]

Kim Morrison said:

structure Vec (n : Nat) (α : Type _) where
  toArray : Array α
  size : toArray.size = n

we shouldn't need to copy paste this anymore since Vector landed in batteries (unless you have reason to believe that the implementation of Vec is implicated in this bug)

[Eric Wieser]

Kim Morrison said:

there is no point providing Decidable instances that don't reduce.

I don't agree with this claim; a non-reducing decidable instance still works with #eval.

[Eric Wieser]

But indeed it's best to make them reduce

[Eric Wieser]

I suspect the problem here is that the Fintype instance doesn't reduce

[Kim Morrison]

Mario Carneiro said:

we shouldn't need to copy paste this anymore since Vector landed in batteries (unless you have reason to believe that the implementation of Vec is implicated in this bug)

I keep forgetting this. In any case many basic simp lemmas seem to be missing for Vector.

[Kim Morrison]

The problem remains with Vector, but it is indeed shorter:

[Kim Morrison]

import Mathlib

set_option autoImplicit true

namespace Batteries

namespace Vector

@[simp] theorem getElem_mk (data : Array α) (size : data.size = n) (i : Nat) (h : i < n) :
    (Vector.mk data size)[i] = data[i] := rfl

end Vector

end Batteries

open Batteries (Vector)

def Equiv.vecEquivFin (α : Type _) (n : Nat) : Vector α n ≃ (Fin n → α) where
  toFun v i := v[i]
  invFun f := ⟨.ofFn f, by simp⟩
  left_inv v := by ext; simp
  right_inv f := by ext; simp

inductive Gate : Nat → Type
| const : Bool → Gate 0
| if : ∀ {n}, Gate n → Gate n → Gate (n + 1)

namespace Gate

def and : Gate 2 := .if (.if (.const true) (.const false)) (.if (.const false) (.const false))

def eval (g : Gate n) (v : Vector Bool n) : Bool :=
  match g, v with
  | .const b, _ => b
  | .if g₁ g₂, v => if v.1.back then eval g₁ v.pop else eval g₂ v.pop

def eval' (g : Gate n) (v : Fin n → Bool) : Bool :=
  match g, v with
  | .const b, _ => b
  | .if g₁ g₂, v => if v 0 then eval' g₁ (v ∘ Fin.succ) else eval' g₂ (v ∘ Fin.succ)

example : ∀ f : Fin 2 → Bool, and.eval' f = (f 0 && f 1) := by decide -- works
example : ∀ f : Fin 2 → Bool, and.eval ((Equiv.vecEquivFin Bool 2).symm f) = (f 0 && f 1) := by decide -- fails
example : ∀ v, and.eval v = (v[0] && v[1]) := by decide -- fails

end Gate

[Eric Wieser]

Here's a shorter repro:

import Mathlib

namespace Batteries.Vector

@[simp] theorem getElem_mk {α} (data : Array α) (size : data.size = n) (i : Nat) (h : i < n) :
    (Vector.mk data size)[i] = data[i] := rfl

end Batteries.Vector

open Batteries (Vector)

example : (⟨.ofFn ![1, 2], by simp⟩ : Vector ℕ 2)[0] = 1 := by decide

[Eric Wieser]

The only decidable instance here is instDecidableEqNat, so I claim the title of this thread is wrong :)

[Eric Wieser]

A similar issue is

example : Array.ofFn ![1, 2] = #[1, 2] := by decide

[Eric Wieser]

That one is caused by Array.isEqvAux being irreducible due to use of well-founded recursion

[Kim Morrison]

Excellent, thank you for the diagnosis, @Eric Wieser. This is super useful and I will try to fix this (or merge a fix!) asap next week.

[Alex Meiburg]

I got another bad decidable instance:

import Mathlib

example : (1/2:ℚ).num = (1/3:ℚ).num := by
  decide

gives

1 goal
⊢ (1 / 2).num = (1 / 3).num
Messages (1)
mathlib-demo.lean:4:2

tactic 'decide' failed for proposition
  (1 / 2).num = (1 / 3).num
since its 'Decidable' instance
  (1 / 2).num.instDecidableEq (1 / 3).num
did not reduce to 'isTrue' or 'isFalse'.

After unfolding the instances 'Int.decEq' and 'Int.instDecidableEq', reduction got stuck at the 'Decidable' instance
  match (1 / 2).num, (1 / 3).num with
  | Int.ofNat a, Int.ofNat b =>
    match decEq a b with
    | isTrue h => isTrue ⋯
    | isFalse h => isFalse ⋯
  | Int.ofNat a, Int.negSucc a_1 => isFalse ⋯
  | Int.negSucc a, Int.ofNat a_1 => isFalse ⋯
  | Int.negSucc a, Int.negSucc b =>
    match decEq a b with
    | isTrue h => isTrue ⋯
    | isFalse h => isFalse ⋯

All Messages (2)

Any ideas what's going on? I can't make much of this match issue

[Eric Wieser]

This fails because / is irreducible

[Eric Wieser]

So once again, this is not a bad decidable instance, but a correct decidable instance applied to a bad argument

[Alex Meiburg]

What's the 'correct' way to simplify/close such a goal? And -- maybe more importantly -- if I have a much larger more complicated goal, and I want to close it with decide? If I have a large expression that ultimately reduces to deciding the equality of two rational numbers, I expect decide to be able to do that.

[Eric Wieser]

decide can only decide the equality of rational numbers which ultimately reduce to a constructor application

[Eric Wieser]

norm_num is the correct tool here

[Eric Wieser]

Alternatively, the fact that / is irreducible is a bug

[Mario Carneiro]

well, the reason it is irreducible is because it unfolds to something terrible

[Mario Carneiro]

we really need some kind of @[unfold_on_closed_term] attribute which allows decide to see through it without letting x / y be unfolded by unification

[Alex Meiburg]

So I tried norm_num earlier but it's pain because there is a _very long_ list of simplification facts I need to feed it, and it's much slower than decide, and if I'm not careful I end up loops -- I often need four or five applications of norm_num where I turn certain simp lemmas off and on again. :(

[Eric Wieser]

What's your goal state?

[Alex Meiburg]

A pretty long formula that involves e.g. bernoulli numbers, fibonacci numbers, and several other functions that I need to evaluate. Here's another one I don't understand why it fails:

example : IsSquare 4 := by decide

This one native_decide works but again, I don't understand why this fails though. It doesn't involve /, right?

tactic 'decide' failed for proposition
  IsSquare 4
since its 'Decidable' instance
  Nat.instDecidablePredIsSquare 4
did not reduce to 'isTrue' or 'isFalse'.

After unfolding the instances 'decidable_of_decidable_of_iff', 'decidable_of_iff'', 'instDecidableEqBool', 'instDecidableEqNat', 'Bool.decEq', 'Nat.decEq', 'Nat.decLe' and 'Nat.instDecidablePredIsSquare', reduction got stuck at the 'Decidable' instance
  match h : (Nat.sqrt 4 * Nat.sqrt 4).beq 4 with
  | true => isTrue ⋯
  | false => isFalse ⋯

[Eric Wieser]

The decision procedure involves Nat.sqrt, which is also irreducible

[Eric Wieser]

All of these changes are new-ish due to Lean changing the rules for reducibility

[Jireh Loreaux]

Is the solution to unseal something?

[Eric Wieser]

Not really, I think well-founded recursion is the real cause