turning a definition into simp lemmas

Stream: lean4

[Jared green]

how do i take a function definition with cases and turn it into simp lemmas?

[Jared green]

open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable

def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

[Emilie (Shad Amethyst)]

What simp lemmas do you wish to obtain for it?

[Jared green]

toProp (Not a) <-> ¬(toProp a)

[Emilie (Shad Amethyst)]

I'd try @[simps] or @[reducible] on toProp, to see which suit you best

[Jared green]

what would that look like?

[Emilie (Shad Amethyst)]

Ah, @[simps] doesn't work because you don't have a structure. @[reducible] means that things like simp and instance synthetization will "see through" toProp, and be able to deduce facts directly from its definition.
This means that when applying @[reducible], simp will be able to treat toProp (Not a) as if you had written ¬toProp a:

@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | Atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

variable {pred : α → Prop} {n₁ n₂ : normalizable α pred}

example : toProp (Or (And (Not n₁) n₁) n₂) ↔ toProp n₂ := by
  simp

Alternatively, proving the four simp theorems isn't too tedious in your example, since they are all defEq:

def toProp (n : normalizable α pred) : Prop :=
  match n with
  | Atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

variable {pred : α → Prop} {n₁ n₂ : normalizable α pred}

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (Atom a : normalizable α pred) ↔ pred a := Iff.rfl

example : toProp (Or (And (Not n₁) n₁) n₂) ↔ toProp n₂ := by
  simp

[Eric Wieser]

Can't you just use @[simp] (not simps) on the definition?

[Joachim Breitner]

I believe that adds the full function equation to the simp set, not the specialized variants corresponding to the cases? Although that may be a reasonable feature request. Code for that already exists for recursive definitions.

[Eric Wieser]

If the function is non-recursive, it does what you say. If it is recursive, it does what I say. The lean3 behavior was to always do what I said.

[Marcus Rossel]

And I'm guessing that related to this right?
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/getEqnsFor.3F.20non-recursive.20function/near/411706112