From fa36fcd448a6473c2aaaa5582953b4d074fe2cc5 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 18 Sep 2025 23:27:25 +0200 Subject: [PATCH] feat: linear-size BEq instance (#10268) This PR adds an alternative implementation of `DerivingBEq` based on comparing `.ctorIdx` and using a dedicated matcher for comparing same constructors (added in #10152), to avoid the quadratic overhead of the default match implementation. The new option `deriving.beq.linear_construction_threshold` sets the constructor count threshold (10 by default) for using the new construction. Such instances also allow `deriving ReflBEq, LawfulBeq`, although these proofs for these properties are still quadratic. --- src/Init/LawfulBEqTactics.lean | 4 +- src/Lean/Elab/Deriving/BEq.lean | 85 ++++++++- src/Lean/Elab/Deriving/DecEq.lean | 1 - .../Meta/Constructions/CasesOnSameCtor.lean | 7 - src/Lean/Meta/MethodSpecs.lean | 5 +- src/Lean/Meta/Tactic/Simp/Types.lean | 7 + tests/lean/run/decEqNonInjIndex.lean | 12 +- tests/lean/run/derivingBEq.lean | 85 ++++++++- tests/lean/run/derivingBEqLinear.lean | 177 ++++++++++++++++++ tests/lean/run/derivingReflBEq.lean | 118 +++++++++++- tests/lean/run/methodSpecsDeriving.lean | 2 + tests/lean/run/reduceBEqSimproc.lean | 37 ++++ 12 files changed, 506 insertions(+), 34 deletions(-) create mode 100644 tests/lean/run/derivingBEqLinear.lean diff --git a/src/Init/LawfulBEqTactics.lean b/src/Init/LawfulBEqTactics.lean index 6e60f5621d..a4940380db 100644 --- a/src/Init/LawfulBEqTactics.lean +++ b/src/Init/LawfulBEqTactics.lean @@ -21,7 +21,7 @@ macro "deriving_ReflEq_tactic" : tactic => `(tactic|( intro x induction x all_goals - simp only [ BEq.refl, ↓reduceDIte, Bool.and_true, *, reduceBEq ] + simp only [ BEq.refl, ↓reduceDIte, Bool.and_true, *, reduceBEq ,reduceCtorIdx] )) theorem and_true_curry {a b : Bool} {P : Prop} @@ -99,6 +99,6 @@ macro "deriving_LawfulEq_tactic" : tactic => `(tactic|( intro y cases y all_goals - simp only [reduceBEq] + simp only [reduceBEq, reduceCtorIdx] repeat deriving_LawfulEq_tactic_step )) diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 1d4e647d33..d6eb3aad9b 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -10,17 +10,27 @@ public import Lean.Data.Options import Lean.Meta.Transform import Lean.Elab.Deriving.Basic import Lean.Elab.Deriving.Util -import Lean.Meta.Eqns +import Lean.Meta.Constructions.CtorIdx +import Lean.Meta.Constructions.CasesOnSameCtor import Lean.Meta.SameCtorUtils namespace Lean.Elab.Deriving.BEq open Lean.Parser.Term open Meta + +register_builtin_option deriving.beq.linear_construction_threshold : Nat := { + defValue := 10 + descr := "If the inductive data type has this many or more constructors, use a different \ + implementation for implementing `BEq` that avoids the quadratic code size produced by the \ + default implementation.\n\n\ + The alternative construction compiles to less efficient code in some cases, so by default \ + it is only used for inductive types with 10 or more constructors." } + def mkBEqHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `BEq 2 indVal -def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do +def mkMatchOld (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) @@ -99,6 +109,77 @@ where alts := alts.push (← mkElseAlt) return alts +def mkMatchNew (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do + assert! header.targetNames.size == 2 + + let x1 := mkIdent header.targetNames[0]! + let x2 := mkIdent header.targetNames[1]! + let ctorIdxName := mkCtorIdxName indVal.name + -- NB: the getMatcherInfo? assumes all matchers are called `match_` + let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor) + mkCasesOnSameCtor casesOnSameCtorName indVal.name + let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do + let ctorName := indVal.ctors[ctorIdx]! + let ctorInfo ← getConstInfoCtor ctorName + forallTelescopeReducing ctorInfo.type fun xs type => do + let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies + let mut ctorArgs1 : Array Term := #[] + let mut ctorArgs2 : Array Term := #[] + + let mut rhs ← `(true) + let mut rhs_empty := true + for i in *...ctorInfo.numFields do + let pos := indVal.numParams + ctorInfo.numFields - i - 1 + let x := xs[pos]! + if type.containsFVar x.fvarId! then + -- If resulting type depends on this field, we don't need to compare + -- and the casesOnSameCtor only has a parameter for it once + ctorArgs1 := ctorArgs1.push (← `(_)) + else + let userName ← x.fvarId!.getUserName + let a := mkIdent (← mkFreshUserName userName) + let b := mkIdent (← mkFreshUserName (userName.appendAfter "'")) + ctorArgs1 := ctorArgs1.push a + ctorArgs2 := ctorArgs2.push b + let xType ← inferType x + if (← isProp xType) then + continue + if xType.isAppOf indVal.name then + if rhs_empty then + rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident) + rhs_empty := false + else + rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident && $rhs) + /- If `x` appears in the type of another field, use `eq_of_beq` to + unify the types of the subsequent variables -/ + else if ← xs[(pos+1)...*].anyM + (fun fvar => (Expr.containsFVar · x.fvarId!) <$> (inferType fvar)) then + rhs ← `(if h : $a:ident == $b:ident then by + cases (eq_of_beq h) + exact $rhs + else false) + rhs_empty := false + else + if rhs_empty then + rhs ← `($a:ident == $b:ident) + rhs_empty := false + else + rhs ← `($a:ident == $b:ident && $rhs) + `(@fun $ctorArgs1.reverse:term* $ctorArgs2.reverse:term* =>$rhs:term) + if indVal.numCtors == 1 then + `( $(mkCIdent casesOnSameCtorName) $x1:term $x2:term rfl $alts:term* ) + else + `( match decEq ($(mkCIdent ctorIdxName) $x1:ident) ($(mkCIdent ctorIdxName) $x2:ident) with + | .isTrue h => $(mkCIdent casesOnSameCtorName) $x1:term $x2:term h $alts:term* + | .isFalse _ => false) + +def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do + if indVal.numCtors ≥ deriving.beq.linear_construction_threshold.get (← getOptions) then + mkMatchNew header indVal auxFunName + else + mkMatchOld header indVal auxFunName + + def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do let auxFunName := ctx.auxFunNames[i]! let indVal := ctx.typeInfos[i]! diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index ca90639f0d..70047ba5fa 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -13,7 +13,6 @@ import Lean.Elab.Deriving.Basic import Lean.Elab.Deriving.Util import Lean.Meta.NatTable import Lean.Meta.Constructions.CtorIdx -import Lean.Meta.Constructions.CtorElim import Lean.Meta.Constructions.CasesOnSameCtor import Lean.Meta.SameCtorUtils diff --git a/src/Lean/Meta/Constructions/CasesOnSameCtor.lean b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean index 866bc7b4fb..3f3d0c6534 100644 --- a/src/Lean/Meta/Constructions/CasesOnSameCtor.lean +++ b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean @@ -220,13 +220,6 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit := Match.addMatcherInfo declName matcherInfo setInlineAttribute declName - -- Pragmatic hack: - -- Normally a matcher is not marked as an aux recursor. We still do that here - -- because this makes the elaborator unfold it more eagerily, it seems, - -- and this works around issues with the structural recursion equation generator - -- (see #10195). - modifyEnv fun env => markAuxRecursor env declName - enableRealizationsForConst declName compileDecl decl diff --git a/src/Lean/Meta/MethodSpecs.lean b/src/Lean/Meta/MethodSpecs.lean index 0b8a2865c9..8d7854d452 100644 --- a/src/Lean/Meta/MethodSpecs.lean +++ b/src/Lean/Meta/MethodSpecs.lean @@ -163,7 +163,8 @@ def rewriteThm (ctx : Simp.Context) (simprocs : Simprocs) let thmInfo ← getConstVal eqThmName let (result, _) ← simp thmInfo.type ctx (simprocs := #[simprocs]) trace[Meta.MethodSpecs] "type for {destThmName}:{indentExpr result.expr}" - let value ← result.mkEqMPR <| mkConst eqThmName (thmInfo.levelParams.map mkLevelParam) + let eqThmApp := mkConst eqThmName (thmInfo.levelParams.map mkLevelParam) + let value := mkAppN (mkConst ``Eq.mp [0]) #[thmInfo.type, result.expr, ← result.getProof, eqThmApp] addDecl <| Declaration.thmDecl { name := destThmName levelParams := thmInfo.levelParams @@ -186,7 +187,7 @@ where let ctx ← Simp.mkContext (simpTheorems := #[s]) (congrTheorems := (← getSimpCongrTheorems)) - (config := { } ) -- Simp.neutralConfig with dsimp := true, letToHave := false }) + (config := { } ) let simprocs ← Simp.getSimprocs let env ← getEnv diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 87a7ed24b5..a9c2f93b4b 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -559,6 +559,13 @@ def Result.mkEqMPR (r : Simp.Result) (e : Expr) : MetaM Expr := do else Meta.mkEqMPR (← r.getProof) e +/-- Construct the `Expr` `h.mp e`, from a `Simp.Result` with proof `h`. -/ +def Result.mkEqMP (r : Simp.Result) (e : Expr) : MetaM Expr := do + if r.proof?.isNone && r.expr == e then + pure e + else + Meta.mkEqMP (← r.getProof) e + def mkCongrFun (r : Result) (a : Expr) : MetaM Result := match r.proof? with | none => return { expr := mkApp r.expr a, proof? := none } diff --git a/tests/lean/run/decEqNonInjIndex.lean b/tests/lean/run/decEqNonInjIndex.lean index 7e04632c6a..e66c25a9aa 100644 --- a/tests/lean/run/decEqNonInjIndex.lean +++ b/tests/lean/run/decEqNonInjIndex.lean @@ -6,18 +6,9 @@ non-injective indices, and just how bad the error messages are. opaque f : Nat → Nat set_option deriving.decEq.linear_construction_threshold 0 +set_option deriving.beq.linear_construction_threshold 0 /-- -error: Tactic `cases` failed with a nested error: -Dependent elimination failed: Failed to solve equation - f n✝¹ = f n✝ -at case `T.mk1` after processing - _, (T.mk1 _ _), _ -the dependent pattern matcher can solve the following kinds of equations -- = and = -- = where the terms are definitionally equal -- = , examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil ---- error: Dependent elimination failed: Failed to solve equation f n✝ = f n -/ @@ -29,6 +20,7 @@ deriving BEq, DecidableEq set_option deriving.decEq.linear_construction_threshold 10000 +set_option deriving.beq.linear_construction_threshold 10000 /-- error: Tactic `cases` failed with a nested error: diff --git a/tests/lean/run/derivingBEq.lean b/tests/lean/run/derivingBEq.lean index de07480f4b..52a1a79d70 100644 --- a/tests/lean/run/derivingBEq.lean +++ b/tests/lean/run/derivingBEq.lean @@ -1,11 +1,17 @@ module +set_option deriving.beq.linear_construction_threshold 1000 + public section inductive Foo | mk1 | mk2 | mk3 deriving @[expose] BEq +/-- info: instBEqFoo.beq_spec (x✝ y✝ : Foo) : (x✝ == y✝) = (x✝.ctorIdx == y✝.ctorIdx) -/ +#guard_msgs in +#check instBEqFoo.beq_spec + namespace Foo theorem ex1 : (mk1 == mk2) = false := rfl @@ -19,17 +25,68 @@ theorem ex5 : (mk2 == mk3) = false := rfl end Foo +inductive L (α : Type u) : Type u + | nil : L α + | cons : α → L α → L α + deriving @[expose] BEq + +/-- +info: instBEqL.beq_spec.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) : + (x✝ == x✝¹) = + match x✝, x✝¹ with + | L.nil, L.nil => true + | L.cons a a_1, L.cons b b_1 => a == b && a_1 == b_1 + | x, x_1 => false +-/ +#guard_msgs in +#check instBEqL.beq_spec + +namespace L +theorem ex1 : (L.cons 10 L.nil == L.cons 20 L.nil) = false := rfl +theorem ex2 : (L.cons 10 L.nil == L.nil) = false := rfl +end L + +namespace InNamespace +inductive L' (α : Type u) : Type u + | nil : L' α + | cons : α → L' α → L' α + deriving @[expose] BEq + +end InNamespace +/-- +info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α) +-/ +#guard_msgs in #print sig InNamespace.instBEqL' +/-- +info: theorem InNamespace.instBEqL'.beq_spec.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : InNamespace.L' α), + (x == x_1) = + match x, x_1 with + | InNamespace.L'.nil, InNamespace.L'.nil => true + | InNamespace.L'.cons a a_1, InNamespace.L'.cons b b_1 => a == b && a_1 == b_1 + | x, x_2 => false +-/ +#guard_msgs in #print sig InNamespace.instBEqL'.beq_spec + inductive Vec (α : Type u) : Nat → Type u | nil : Vec α 0 | cons : α → {n : Nat} → Vec α n → Vec α (n+1) deriving @[expose] BEq -namespace Vec -theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false := - rfl +/-- +info: instBEqVec.beq_spec.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] (x✝ x✝¹ : Vec α✝ a✝) : + (x✝ == x✝¹) = + match a✝, x✝, x✝¹ with + | .(0), Vec.nil, Vec.nil => true + | .(a_1 + 1), Vec.cons a a_2, Vec.cons b b_1 => a == b && a_2 == b_1 + | x, x_1, x_2 => false +-/ +#guard_msgs in +#check instBEqVec.beq_spec -theorem ex2 : (cons 10 Vec.nil == cons 10 Vec.nil) = true := - rfl +namespace Vec +theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false := rfl + +theorem ex2 : (cons 10 Vec.nil == cons 10 Vec.nil) = true := rfl theorem ex3 : (cons 20 (cons 11 Vec.nil) == cons 20 (cons 10 Vec.nil)) = false := rfl @@ -101,6 +158,24 @@ deriving BEq #with_exporting #reduce fun (a : PrivField) => a == a +private structure PrivStruct where + a : Nat +deriving BEq + +-- Instance and spec should be private +/-- info: private def instBEqPrivStruct : BEq PrivStruct -/ +#guard_msgs in +#print sig instBEqPrivStruct + +/-- info: private def instBEqPrivStruct.beq : PrivStruct → PrivStruct → Bool -/ +#guard_msgs in +#print sig instBEqPrivStruct.beq +/-- +info: private theorem instBEqPrivStruct.beq_spec : ∀ (x x_1 : PrivStruct), (x == x_1) = (x.a == x_1.a) +-/ +#guard_msgs in +#print sig instBEqPrivStruct.beq_spec + end -- Try again without `public section` diff --git a/tests/lean/run/derivingBEqLinear.lean b/tests/lean/run/derivingBEqLinear.lean new file mode 100644 index 0000000000..11257bf6b3 --- /dev/null +++ b/tests/lean/run/derivingBEqLinear.lean @@ -0,0 +1,177 @@ +module + +set_option deriving.beq.linear_construction_threshold 0 + +public section + +inductive Foo + | mk1 | mk2 | mk3 + deriving @[expose] BEq + +/-- info: instBEqFoo.beq_spec (x✝ y✝ : Foo) : (x✝ == y✝) = (x✝.ctorIdx == y✝.ctorIdx) -/ +#guard_msgs in +#check instBEqFoo.beq_spec + +namespace Foo +theorem ex1 : (mk1 == mk2) = false := + rfl +theorem ex2 : (mk1 == mk1) = true := + rfl +theorem ex3 : (mk2 == mk2) = true := + rfl +theorem ex4 : (mk3 == mk3) = true := + rfl +theorem ex5 : (mk2 == mk3) = false := + rfl +end Foo + +inductive L (α : Type u) : Type u + | nil : L α + | cons : α → L α → L α + deriving @[expose] BEq + +/-- +info: instBEqL.beq_spec.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) : + (x✝ == x✝¹) = + match decEq x✝.ctorIdx x✝¹.ctorIdx with + | isTrue h => + match x✝, x✝¹, h with + | L.nil, L.nil, ⋯ => true + | L.cons a a_1, L.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1 + | isFalse h => false +-/ +#guard_msgs in #check instBEqL.beq_spec + +/-- error: Unknown identifier `instBEqL.beq_spec_2` -/ +#guard_msgs in #check instBEqL.beq_spec_2 + +namespace L +theorem ex1 : (L.cons 10 L.nil == L.cons 20 L.nil) = false := rfl +theorem ex2 : (L.cons 10 L.nil == L.nil) = false := rfl +end L + +namespace InNamespace +inductive L' (α : Type u) : Type u + | nil : L' α + | cons : α → L' α → L' α + deriving @[expose] BEq + +end InNamespace +/-- +info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α) +-/ +#guard_msgs in #print sig InNamespace.instBEqL' +/-- +info: theorem InNamespace.instBEqL'.beq_spec.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : InNamespace.L' α), + (x == x_1) = + match decEq x.ctorIdx x_1.ctorIdx with + | isTrue h => + match x, x_1, h with + | InNamespace.L'.nil, InNamespace.L'.nil, ⋯ => true + | InNamespace.L'.cons a a_1, InNamespace.L'.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1 + | isFalse h => false +-/ +#guard_msgs in #print sig InNamespace.instBEqL'.beq_spec + +inductive Vec (α : Type u) : Nat → Type u + | nil : Vec α 0 + | cons : α → {n : Nat} → Vec α n → Vec α (n+1) + deriving @[expose] BEq + +/-- +info: instBEqVec.beq_spec.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] (x✝ x✝¹ : Vec α✝ a✝) : + (x✝ == x✝¹) = + match decEq x✝.ctorIdx x✝¹.ctorIdx with + | isTrue h => + match a✝, x✝, x✝¹ with + | 0, Vec.nil, Vec.nil, ⋯ => true + | x + 1, Vec.cons a a_1, Vec.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1 + | isFalse h => false +-/ +#guard_msgs in +#check instBEqVec.beq_spec + +namespace Vec +theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false := rfl + +theorem ex2 : (cons 10 Vec.nil == cons 10 Vec.nil) = true := rfl + +theorem ex3 : (cons 20 (cons 11 Vec.nil) == cons 20 (cons 10 Vec.nil)) = false := + rfl + +theorem ex4 : (cons 20 (cons 11 Vec.nil) == cons 20 (cons 11 Vec.nil)) = true := + rfl +end Vec + +inductive Bla (α : Type u) where + | node : List (Bla α) → Bla α + | leaf : α → Bla α + deriving BEq + +namespace Bla + +#guard node [] != leaf 10 +#guard node [leaf 10] == node [leaf 10] +#guard node [leaf 10] != node [leaf 10, leaf 20] + +end Bla + +mutual +inductive Tree (α : Type u) where + | node : TreeList α → Tree α + | leaf : α → Tree α + deriving BEq + +inductive TreeList (α : Type u) where + | nil : TreeList α + | cons : Tree α → TreeList α → TreeList α + deriving BEq +end + +def ex1 [BEq α] : BEq (Tree α) := + inferInstance + +def ex2 [BEq α] : BEq (TreeList α) := + inferInstance + +/-! Private fields should yield public, no-expose instances. -/ + +structure PrivField where + private a : Nat +deriving BEq + +/-- info: fun a => instBEqPrivField.beq a a -/ +#guard_msgs in +#with_exporting +#reduce fun (a : PrivField) => a == a + +private structure PrivStruct where + a : Nat +deriving BEq + +-- Instance and spec should be private +/-- info: private def instBEqPrivStruct : BEq PrivStruct -/ +#guard_msgs in +#print sig instBEqPrivStruct + +/-- info: private def instBEqPrivStruct.beq : PrivStruct → PrivStruct → Bool -/ +#guard_msgs in +#print sig instBEqPrivStruct.beq +/-- +info: private theorem instBEqPrivStruct.beq_spec : ∀ (x x_1 : PrivStruct), (x == x_1) = (x.a == x_1.a) +-/ +#guard_msgs in +#print sig instBEqPrivStruct.beq_spec + +end + +-- Try again without `public section` + +public structure PrivField2 where + private a : Nat +deriving BEq + +/-- info: fun a => instBEqPrivField2.beq a a -/ +#guard_msgs in +#with_exporting +#reduce fun (a : PrivField2) => a == a diff --git a/tests/lean/run/derivingReflBEq.lean b/tests/lean/run/derivingReflBEq.lean index c56a7c70c1..6aab58e7c7 100644 --- a/tests/lean/run/derivingReflBEq.lean +++ b/tests/lean/run/derivingReflBEq.lean @@ -1,3 +1,6 @@ +namespace RegularBEq +set_option deriving.beq.linear_construction_threshold 1000 + -- set_option trace.Elab.Deriving.lawfulBEq true inductive L (α : Type u) where @@ -5,7 +8,9 @@ inductive L (α : Type u) where | cons : α → L α → L α deriving BEq, ReflBEq, LawfulBEq -/-- info: theorem instReflBEqL.{u_1} : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α], ReflBEq (L α) -/ +/-- +info: theorem RegularBEq.instReflBEqL.{u_1} : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α], ReflBEq (L α) +-/ #guard_msgs in #print sig instReflBEqL @@ -15,7 +20,7 @@ inductive Vec (α : Type u) : Nat → Type u where deriving BEq, ReflBEq, LawfulBEq /-- -info: theorem instReflBEqVec.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : BEq α] [ReflBEq α], ReflBEq (Vec α a) +info: theorem RegularBEq.instReflBEqVec.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : BEq α] [ReflBEq α], ReflBEq (Vec α a) -/ #guard_msgs in #print sig instReflBEqVec @@ -25,7 +30,7 @@ inductive Enum | mk1 | mk2 | mk3 deriving BEq, ReflBEq, LawfulBEq -/-- info: theorem instReflBEqEnum : ReflBEq Enum -/ +/-- info: theorem RegularBEq.instReflBEqEnum : ReflBEq Enum -/ #guard_msgs in #print sig instReflBEqEnum @@ -38,13 +43,13 @@ inductive WithHEq (α : Type u) : Nat → Type u where deriving BEq, ReflBEq, LawfulBEq /-- -info: instReflBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [ReflBEq α✝] : ReflBEq (WithHEq α✝ a✝) +info: RegularBEq.instReflBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [ReflBEq α✝] : ReflBEq (WithHEq α✝ a✝) -/ #guard_msgs in #check instReflBEqWithHEq /-- -info: instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [LawfulBEq α✝] : LawfulBEq (WithHEq α✝ a✝) +info: RegularBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [LawfulBEq α✝] : LawfulBEq (WithHEq α✝ a✝) -/ #guard_msgs in #check instLawfulBEqWithHEq @@ -91,3 +96,106 @@ inductive TreeList (α : Type u) where | cons : Tree α → TreeList α → TreeList α deriving BEq end + +end RegularBEq + +namespace LinearBEq +set_option deriving.beq.linear_construction_threshold 0 + +-- set_option trace.Elab.Deriving.lawfulBEq true + +inductive L (α : Type u) where + | nil : L α + | cons : α → L α → L α +deriving BEq, ReflBEq, LawfulBEq + +/-- +info: theorem LinearBEq.instReflBEqL.{u_1} : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α], ReflBEq (L α) +-/ +#guard_msgs in +#print sig instReflBEqL + +inductive Vec (α : Type u) : Nat → Type u where + | nil : Vec α 0 + | cons : ∀ {n}, α → Vec α n → Vec α (n+1) +deriving BEq, ReflBEq, LawfulBEq + +/-- +info: theorem LinearBEq.instReflBEqVec.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : BEq α] [ReflBEq α], ReflBEq (Vec α a) +-/ +#guard_msgs in +#print sig instReflBEqVec + + +inductive Enum + | mk1 | mk2 | mk3 +deriving BEq, ReflBEq, LawfulBEq + +/-- info: theorem LinearBEq.instReflBEqEnum : ReflBEq Enum -/ +#guard_msgs in +#print sig instReflBEqEnum + +-- The following type has `Eq.rec`’s in its `BEq` implementation, +-- but `simp` seems to handle that just fine + +inductive WithHEq (α : Type u) : Nat → Type u where + | nil : WithHEq α 0 + | cons : ∀ {n m} , α → WithHEq α n → WithHEq α m → WithHEq α (n+1) +deriving BEq, ReflBEq, LawfulBEq + +/-- +info: LinearBEq.instReflBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [ReflBEq α✝] : ReflBEq (WithHEq α✝ a✝) +-/ +#guard_msgs in +#check instReflBEqWithHEq + +/-- +info: LinearBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [LawfulBEq α✝] : LawfulBEq (WithHEq α✝ a✝) +-/ +#guard_msgs in +#check instLawfulBEqWithHEq + + +-- No `BEq` derived? Not a great error message yet, but the error location helps, so good enough. + +/-- +error: failed to synthesize + BEq Foo + +Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +-/ +#guard_msgs in +structure Foo where + deriving ReflBEq + +-- No `ReflBEq` but `LawfulBEq`? ot a great error message yet. + +/-- +@ +2:16...25 +error: failed to synthesize + ReflBEq Bar + +Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +-/ +#guard_msgs (positions := true) in +structure Bar where + deriving BEq, LawfulBEq + +/-- +@ +5:16...23 +error: Deriving `ReflBEq` for mutual inductives is not supported +-/ +#guard_msgs (positions := true) in +mutual +inductive Tree (α : Type u) where + | node : TreeList α → Tree α + | leaf : α → Tree α + deriving BEq, ReflBEq, LawfulBEq + +inductive TreeList (α : Type u) where + | nil : TreeList α + | cons : Tree α → TreeList α → TreeList α + deriving BEq +end + +end LinearBEq diff --git a/tests/lean/run/methodSpecsDeriving.lean b/tests/lean/run/methodSpecsDeriving.lean index 40c186aa23..19428fa776 100644 --- a/tests/lean/run/methodSpecsDeriving.lean +++ b/tests/lean/run/methodSpecsDeriving.lean @@ -1,3 +1,5 @@ +set_option deriving.beq.linear_construction_threshold 1000 + inductive L (α : Type) where | nil : L α | cons : α → L α → L α diff --git a/tests/lean/run/reduceBEqSimproc.lean b/tests/lean/run/reduceBEqSimproc.lean index b536387d43..fb8f3e3e4d 100644 --- a/tests/lean/run/reduceBEqSimproc.lean +++ b/tests/lean/run/reduceBEqSimproc.lean @@ -2,6 +2,8 @@ module -- set_option trace.Elab.Deriving.lawfulBEq true -- set_option trace.Meta.MethodSpecs true +set_option deriving.beq.linear_construction_threshold 1000 + inductive L (α : Type u) where | nil : L α | cons : α → L α → L α @@ -12,6 +14,41 @@ example {n m : Nat} (h : n = m) : simp [reduceBEq] assumption +-- Linear construction + +namespace Linear + +set_option deriving.beq.linear_construction_threshold 0 + +inductive L (α : Type u) where + | nil : L α + | cons : α → L α → L α +deriving BEq + +-- This should still split the equations + +/-- +info: Linear.instBEqL.beq.eq_1.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) : + instBEqL.beq x✝ x✝¹ = + match decEq x✝.ctorIdx x✝¹.ctorIdx with + | isTrue h => + match x✝, x✝¹, h with + | L.nil, L.nil, ⋯ => true + | L.cons a a_1, L.cons a' a'_1, ⋯ => a == a' && instBEqL.beq a_1 a'_1 + | isFalse h => false +-/ +#guard_msgs in +#check instBEqL.beq.eq_1 + +-- And this should work without L.ctorIdx + +example {n m : Nat} (h : n = m) : + (L.cons n (L.nil : L Nat) == L.cons m (L.nil : L Nat)) = true := by + simp [reduceBEq, reduceCtorIdx] + assumption + +end Linear + -- Module system interactions namespace A