decidable vector

Stream: new members

[Bjørn Kjos-Hanssen]

How do I get Lean to recognize a quantifier like ∀ g : vector (fin 2) 3 as decidable?

As a mwe, I think this code worked last year, but now I get failed to synthesize class instance for decidable.

def is_witness {n:ℕ} (b:ℕ) (x : vector (fin b) n) (q:ℕ) (h : vector (fin q) n.succ): Prop :=
  ∀ g : vector (fin q) n.succ,
    g.1.nth 0 = h.1.nth 0 →
    g.1.nth n = h.1.nth n →
    ∀ y : vector (fin b) n, (
      ∀ k : fin n, ∃ l : fin n,
        [h.nth l.1, h.nth l.1.succ] =
        [g.nth k.1, g.nth k.1.succ] ∧ x.nth l = y.nth k
    ) →
    g=h ∧ x=y

instance {n:ℕ} (b:ℕ) (x : vector (fin b) n) (q:ℕ) (h : vector (fin q) n.succ):
decidable (is_witness b x q h) :=
decidable_of_iff (
  ∀ g : vector (fin q) n.succ,
    g.1.nth 0 = h.1.nth 0 →
    g.1.nth n = h.1.nth n →
    ∀ y : vector (fin b) n, (
      ∀ k : fin n, ∃ l : fin n,
        [h.nth l.1, h.nth l.1.succ] =
        [g.nth k.1, g.nth k.1.succ] ∧ x.nth l = y.nth k
    ) →
    g=h ∧ x=y
) (by rw is_witness)

[Mario Carneiro]

there should be an instance of fintype (vector A n) when fintype A

[Bjørn Kjos-Hanssen]

Thanks @Mario Carneiro this does fix the problem (but it has a sorry):

instance {b n : ℕ} : fintype (vector (fin b) n) := sorry

[Mario Carneiro]

you are probably just missing an import if by apply_instance doesn't prove it

[Mario Carneiro]

import data.fintype.vector maybe

[Bjørn Kjos-Hanssen]

Thanks, that did it! So I guess to get anything to be decidable one tries to import data.fintype.anything.