Decidable instance

Stream: new members

[Sébastien Boisgérault]

Hello! :wave:

Below my first definition of an instance of Decidable. That works, but I am pretty sure that my definition of the instance is very clunky; could anyone have a look at suggest a more terse/idiomatic implementation?

import Mathlib

inductive TheAnswerIs : Nat -> Prop where
| intro : TheAnswerIs 42

/--
error: failed to synthesize
  Decidable (TheAnswerIs 0)

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
#synth Decidable (TheAnswerIs 0)

instance (n : Nat) : Decidable (TheAnswerIs n) :=
  if h : 42 = n then
    isTrue (cast (congrArg TheAnswerIs h) TheAnswerIs.intro)
  else
    have k : ¬TheAnswerIs n := by
      intro answer
      match answer with
      | TheAnswerIs.intro => simp at h
    isFalse k

#synth Decidable (TheAnswerIs 0)

#synth Decidable (TheAnswerIs 42)

#eval decide (TheAnswerIs 0)
-- false

#eval decide (TheAnswerIs 42)
-- true

Best regards,

Sébastien

[Kenny Lau]

you would first prove that theansweris n iff n = 42 and then pull over the decidable instance for equality

[Sébastien Boisgérault]

Something like that?

-- Simpler derivation of the instance
theorem the_answer_is_iff_eq {n : Nat} : TheAnswerIs n <-> n = 42 := by
  constructor
  . intro answer
    match answer with
    | TheAnswerIs.intro => rfl
  . intro h
    rw [h]
    exact TheAnswerIs.intro

instance (n : Nat) : Decidable (TheAnswerIs n) :=
  match decEq n 42 with
  | Decidable.isFalse h => isFalse ((Iff.not the_answer_is_iff_eq).mpr h)
  | Decidable.isTrue h => isTrue (the_answer_is_iff_eq.mpr h)

It is indeed cleaner. Thank you !:thank_you:

[Kenny Lau]

@Sébastien Boisgérault there is already a standard way to pull it over

[Kenny Lau]

decidable_of_decidable_of_iff

[Sébastien Boisgérault]

Ah, I see!

instance (n : Nat) : Decidable (TheAnswerIs n) :=
  decidable_of_decidable_of_iff the_answer_is_iff_eq.symm

[Kenny Lau]

inductive TheAnswerIs : Nat → Prop where
  | intro : TheAnswerIs 42

theorem theAnswerIs_iff_eq_42 {n : Nat} : TheAnswerIs n ↔ n = 42 :=
  ⟨fun ⟨⟩ ↦ rfl, (· ▸ ⟨⟩)⟩

instance (n : Nat) : Decidable (TheAnswerIs n) :=
  decidable_of_decidable_of_iff theAnswerIs_iff_eq_42.symm