If a finite number of propositions are decidable

Stream: new members

[Asei Inoue]

I wanted to show that if a finite number of propositions are decidable, then the proposition that they all hold is also decidable. However, an error occurred and I could not write what I needed to show.

variable {n : Nat} (P : Fin n → Prop)

-- #check (Nat → Prop)

def all {n : Nat} (props : Fin n → Prop) : Prop := ∀ n, props n

/-
application type mismatch
  Decidable all
argument
  all
has type
  (Fin ?m.44 → Prop) → Prop : Type
but is expected to have type
  Prop : Type
-/
instance (h : (i : Fin n) → Decidable (P i)) : Decidable all where

[Markus Himmel]

Your all has an explicit parameter which you need to supply:

variable {n : Nat} (P : Fin n → Prop)

def all {n : Nat} (props : Fin n → Prop) : Prop := ∀ n, props n

instance [(i : Fin n) → Decidable (P i)] : Decidable (all P) :=
  show Decidable (∀ n, P n) from inferInstance

[Asei Inoue]

@Markus Himmel Thank you!