Type error in simp #12398
Description
Prerequisites
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
On the test theorem below, simp produces this error:
Application type mismatch: The argument
congrArg is_nnf to_nnf.eq_7
has type
TT.Not.to_nnf.is_nnf = FF.is_nnf
but is expected to have type
?p = True
in the application
of_eq_true (congrArg is_nnf to_nnf.eq_7)
Here's the input:
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
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
where
all_nnf (a: Array (PFormula α)): Prop := ∀ i, (h: i < a.size) → a[i].is_nnf
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
Expected behavior:
Close the goal. This used to work before 4.27.0.
Versions
"4.27.0"
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.