attribute [local simp] Decidable.imp_iff_not_or

Stream: new members

[Lars Ericson]

Just curious, is attribute [local simp] documented anywhere? I was getting an error

'Decidable.imp_iff_not_or' does not have [simp] attribute

and Perplexity.AI suggested this workaround, which worked, but I can't find a Lean tutorial or users manual that discusses it.

[Ruben Van de Velde]

In what context did you get that error?

[Kyle Miller]

That error only happens if you are trying to do simp [-Decidable.imp_iff_not_or]. The error means "Decidable.imp_iff_not_or is not a simp lemma. There is no need to remove it from the simp set."

There's no need to do attribute [local simp] just to enable removing it again.

[Lars Ericson]

I am playing with @Alex Oltean 's thesis code for hybrid logic and I needed it to make this lemma check:

attribute [local simp] Decidable.imp_iff_not_or

lemma new_nom_gt      : nom_occurs i φ → i.letter < φ.new_nom.letter   := by
  induction φ with
  | nom i          =>
      simp [nom_occurs, Form.new_nom, -Decidable.imp_iff_not_or]
      intro h
      rw [h]
      exact Nat.lt_succ_self i.letter
  | impl ψ χ ih1 ih2 =>
      simp only [nom_occurs, Form.new_nom, Bool.or_eq_true, max]
      intro h
      apply Or.elim h
      . intro ha
        clear ih2 h
        have ih1 := ih1 ha
        by_cases hc : (Form.new_nom ψ).letter > (Form.new_nom χ).letter
        . simp [hc]
          assumption
        . simp [hc]
          simp at hc
          exact Nat.lt_of_lt_of_le ih1 hc
      . intro hb
        clear ih1 h
        have ih2 := ih2 hb
        by_cases hc : (Form.new_nom ψ).letter > (Form.new_nom χ).letter
        . simp [hc]
          simp at hc
          exact Nat.lt_trans ih2 hc
        . simp [hc]
          assumption
  | box      =>
      assumption
  | bind     =>
      assumption
  | _ => simp [nom_occurs]

In his original code he defined a theorem

@[simp]
theorem implication_disjunction : (p → q) ↔ (¬p ∨ q) := by
  apply Iff.intro
  . intro impl
    exact byCases
      (λ hp  :  p => Or.inr (impl hp))
      (λ hnp : ¬p => Or.inl hnp)
  . intros disj hp
    exact Or.elim disj
      (λ hnp : ¬p => False.elim (hnp hp))
      (λ hq  :  q => hq)

which using apply? turns out to be Decidable.imp_iff_not_or. The theorem is labelled with [simp]. Without thinking about that I replaced all uses of implication_disjunction with Decidable.imp_iff_not_or. Then I got the error about it not being a simp lemma, and then Perplexity gave me that fix. Then I was curious about the fix and I couldn't find it in the manual. That's the whole story!

[Kyle Miller]

attribute [...] declName is how you set attributes after the fact, rather than using the @[...] declaration syntax.

Just like how @[local simp] declaration adds the simp attribute in only the current scope, attribute [local simp] declName adds the simp attribute in only the local scope.