diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index db3a6d1e46..5b4a443d78 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -6,21 +6,32 @@ Authors: Leonardo de Moura module prelude +public import Lean.Data.Options import Lean.Meta.Transform import Lean.Meta.Inductive 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 namespace Lean.Elab.Deriving.DecEq open Lean.Parser.Term open Meta +register_builtin_option deriving.decEq.linear_construction_threshold : Nat := { + defValue := 10 + descr := "If the inductive data type has this many or more constructors, use a different \ + implementation for deciding equality 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 mkDecEqHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `DecidableEq 2 indVal -def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Term := do +def mkMatchOld (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Term := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) @@ -91,6 +102,76 @@ where alts := alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term)) return alts +def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : 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 mathcers 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 todo := #[] + + for i in *...ctorInfo.numFields do + let x := xs[indVal.numParams + i]! + if type.containsFVar x.fvarId! then + -- If resulting type depends on this field, we don't need to bring it into + -- scope nor compare it + ctorArgs1 := ctorArgs1.push (← `(_)) + else + let a := mkIdent (← mkFreshUserName `a) + let b := mkIdent (← mkFreshUserName `b) + ctorArgs1 := ctorArgs1.push a + ctorArgs2 := ctorArgs2.push b + let xType ← inferType x + let indValNum := + ctx.typeInfos.findIdx? + (xType.isAppOf ∘ ConstantVal.name ∘ InductiveVal.toConstantVal) + let recField := indValNum.map (ctx.auxFunNames[·]!) + let isProof ← isProp xType + todo := todo.push (a, b, recField, isProof) + let rhs ← mkSameCtorRhs todo.toList + `(@fun $ctorArgs1:term* $ctorArgs2:term* =>$rhs:term) + if indVal.numCtors == 1 then + `( $(mkCIdent casesOnSameCtorName) $x1:term $x2:term rfl $alts:term* ) + else + `( if h : $(mkCIdent ctorIdxName) $x1:ident = $(mkCIdent ctorIdxName) $x2:ident then + $(mkCIdent casesOnSameCtorName) $x1:term $x2:term h $alts:term* + else + isFalse (fun h' => h (congrArg $(mkCIdent ctorIdxName) h'))) +where + mkSameCtorRhs : List (Ident × Ident × Option Name × Bool) → TermElabM Term + | [] => ``(isTrue rfl) + | (a, b, recField, isProof) :: todo => withFreshMacroScope do + let rhs ← if isProof then + `(have h : @$a = @$b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term) + else + let sameCtor ← mkSameCtorRhs todo + `(if h : @$a = @$b then + by subst h; exact $sameCtor:term + else + isFalse (by intro n; injection n; apply h _; assumption)) + if let some auxFunName := recField then + -- add local instance for `a = b` using the function being defined `auxFunName` + `(let inst := $(mkIdent auxFunName) @$a @$b; $rhs) + else + return rhs + + +def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Term := do + if indVal.numCtors ≥ deriving.decEq.linear_construction_threshold.get (← getOptions) then + mkMatchNew ctx header indVal + else + mkMatchOld ctx header indVal + def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): TermElabM (TSyntax `command) := do let header ← mkDecEqHeader indVal let body ← mkMatch ctx header indVal diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index f9baf10d89..b2db2a60a7 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -197,6 +197,7 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : mkLambdaFVars xs (← loop belowForAlt altBody) pure { matcherApp with alts := altsNew }.toExpr else + trace[Elab.definition.structural] "`matcherApp.addArg?` failed" processApp e | none => processApp e | e => diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean index 4c14babc63..7eada680c1 100644 --- a/src/Lean/Meta/Constructions.lean +++ b/src/Lean/Meta/Constructions.lean @@ -10,5 +10,6 @@ public import Lean.Meta.Constructions.CasesOn public import Lean.Meta.Constructions.NoConfusion public import Lean.Meta.Constructions.RecOn public import Lean.Meta.Constructions.BRecOn +public import Lean.Meta.Constructions.CasesOnSameCtor public section diff --git a/src/Lean/Meta/Constructions/CasesOnSameCtor.lean b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean new file mode 100644 index 0000000000..b3f2f74c23 --- /dev/null +++ b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean @@ -0,0 +1,248 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +module + +prelude +public import Lean.Meta.Basic +import Lean.AddDecl +import Lean.Meta.AppBuilder +import Lean.Meta.CompletionName +import Lean.Meta.Constructions.CtorIdx +import Lean.Meta.Constructions.CtorElim +import Lean.Elab.App + +/-! +See `mkCasesOnSameCtor` below. +-/ + +namespace Lean + +open Meta + +/-- +Helper for `mkCasesOnSameCtor` that constructs a heterogenous matcher (indices may differ) +and does not include the equality proof in the motive (so it's not a the shape of a matcher) yet. +-/ +public def mkCasesOnSameCtorHet (declName : Name) (indName : Name) : MetaM Unit := do + let ConstantInfo.inductInfo info ← getConstInfo indName | unreachable! + let casesOnName := mkCasesOnName indName + let casesOnInfo ← getConstVal casesOnName + let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`" + let e ← forallBoundedTelescope casesOnInfo.type info.numParams fun params t => + forallBoundedTelescope t (some 1) fun _ t => -- ignore motive + forallBoundedTelescope t (some (info.numIndices + 1)) fun ism1 _ => + forallBoundedTelescope t (some (info.numIndices + 1)) fun ism2 _ => do + let motiveType ← mkForallFVars (ism1 ++ ism2) (mkSort v) + withLocalDecl `motive .implicit motiveType fun motive => do + + let altTypes ← info.ctors.toArray.mapIdxM fun i ctorName => do + let ctor := mkAppN (mkConst ctorName us) params + let ctorType ← inferType ctor + forallTelescope ctorType fun zs1 ctorRet1 => do + let ctorApp1 := mkAppN ctor zs1 + let ctorRet1 ← whnf ctorRet1 + let is1 : Array Expr := ctorRet1.getAppArgs[info.numParams:] + let ism1 := is1.push ctorApp1 + forallTelescope ctorType fun zs2 ctorRet2 => do + let ctorApp2 := mkAppN ctor zs2 + let ctorRet2 ← whnf ctorRet2 + let is2 : Array Expr := ctorRet2.getAppArgs[info.numParams:] + let ism2 := is2.push ctorApp2 + let e := mkAppN motive (ism1 ++ ism2) + let e ← mkForallFVars (zs1 ++ zs2) e + let name := match ctorName with + | Name.str _ s => Name.mkSimple s + | _ => Name.mkSimple s!"alt{i+1}" + return (name, e) + withLocalDeclsDND altTypes fun alts => do + + let ctorApp1 := mkAppN (mkConst (mkCtorIdxName indName) us) (params ++ ism1) + let ctorApp2 := mkAppN (mkConst (mkCtorIdxName indName) us) (params ++ ism2) + let heqType ← mkEq ctorApp1 ctorApp2 + let heqType' ← mkEq ctorApp2 ctorApp1 + withLocalDeclD `h heqType fun heq => do + let motive1 ← mkLambdaFVars ism1 (← mkArrow heqType' (mkAppN motive (ism1 ++ ism2))) + let e := mkConst casesOnInfo.name (v :: us) + let e := mkAppN e params + let e := mkApp e motive1 + let e := mkAppN e ism1 + let alts1 ← info.ctors.toArray.mapIdxM fun i ctorName => do + let ctor := mkAppN (mkConst ctorName us) params + let ctorType ← inferType ctor + forallTelescope ctorType fun zs1 ctorRet1 => do + let ctorApp1 := mkAppN ctor zs1 + let ctorRet1 ← whnf ctorRet1 + let is1 : Array Expr := ctorRet1.getAppArgs[info.numParams:] + let ism1 := is1.push ctorApp1 + -- Here we let the typecheker reduce the `ctorIdx` application + let heq := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat) ctorApp2 (mkRawNatLit i) + withLocalDeclD `h heq fun h => do + let motive2 ← mkLambdaFVars ism2 (mkAppN motive (ism1 ++ ism2)) + let alt ← forallTelescope ctorType fun zs2 _ => do + mkLambdaFVars zs2 <| mkAppN alts[i]! (zs1 ++ zs2) + let e := if info.numCtors = 1 then + let casesOn := mkConst (mkCasesOnName indName) (v :: us) + mkAppN casesOn (params ++ #[motive2] ++ ism2 ++ #[alt]) + else + let casesOn := mkConst (mkConstructorElimName indName ctorName) (v :: us) + mkAppN casesOn (params ++ #[motive2] ++ ism2 ++ #[h, alt]) + mkLambdaFVars (zs1.push h) e + let e := mkAppN e alts1 + let e := mkApp e (← mkEqSymm heq) + mkLambdaFVars (params ++ #[motive] ++ ism1 ++ ism2 ++ #[heq] ++ alts) e + + addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe + (name := declName) + (levelParams := casesOnInfo.levelParams) + (type := (← inferType e)) + (value := e) + (hints := ReducibilityHints.abbrev) + )) + modifyEnv fun env => markAuxRecursor env declName + modifyEnv fun env => addToCompletionBlackList env declName + modifyEnv fun env => addProtected env declName + Elab.Term.elabAsElim.setTag declName + setReducibleAttribute declName + +def withSharedIndices (ctor : Expr) (k : Array Expr → Expr → Expr → MetaM α) : MetaM α := do + let ctorType ← inferType ctor + forallTelescopeReducing ctorType fun zs ctorRet => do + let ctor1 := mkAppN ctor zs + let rec go ctor2 todo acc := do + match todo with + | [] => k acc ctor1 ctor2 + | z::todo' => + if ctorRet.containsFVar z.fvarId! then + go (mkApp ctor2 z) todo' acc + else + let t ← whnfForall (← inferType ctor2) + assert! t.isForall + withLocalDeclD t.bindingName! t.bindingDomain! fun z' => do + go (mkApp ctor2 z') todo' (acc.push z') + go ctor zs.toList zs + +/-- +This constructs a matcher for a match statement that matches on the constructors of +a data type in parallel. So if `h : x1.ctorIdx = x2.ctorIdx`, then it implements +``` +match x1, x2, h with +| ctor1 .. , ctor1 .. , _ => ... +| ctor2 .. , ctor2 .. , _ => ... +``` +The normal matcher supports such matches, but implements them using nested `casesOn`, which +leads to a quadratic blow-up. This function uses the per-constructor eliminators to implement this +more efficiently. + +This is useful for implementing or deriving functionality like `BEq`, `DecidableEq`, `Ord` and +proving their lawfulness. + +One could imagine a future where `match` compilation is smart enough to do that automatically; then +this module can be dropped. + +Note that for some data types where the indices determine the constructor (e.g. `Vec`), this leads +to less efficient code than the normal matcher, as this needs to read the constructor tag on both +arguments, wheras the normal matcher produces code that reads just the first argument’s tag, and +then boldly reads the second argument’s fields. +-/ +public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit := do + let ConstantInfo.inductInfo info ← getConstInfo indName | unreachable! + + let casesOnSameCtorHet := declName ++ `het + mkCasesOnSameCtorHet casesOnSameCtorHet indName + let casesOnName := mkCasesOnName indName + let casesOnInfo ← getConstVal casesOnName + let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`" + forallBoundedTelescope casesOnInfo.type info.numParams fun params t => + let t0 := t.bindingBody! -- ignore motive + forallBoundedTelescope t0 (some info.numIndices) fun is t => + forallBoundedTelescope t (some 1) fun x1 _ => + forallBoundedTelescope t (some 1) fun x2 _ => do + let x1 := x1[0]! + let x2 := x2[0]! + let ctorApp1 := mkAppN (mkConst (mkCtorIdxName indName) us) (params ++ is ++ #[x1]) + let ctorApp2 := mkAppN (mkConst (mkCtorIdxName indName) us) (params ++ is ++ #[x2]) + let heqType ← mkEq ctorApp1 ctorApp2 + withLocalDeclD `h heqType fun heq => do + let motiveType ← mkForallFVars (is ++ #[x1,x2,heq]) (mkSort v) + withLocalDecl `motive .implicit motiveType fun motive => do + + let altTypes ← info.ctors.toArray.mapIdxM fun i ctorName => do + let ctor := mkAppN (mkConst ctorName us) params + withSharedIndices ctor fun zs12 ctorApp1 ctorApp2 => do + let ctorRet1 ← whnf (← inferType ctorApp1) + let is : Array Expr := ctorRet1.getAppArgs[info.numParams:] + let e := mkAppN motive (is ++ #[ctorApp1, ctorApp2, (← mkEqRefl (mkNatLit i))]) + let e ← mkForallFVars zs12 e + let name := match ctorName with + | Name.str _ s => Name.mkSimple s + | _ => Name.mkSimple s!"alt{i+1}" + return (name, e) + withLocalDeclsDND altTypes fun alts => do + forallBoundedTelescope t0 (some (info.numIndices + 1)) fun ism1' _ => + forallBoundedTelescope t0 (some (info.numIndices + 1)) fun ism2' _ => do + let (motive', newRefls) ← + withNewEqs (is.push x1) ism1' fun newEqs1 newRefls1 => do + withNewEqs (is.push x2) ism2' fun newEqs2 newRefls2 => do + let motive' := mkAppN motive (is ++ #[x1, x2, heq]) + let motive' ← mkForallFVars (newEqs1 ++ newEqs2) motive' + let motive' ← mkLambdaFVars (ism1' ++ ism2') motive' + return (motive', newRefls1 ++ newRefls2) + let casesOn2 := mkConst casesOnSameCtorHet (v :: us) + let casesOn2 := mkAppN casesOn2 params + let casesOn2 := mkApp casesOn2 motive' + let casesOn2 := mkAppN casesOn2 (is ++ #[x1] ++ is ++ #[x2]) + let casesOn2 := mkApp casesOn2 heq + let altTypes' ← inferArgumentTypesN info.numCtors casesOn2 + let alts' ← info.ctors.toArray.mapIdxM fun i ctorName => do + let ctor := mkAppN (mkConst ctorName us) params + let ctorType ← inferType ctor + forallTelescope ctorType fun zs1 _ctorRet1 => do + forallTelescope ctorType fun zs2 _ctorRet2 => do + let altType ← instantiateForall altTypes'[i]! (zs1 ++ zs2) + let alt ← mkFreshExprSyntheticOpaqueMVar altType + let goal := alt.mvarId! + let some (goal, _) ← Cases.unifyEqs? newRefls.size goal {} + | throwError "unifyEqns? unexpectedly closed goal" + let [] ← goal.apply alts[i]! + | throwError "could not apply {alts[i]!} to close\n{goal}" + mkLambdaFVars (zs1 ++ zs2) (← instantiateMVars alt) + let casesOn2 := mkAppN casesOn2 alts' + let casesOn2 := mkAppN casesOn2 newRefls + let e ← mkLambdaFVars (params ++ #[motive] ++ is ++ #[x1,x2] ++ #[heq] ++ alts) casesOn2 + + let decl := .defnDecl (← mkDefinitionValInferringUnsafe + (name := declName) + (levelParams := casesOnInfo.levelParams) + (type := (← inferType e)) + (value := e) + (hints := ReducibilityHints.abbrev) + ) + let matcherInfo : MatcherInfo := { + numParams := info.numParams + numDiscrs := info.numIndices + 3 + altNumParams := altTypes.map (·.2.getNumHeadForalls) + uElimPos? := some 0 + discrInfos := #[{}, {}, {}]} + + -- Compare attributes with `mkMatcherAuxDefinition` + addDecl decl + Elab.Term.elabAsElim.setTag declName + 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 + + +end Lean diff --git a/tests/lean/decEqMutualInductives.lean b/tests/lean/decEqMutualInductives.lean index fbe0af7e91..2bff0e297f 100644 --- a/tests/lean/decEqMutualInductives.lean +++ b/tests/lean/decEqMutualInductives.lean @@ -3,25 +3,58 @@ -- Print the generated derivations set_option trace.Elab.Deriving.decEq true +namespace A +set_option deriving.decEq.linear_construction_threshold 1000 + mutual -inductive Tree : Type := +inductive Tree : Type where | node : ListTree → Tree -inductive ListTree : Type := +inductive ListTree : Type where | nil : ListTree | cons : Tree → ListTree → ListTree deriving DecidableEq end mutual -inductive Foo₁ : Type := +inductive Foo₁ : Type where | foo₁₁ : Foo₁ | foo₁₂ : Foo₂ → Foo₁ deriving DecidableEq -inductive Foo₂ : Type := +inductive Foo₂ : Type where | foo₂ : Foo₃ → Foo₂ -inductive Foo₃ : Type := +inductive Foo₃ : Type where | foo₃ : Foo₁ → Foo₃ end + +end A + +namespace B +set_option deriving.decEq.linear_construction_threshold 0 + +mutual +inductive Tree : Type where + | node : ListTree → Tree + +inductive ListTree : Type where + | nil : ListTree + | cons : Tree → ListTree → ListTree + deriving DecidableEq +end + +mutual +inductive Foo₁ : Type where + | foo₁₁ : Foo₁ + | foo₁₂ : Foo₂ → Foo₁ +deriving DecidableEq + +inductive Foo₂ : Type where + | foo₂ : Foo₃ → Foo₂ + +inductive Foo₃ : Type where + | foo₃ : Foo₁ → Foo₃ +end + +end B diff --git a/tests/lean/decEqMutualInductives.lean.expected.out b/tests/lean/decEqMutualInductives.lean.expected.out index 471759afd9..d8d0ec512e 100644 --- a/tests/lean/decEqMutualInductives.lean.expected.out +++ b/tests/lean/decEqMutualInductives.lean.expected.out @@ -1,18 +1,18 @@ [Elab.Deriving.decEq] [mutual - def decEqTree✝ (x✝ : @Tree✝) (x✝¹ : @Tree✝) : Decidable✝ (x✝ = x✝¹) := + def decEqTree✝ (x✝ : @A.Tree✝) (x✝¹ : @A.Tree✝) : Decidable✝ (x✝ = x✝¹) := match x✝, x✝¹ with - | @Tree.node a✝, @Tree.node b✝ => + | @A.Tree.node a✝, @A.Tree.node b✝ => let inst✝ := decEqListTree✝ @a✝ @b✝; if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝ else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption) termination_by structural x✝ - def decEqListTree✝ (x✝² : @ListTree✝) (x✝³ : @ListTree✝) : Decidable✝ (x✝² = x✝³) := + def decEqListTree✝ (x✝² : @A.ListTree✝) (x✝³ : @A.ListTree✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with - | @ListTree.nil, @ListTree.nil => isTrue✝¹ rfl✝¹ - | ListTree.nil .., ListTree.cons .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) - | ListTree.cons .., ListTree.nil .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) - | @ListTree.cons a✝¹ a✝², @ListTree.cons b✝¹ b✝² => + | @A.ListTree.nil, @A.ListTree.nil => isTrue✝¹ rfl✝¹ + | A.ListTree.nil .., A.ListTree.cons .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) + | A.ListTree.cons .., A.ListTree.nil .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) + | @A.ListTree.cons a✝¹ a✝², @A.ListTree.cons b✝¹ b✝² => let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹; if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact @@ -22,34 +22,87 @@ else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption) termination_by structural x✝² end, - instance : DecidableEq✝ (@ListTree✝) := + instance : DecidableEq✝ (@A.ListTree✝) := decEqListTree✝] [Elab.Deriving.decEq] [mutual - def decEqFoo₁✝ (x✝ : @Foo₁✝) (x✝¹ : @Foo₁✝) : Decidable✝ (x✝ = x✝¹) := + def decEqFoo₁✝ (x✝ : @A.Foo₁✝) (x✝¹ : @A.Foo₁✝) : Decidable✝ (x✝ = x✝¹) := match x✝, x✝¹ with - | @Foo₁.foo₁₁, @Foo₁.foo₁₁ => isTrue✝ rfl✝ - | Foo₁.foo₁₁ .., Foo₁.foo₁₂ .. => isFalse✝ (by intro h✝; injection h✝) - | Foo₁.foo₁₂ .., Foo₁.foo₁₁ .. => isFalse✝ (by intro h✝; injection h✝) - | @Foo₁.foo₁₂ a✝, @Foo₁.foo₁₂ b✝ => + | @A.Foo₁.foo₁₁, @A.Foo₁.foo₁₁ => isTrue✝ rfl✝ + | A.Foo₁.foo₁₁ .., A.Foo₁.foo₁₂ .. => isFalse✝ (by intro h✝; injection h✝) + | A.Foo₁.foo₁₂ .., A.Foo₁.foo₁₁ .. => isFalse✝ (by intro h✝; injection h✝) + | @A.Foo₁.foo₁₂ a✝, @A.Foo₁.foo₁₂ b✝ => let inst✝ := decEqFoo₂✝ @a✝ @b✝; if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹ else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption) termination_by structural x✝ - def decEqFoo₂✝ (x✝² : @Foo₂✝) (x✝³ : @Foo₂✝) : Decidable✝ (x✝² = x✝³) := + def decEqFoo₂✝ (x✝² : @A.Foo₂✝) (x✝³ : @A.Foo₂✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with - | @Foo₂.foo₂ a✝¹, @Foo₂.foo₂ b✝¹ => + | @A.Foo₂.foo₂ a✝¹, @A.Foo₂.foo₂ b✝¹ => let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹; if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝² else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption) termination_by structural x✝² - def decEqFoo₃✝ (x✝⁴ : @Foo₃✝) (x✝⁵ : @Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := + def decEqFoo₃✝ (x✝⁴ : @A.Foo₃✝) (x✝⁵ : @A.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := match x✝⁴, x✝⁵ with - | @Foo₃.foo₃ a✝², @Foo₃.foo₃ b✝² => + | @A.Foo₃.foo₃ a✝², @A.Foo₃.foo₃ b✝² => let inst✝² := decEqFoo₁✝ @a✝² @b✝²; if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³ else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption) termination_by structural x✝⁴ end, - instance : DecidableEq✝ (@Foo₁✝) := + instance : DecidableEq✝ (@A.Foo₁✝) := + decEqFoo₁✝] +[Elab.Deriving.decEq] + [mutual + def decEqTree✝ (x✝ : @B.Tree✝) (x✝¹ : @B.Tree✝) : Decidable✝ (x✝ = x✝¹) := + B.Tree.match_on_same_ctor✝ x✝ x✝¹ rfl✝ + @fun a✝ b✝ => + let inst✝ := decEqListTree✝ @a✝ @b✝; + if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝¹ + else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption) + termination_by structural x✝ + def decEqListTree✝ (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) := + if h✝¹ : B.ListTree.ctorIdx✝ x✝² = B.ListTree.ctorIdx✝ x✝³ then + B.ListTree.match_on_same_ctor✝ x✝² x✝³ h✝¹ (@fun => isTrue✝¹ rfl✝) + @fun a✝¹ a✝² b✝¹ b✝² => + let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹; + if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; + exact + let inst✝² := decEqListTree✝ @a✝² @b✝²; + if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝² + else isFalse✝¹ (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption) + else isFalse✝² (by intro n✝²; injection n✝²; apply h✝² _; assumption) + else isFalse✝³ (fun h'✝ => h✝¹ (congrArg✝ B.ListTree.ctorIdx✝ h'✝)) + termination_by structural x✝² + end, + instance : DecidableEq✝ (@B.ListTree✝) := + decEqListTree✝] +[Elab.Deriving.decEq] + [mutual + def decEqFoo₁✝ (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) := + if h✝ : B.Foo₁.ctorIdx✝ x✝ = B.Foo₁.ctorIdx✝ x✝¹ then + B.Foo₁.match_on_same_ctor✝ x✝ x✝¹ h✝ (@fun => isTrue✝ rfl✝) + @fun a✝ b✝ => + let inst✝ := decEqFoo₂✝ @a✝ @b✝; + if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹ + else isFalse✝ (by intro n✝; injection n✝; apply h✝¹ _; assumption) + else isFalse✝¹ (fun h'✝ => h✝ (congrArg✝ B.Foo₁.ctorIdx✝ h'✝)) + termination_by structural x✝ + def decEqFoo₂✝ (x✝² : @B.Foo₂✝) (x✝³ : @B.Foo₂✝) : Decidable✝ (x✝² = x✝³) := + B.Foo₂.match_on_same_ctor✝ x✝² x✝³ rfl✝ + @fun a✝¹ b✝¹ => + let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹; + if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝² + else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption) + termination_by structural x✝² + def decEqFoo₃✝ (x✝⁴ : @B.Foo₃✝) (x✝⁵ : @B.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := + B.Foo₃.match_on_same_ctor✝ x✝⁴ x✝⁵ rfl✝ + @fun a✝² b✝² => + let inst✝² := decEqFoo₁✝ @a✝² @b✝²; + if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³ + else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption) + termination_by structural x✝⁴ + end, + instance : DecidableEq✝ (@B.Foo₁✝) := decEqFoo₁✝] diff --git a/tests/lean/run/casesOnSameCtor.lean b/tests/lean/run/casesOnSameCtor.lean new file mode 100644 index 0000000000..c8700e0529 --- /dev/null +++ b/tests/lean/run/casesOnSameCtor.lean @@ -0,0 +1,162 @@ +import Lean + +/-! This tests and documents the constructions in CasesOnSameCtor. -/ + +open Lean Meta + +inductive Vec (α : Type u) : Nat → Type u + | nil : Vec α 0 + | cons : α → {n : Nat} → Vec α n → Vec α (n+1) + +namespace Vec + +-- set_option debug.skipKernelTC true +run_meta mkCasesOnSameCtor `Vec.match_on_same_ctor ``Vec + +/-- +info: Vec.match_on_same_ctor.het.{u_1, u} {α : Type u} {motive : {a : Nat} → Vec α a → {a : Nat} → Vec α a → Sort u_1} + {a✝ : Nat} (t : Vec α a✝) {a✝¹ : Nat} (t✝ : Vec α a✝¹) (h : t.ctorIdx = t✝.ctorIdx) (nil : motive nil nil) + (cons : + (a : α) → + {n : Nat} → (a_1 : Vec α n) → (a_2 : α) → {n_1 : Nat} → (a_3 : Vec α n_1) → motive (cons a a_1) (cons a_2 a_3)) : + motive t t✝ +-/ +#guard_msgs in +#check Vec.match_on_same_ctor.het + +/-- +info: Vec.match_on_same_ctor.{u_1, u} {α : Type u} + {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝) + (h : t.ctorIdx = t✝.ctorIdx) (nil : motive nil nil ⋯) + (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a_2 : α) → (a_3 : Vec α n) → motive (cons a a_1) (cons a_2 a_3) ⋯) : + motive t t✝ h +-/ +#guard_msgs in +#check Vec.match_on_same_ctor + +-- Splitter and equations are generated +/-- +info: Vec.match_on_same_ctor.splitter.{u_1, u} {α : Type u} + {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝) + (h : t.ctorIdx = t✝.ctorIdx) (h_1 : motive nil nil ⋯) + (h_2 : (a : α) → (n : Nat) → (a_1 : Vec α n) → (a_2 : α) → (a_3 : Vec α n) → motive (cons a a_1) (cons a_2 a_3) ⋯) : + motive t t✝ h +-/ +#guard_msgs in +#check Vec.match_on_same_ctor.splitter + +-- Since there is no overlap, the splitter is equal to the matcher +-- (I wonder if we should use this in general in MatchEq) +example : @Vec.match_on_same_ctor = @Vec.match_on_same_ctor.splitter := by rfl + +/-- +info: Vec.match_on_same_ctor.eq_2.{u_1, u} {α : Type u} + {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} (a✝ : α) (n : Nat) (a✝¹ : Vec α n) + (a✝² : α) (a✝³ : Vec α n) (nil : motive nil nil ⋯) + (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a_2 : α) → (a_3 : Vec α n) → motive (cons a a_1) (cons a_2 a_3) ⋯) : + (match n + 1, Vec.cons a✝ a✝¹, Vec.cons a✝² a✝³ with + | 0, Vec.nil, Vec.nil, ⋯ => nil + | n + 1, Vec.cons a a_1, Vec.cons a_2 a_3, ⋯ => cons a a_1 a_2 a_3) = + cons a✝ a✝¹ a✝² a✝³ +-/ +#guard_msgs in +#check Vec.match_on_same_ctor.eq_2 + +-- Recursion works + +-- set_option trace.split.debug true +-- set_option trace.split.failure true +-- set_option trace.Elab.definition.structural.eqns true + +def decEqVec {α} {a} [DecidableEq α] (x : @Vec α a) (x_1 : @Vec α a) : Decidable (x = x_1) := + if h : Vec.ctorIdx x = Vec.ctorIdx x_1 then + Vec.match_on_same_ctor x x_1 h (isTrue rfl) + @fun a_1 _ a_2 b b_1 => + if h_1 : @a_1 = @b then by + subst h_1 + exact + let inst := decEqVec @a_2 @b_1; + if h_2 : @a_2 = @b_1 then by subst h_2; exact isTrue rfl + else isFalse (by intro n; injection n; apply h_2 _; assumption) + else isFalse (by intro n_1; injection n_1; apply h_1 _; assumption) + else isFalse (fun h' => h (congrArg Vec.ctorIdx h')) +termination_by structural x + + +-- Equation generation and pretty match syntax: + +/-- +info: theorem Vec.decEqVec.eq_def.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : DecidableEq α] (x x_1 : Vec α a), + x.decEqVec x_1 = + if h : x.ctorIdx = x_1.ctorIdx then + match a, x, x_1 with + | 0, Vec.nil, Vec.nil, ⋯ => isTrue ⋯ + | x + 1, Vec.cons a_1 a_2, Vec.cons b b_1, ⋯ => + if h_1 : a_1 = b then + h_1 ▸ + have inst_1 := a_2.decEqVec b_1; + if h_2 : a_2 = b_1 then + h_2 ▸ + have inst := a_2.decEqVec a_2; + isTrue ⋯ + else isFalse ⋯ + else isFalse ⋯ + else isFalse ⋯ +-/ +#guard_msgs(pass trace, all) in +#print sig decEqVec.eq_def + + +-- Incidentially, normal match syntax is able to produce an equivalent matcher +-- (with different implementation): +-- (see #10195 for problems with equation generation) + +def decEqVecPlain {α} {a} [DecidableEq α] (x : @Vec α a) (x_1 : @Vec α a) : Decidable (x = x_1) := + if h : Vec.ctorIdx x = Vec.ctorIdx x_1 then + match x, x_1, h with + | Vec.nil, Vec.nil, _ => isTrue rfl + | Vec.cons a_1 a_2, Vec.cons b b_1, _ => + if h_1 : @a_1 = @b then by + subst h_1 + exact + let inst := decEqVecPlain @a_2 @b_1; + if h_2 : @a_2 = @b_1 then by subst h_2; exact isTrue rfl + else isFalse (by intro n; injection n; apply h_2 _; assumption) + else isFalse (by intro n_1; injection n_1; apply h_1 _; assumption) + else isFalse (fun h' => h (congrArg Vec.ctorIdx h')) +termination_by structural x +end Vec + +namespace List +-- set_option debug.skipKernelTC true +-- set_option trace.compiler.ir.result true + +run_meta mkCasesOnSameCtor `List.match_on_same_ctor ``List + +/-- +info: List.match_on_same_ctor.{u_1, u} {α : Type u} {motive : (t t_1 : List α) → t.ctorIdx = t_1.ctorIdx → Sort u_1} + (t t✝ : List α) (h : t.ctorIdx = t✝.ctorIdx) (nil : motive [] [] ⋯) + (cons : + (head : α) → (tail : List α) → (head_1 : α) → (tail_1 : List α) → motive (head :: tail) (head_1 :: tail_1) ⋯) : + motive t t✝ h +-/ +#guard_msgs in +#check List.match_on_same_ctor + +end List + +namespace BadIdx +opaque f : Nat → Nat +inductive T : (n : Nat) → Type where + | mk1 : Fin n → T (f n) + | mk2 : Fin (2*n) → T (f n) + +run_meta mkCasesOnSameCtorHet `BadIdx.casesOn2Het ``T +/-- +error: Dependent elimination failed: Failed to solve equation + f n✝ = f n +-/ +#guard_msgs in +run_meta mkCasesOnSameCtor `BadIdx.casesOn2 ``T + +end BadIdx diff --git a/tests/lean/run/decEqNonInjIndex.lean b/tests/lean/run/decEqNonInjIndex.lean new file mode 100644 index 0000000000..7e04632c6a --- /dev/null +++ b/tests/lean/run/decEqNonInjIndex.lean @@ -0,0 +1,58 @@ +/-! +This test checks what deriving `DecidableEq` does when the inductive type has +non-injective indices, and just how bad the error messages are. +-/ + +opaque f : Nat → Nat + +set_option deriving.decEq.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 +-/ +#guard_msgs(pass trace, all) in +inductive T : (n : Nat) → Type where + | mk1 : Fin n → T (f n) + | mk2 : Fin (2*n) → T (f n) +deriving BEq, DecidableEq + + +set_option deriving.decEq.linear_construction_threshold 10000 + +/-- +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: 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 +-/ +#guard_msgs(pass trace, all) in +inductive T' : (n : Nat) → Type where + | mk1 : Fin n → T' (f n) + | mk2 : Fin (2*n) → T' (f n) +deriving BEq, DecidableEq diff --git a/tests/lean/run/linearDecEq.lean b/tests/lean/run/linearDecEq.lean new file mode 100644 index 0000000000..1c8cab7535 --- /dev/null +++ b/tests/lean/run/linearDecEq.lean @@ -0,0 +1,39 @@ +/-! +Tests for deriving decidable equality using the linear-size parallel match construction that takes +`x1.ctorIdx = x2.ctorIdx` as assumption. +-/ + +-- We always want to use the new construction in this test +set_option deriving.decEq.linear_construction_threshold 0 + +inductive EmptyType : Type +deriving DecidableEq + +structure SimpleStruct where + field : Bool +deriving DecidableEq + +inductive DependentStruct1 : Nat → Type where + | mk (n : Nat) (x : Fin n): DependentStruct1 n +deriving DecidableEq + +/-- +error: Dependent elimination failed: Failed to solve equation + Decidable.rec (fun h => (fun x => 1) h) (fun h => (fun x => 0) h) (instDecidableEqBool b✝ true) = + Decidable.rec (fun h => (fun x => 1) h) (fun h => (fun x => 0) h) (instDecidableEqBool b true) +-/ +#guard_msgs in +inductive DependentStruct2 : Nat → Type where + | mk (b : Bool) : DependentStruct2 (if b then 0 else 1) +deriving DecidableEq + +inductive Vec (α : Type u) : Nat → Type u + | nil : Vec α 0 + | cons : α → {n : Nat} → Vec α n → Vec α (n+1) +deriving DecidableEq + +inductive Test (α : Type) + | mk₀ + | mk₁ : (n : Nat) → (α × α) → List α → Vec α n → Test α + | mk₂ : Test α → α → Test α +deriving DecidableEq diff --git a/tests/lean/run/match_ctorIdx.lean b/tests/lean/run/match_ctorIdx.lean new file mode 100644 index 0000000000..1e27012f15 --- /dev/null +++ b/tests/lean/run/match_ctorIdx.lean @@ -0,0 +1,5 @@ +def test1 (x1 x2 : List α) (h : x2.ctorIdx = x1.ctorIdx) : Bool := + match x1, x2, h with + | .nil, .nil, _h => true + | .cons _h1 _t1, .cons _h2 _t2, _h => false + -- NB: This is a complete pattern match diff --git a/tests/playground/noConfusionDecEqExp.lean b/tests/playground/noConfusionDecEqExp.lean index 62263893d1..5fac2b32c5 100644 --- a/tests/playground/noConfusionDecEqExp.lean +++ b/tests/playground/noConfusionDecEqExp.lean @@ -5,13 +5,6 @@ inductive Foo (α : Type u) where | mk4 (val : String) | mk5 (head : α) (tail : Foo α) -def Foo.ctorIdx : Foo α → Nat - | .mk1 .. => 0 - | .mk2 .. => 1 - | .mk3 .. => 2 - | .mk4 .. => 3 - | .mk5 .. => 4 - @[elab_as_elim] def Foo.elimCtor1 {motive : Foo α → Sort v} (a : Foo α) (hIdx : a.ctorIdx == 0) (h : (val : α) → motive (Foo.mk1 val)) : motive a := match a with