f20cae3729
This PR sets the `irreducible` attribute before generating the equations for recursive definitions. This prevents these equations to be marked as `defeq`, which could lead to `simp` generation proofs that do not type check at default transparency. This issue is surfacing more easily since well-founded recursion on `Nat` is implemented with a dedicated fix point operator (#7965). Before that, `WellFounded.fix` was used, which is inherently not reducing, so we did get the desired result even without the explicit reducibility setting. Fixes #12398.
70 lines
1.9 KiB
Text
70 lines
1.9 KiB
Text
inductive PFormula (α: Type): Type where
|
||
| And: Array (PFormula α) → PFormula α
|
||
| Or: Array (PFormula α) → PFormula α
|
||
| Not: (PFormula α) → PFormula α
|
||
| Atom: α → PFormula α
|
||
| FF: PFormula α
|
||
| TT: PFormula α
|
||
|
||
namespace PFormula
|
||
|
||
@[simp]
|
||
def is_atom (f: PFormula α): Prop :=
|
||
match f with
|
||
| .Atom _ => True
|
||
| _ => False
|
||
|
||
-- set_option trace.Elab.definition.eqns true
|
||
def is_nnf (f: PFormula α): Prop :=
|
||
match f with
|
||
| .And a | .Or a => all_nnf a
|
||
| .Not g => g.is_atom
|
||
| .Atom _ | .TT | .FF => True
|
||
termination_by sizeOf f
|
||
where
|
||
all_nnf (a: Array (PFormula α)): Prop := ∀ i, (h: i < a.size) → a[i].is_nnf
|
||
termination_by sizeOf a
|
||
|
||
-- This is irreducible
|
||
|
||
/-- info: @[irreducible] def PFormula.is_nnf : {α : Type} → PFormula α → Prop -/
|
||
#guard_msgs in
|
||
#print sig is_nnf
|
||
|
||
-- So this should not be defeq!
|
||
|
||
/-- info: theorem PFormula.is_nnf.eq_4 : ∀ {α : Type} (a : α), (Atom a).is_nnf = True -/
|
||
#guard_msgs(pass trace, all) in
|
||
#print sig is_nnf.eq_4
|
||
|
||
-- If we try to prove it manually, it the irreducibility of `is_nnf` prevents that:
|
||
theorem eq_4 : ∀ {α : Type} (a : α), (Atom a).is_nnf = True := by
|
||
intros
|
||
fail_if_success rfl -- Should not work
|
||
apply is_nnf.eq_4
|
||
|
||
|
||
def to_nnf (f: PFormula α): PFormula α :=
|
||
match f with
|
||
| .And a => And (a.mapFinIdx (fun i _ _ => a[i].to_nnf))
|
||
| .Or a => Or (a.mapFinIdx (fun i _ _ => a[i].to_nnf))
|
||
| .Not g =>
|
||
match g with
|
||
| .And a => Or (a.mapFinIdx
|
||
(fun i _ _ =>
|
||
have : sizeOf a[i] < sizeOf a := by simp
|
||
(Not a[i]).to_nnf))
|
||
| .Or a => And (a.mapFinIdx
|
||
(fun i _ _ =>
|
||
have : sizeOf a[i] < sizeOf a := by simp
|
||
(Not a[i]).to_nnf))
|
||
| .Not h => h.to_nnf
|
||
| .Atom x => Not (.Atom x)
|
||
| .TT => .FF
|
||
| .FF => .TT
|
||
| g => g
|
||
|
||
theorem test: (TT: PFormula α).Not.to_nnf.is_nnf := by
|
||
simp [is_nnf, to_nnf]
|
||
|
||
end PFormula
|