lean fails to determine [] in s decidable?

Stream: general

[Jared green]

how could it be? i get the error message :
typeclass instance problem is stuck, it is often due to metavariables
Decidable ([] ∈ s)
for this:

import Init.Data.List
import Init.PropLemmas
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
import Batteries.Data.List.Basic

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

def bcompatible (s : List (Bool × normalizable α pred)) (t : List (Bool × normalizable α pred)) : Bool :=
  s.all (fun x => t.all (fun y =>  x.snd == y.snd -> x.fst == y.fst))

def cleand (wireset : List ( normalizable α pred)) (n : List (List (List (Bool × normalizable α pred)))) : List (List (List (Bool × normalizable α pred))) :=
  let wireset_t : List (Bool × normalizable α pred) := (wireset).foldr (fun x y => (true,x) :: (false,x) :: y) [];
  let complement : List (Bool × normalizable α pred) -> List (Bool × normalizable α pred) := fun x : List (Bool × normalizable α pred) =>
  wireset_t.filter (fun y : Bool × normalizable α pred =>  ¬ (y ∈ x));
  let s := n.map (fun x => x.filter (fun y => wireset ⊆ (y.map Prod.snd)));
  let f := (if [] ∈ s then s else
    ((s.map (fun t =>
      (t.filter
        (fun w => s.all
          (fun u => u.any
            (fun v => bcompatible (complement v) (complement w))))))).map
    (fun t => t.map
      (fun r =>
        (((s.filter
          (fun u => u ≠ t)).map
          (fun p =>
            (p.filter
              (fun v => bcompatible (complement v) (complement r))))).map
        (fun w => List.flatten (w.filter
          (fun v => bcompatible (complement v) (complement r))))).foldr
        (fun x y => y.filter (fun z => z ∈ x)) r))));
  if f = s then s else cleand wireset f

[Matt Diamond]

I'm not sure what's going on, but if you want a quick fix to get past the error for now, you can add this line above the if statement:

have : Decidable ([] ∈ s) := by infer_instance

(For some reason inferInstance doesn't work here in term mode...)

[Jared green]

now how about proving termination? (all the individual lists get shorter because of filtering)

[Jz Pan]

Matt Diamond said:

I'm not sure what's going on, but if you want a quick fix to get past the error for now, you can add this line above the if statement:

have : Decidable ([] ∈ s) := by infer_instance

(For some reason inferInstance doesn't work here in term mode...)

Maybe you want let instead of have since Decidable carries data.

[Jared green]

doesnt work

[Damiano Testa]

I think that Lean is failing to infer the type of s: explicitly mentioning the type ascription (with the type copied from the infoview!) makes the ite works:

(if [] ∈ (s : List (List (List (Bool × normalizable α pred)))) then s else ...

[Damiano Testa]

There might be some "depth" involved when trying to synthesize the instance and it might give up after some number of attempts, which is too many in this case.

[Jared green]

first, it makes more sense to place it on the initial let binding(on s). second, why would it go deeper than 1 for a list type?