decidable instance of prop logic eval function

Stream: general

[Paige Thomas]

I'm wondering if there is a way to make the #eval here work, where it gives

failed to synthesize
  Decidable (eval (gen_valuation (fun x => True) [("P", False)]) (atom_ "P"))

I proved a decidable instance, but I'm guessing it probably can't use it because of the (h1 : ∀ (el : String × Prop), el ∈ l → Decidable el.2) hypothesis?

import Mathlib.Tactic
import Mathlib.Util.CompileInductive


set_option autoImplicit false


namespace Prop_

/--
  The type of formulas.
-/
inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Repr

compile_inductive% Formula_


open Formula_


/--
  A function from the set of atoms to the set of truth values `{False, True}`.
-/
def Valuation : Type := String → Prop
  deriving Inhabited


/--
  `eval V F` := True if and only if the formula `F` evaluates to `True` given the valuation `V`.
-/
def eval
  (V : Valuation) :
  Formula_ → Prop
  | false_ => False
  | true_ => True
  | atom_ X => V X
  | not_ phi => ¬ eval V phi
  | and_ phi psi => eval V phi ∧ eval V psi
  | or_ phi psi => eval V phi ∨ eval V psi
  | imp_ phi psi => eval V phi → eval V psi
  | iff_ phi psi => eval V phi ↔ eval V psi

instance
  (V : Valuation)
  [DecidablePred V]
  (F : Formula_) :
  Decidable (eval V F) :=
  by
  induction F
  all_goals
    simp only [eval]
    infer_instance

def Function.updateITE
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a : α)
  (b : β)
  (c : α) :
  β :=
  if c = a then b else f c


def gen_valuation
  (default : Valuation) :
  List (String × Prop) → Valuation
  | [] => default
  | hd :: tl => Function.updateITE (gen_valuation default tl) hd.fst hd.snd


instance
  (V : Valuation)
  [DecidablePred V]
  (l : List (String × Prop))
  (F : Formula_)
  (h1 : ∀ (el : String × Prop), el ∈ l → Decidable el.2) :
  Decidable (eval (gen_valuation V l) F) :=
  by
  have s1 : DecidablePred (gen_valuation V l) :=
  by
    induction l
    case nil =>
      simp only [gen_valuation]
      infer_instance
    case cons hd tl ih =>
      simp only [gen_valuation]
      unfold DecidablePred
      intro a
      simp only [Function.updateITE]
      split_ifs
      case pos c1 =>
        apply h1
        simp
      case neg c1 =>
        apply ih
        intro el a1
        apply h1
        simp
        tauto
  infer_instance


#eval eval (gen_valuation (fun _ => True) [("P", False)]) (atom_ "P")

[Yury G. Kudryashov]

Instance search doesn't work with non instance assumptions

[Paige Thomas]

I guess maybe I should change this all to Bool.

[Yury G. Kudryashov]

If you don't need undecidable propositions, then Bool is better.

[Paige Thomas]

I haveset_option autoImplicit false, but for some reason it doesn't complain about eval V P ↔ eval V Q, where both eval V P and eval V Q are Bool. Is there a way to make it complain and require that it be written (eval V P = true) ↔ (eval V Q = true)?

[Yury G. Kudryashov]

This has nothing to do with autoImplicit. Lean knows how to coerce a Bool to a Prop.

[Yury G. Kudryashov]

So, if you use a Bool in a context that expects Prop, then it replaces it with b = true.

[Yury G. Kudryashov]

It's docs#boolToProp

[Yury G. Kudryashov]

You can try locally disabling this instance.

[Paige Thomas]

I see.

[Paige Thomas]

Is there a way to disable all automatic coercions?

[Yury G. Kudryashov]

AFAIK, no. Why do you want it?

[Paige Thomas]

Just to make it easier to differentiate things and see what the type really is and what is being done.

[Paige Thomas]

I can write it manually, but if it complained I would be sure of not missing an instance.

[Paige Thomas]

Alternatively a linter would also work.