fix: igore instance implicit arguments in term ordering used at simp
closes #972
This commit is contained in:
Leonardo de Moura
parent
d4f7899591
commit
02677cf326
5 changed files with 188 additions and 115 deletions
161
src/Lean/Meta/ACLt.lean
Normal file
161
src/Lean/Meta/ACLt.lean
Normal file
|
|
@ -0,0 +1,161 @@
|
|||
/-
|
||||
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Meta.Basic
|
||||
import Lean.Meta.FunInfo
|
||||
|
||||
namespace Lean
|
||||
|
||||
def Expr.ctorWeight : Expr → UInt8
|
||||
| bvar .. => 0
|
||||
| fvar .. => 1
|
||||
| mvar .. => 2
|
||||
| sort .. => 3
|
||||
| const .. => 4
|
||||
| lit .. => 5
|
||||
| mdata .. => 6
|
||||
| proj .. => 7
|
||||
| app .. => 8
|
||||
| lam .. => 9
|
||||
| forallE .. => 10
|
||||
| letE .. => 11
|
||||
|
||||
namespace Meta
|
||||
namespace ACLt
|
||||
|
||||
mutual
|
||||
|
||||
/--
|
||||
An AC-compatible ordering.
|
||||
|
||||
Recall that an AC-compatible ordering if it is monotonic, well-founded, and total.
|
||||
Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of
|
||||
each expression in Lean 4. Even if we did, we would need to have a weight where implicit instace arguments are ignored.
|
||||
So, we use a LPO-like term ordering.
|
||||
|
||||
Remark: this method is used to implement ordered rewriting. We ignore implicit instance
|
||||
arguments to address an issue reported at issue #972.
|
||||
|
||||
Remark: the order is not really total on terms since
|
||||
- We instance implicit arguments.
|
||||
- We ignore metadata.
|
||||
- We ignore universe parameterst at constants.
|
||||
-/
|
||||
unsafe def lt (a b : Expr) : MetaM Bool :=
|
||||
if ptrAddrUnsafe a == ptrAddrUnsafe b then
|
||||
false
|
||||
-- We ignore metadata
|
||||
else if a.isMData then
|
||||
lt a.mdataExpr! b
|
||||
else if b.isMData then
|
||||
lt a b.mdataExpr!
|
||||
else
|
||||
lpo a b
|
||||
|
||||
where
|
||||
ltPair (a₁ a₂ b₁ b₂ : Expr) : MetaM Bool := do
|
||||
if (← lt a₁ b₁) then
|
||||
return true
|
||||
else if (← lt b₁ a₁) then
|
||||
return false
|
||||
else
|
||||
lt a₂ b₂
|
||||
|
||||
ltApp (a b : Expr) : MetaM Bool := do
|
||||
let aFn := a.getAppFn
|
||||
let bFn := b.getAppFn
|
||||
if (← lt aFn bFn) then
|
||||
return true
|
||||
else if (← lt bFn aFn) then
|
||||
return false
|
||||
else
|
||||
let aArgs := a.getAppArgs
|
||||
let bArgs := b.getAppArgs
|
||||
if aArgs.size < bArgs.size then
|
||||
return true
|
||||
else if aArgs.size > bArgs.size then
|
||||
return false
|
||||
else
|
||||
let infos := (← getFunInfoNArgs aFn aArgs.size).paramInfo
|
||||
for i in [:infos.size] do
|
||||
-- We ignore instance implicit arguments during comparison
|
||||
if !infos[i].isInstImplicit then
|
||||
if (← lt aArgs[i] bArgs[i]) then
|
||||
return true
|
||||
else if (← lt bArgs[i] aArgs[i]) then
|
||||
return false
|
||||
for i in [infos.size:aArgs.size] do
|
||||
if (← lt aArgs[i] bArgs[i]) then
|
||||
return true
|
||||
else if (← lt bArgs[i] aArgs[i]) then
|
||||
return false
|
||||
return false
|
||||
|
||||
lexSameCtor (a b : Expr) : MetaM Bool :=
|
||||
match a with
|
||||
-- Atomic
|
||||
| Expr.bvar i .. => i < b.bvarIdx!
|
||||
| Expr.fvar id .. => Name.quickLt id.name b.fvarId!.name
|
||||
| Expr.mvar id .. => Name.quickLt id.name b.mvarId!.name
|
||||
| Expr.sort u .. => Level.normLt u b.sortLevel!
|
||||
| Expr.const n .. => Name.quickLt n b.constName! -- We igore the levels
|
||||
| Expr.lit v .. => Literal.lt v b.litValue!
|
||||
-- Composite
|
||||
| Expr.proj _ i e .. => if i != b.projIdx! then i < b.projIdx! else lt e b.projExpr!
|
||||
| Expr.app .. => ltApp a b
|
||||
| Expr.lam _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
|
||||
| Expr.forallE _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
|
||||
| Expr.letE _ _ v e .. => ltPair v e b.letValue! b.letBody!
|
||||
-- See main function
|
||||
| Expr.mdata .. => unreachable!
|
||||
|
||||
lex (a b : Expr) : MetaM Bool :=
|
||||
if a.ctorWeight < b.ctorWeight then
|
||||
return true
|
||||
else if a.ctorWeight > b.ctorWeight then
|
||||
return false
|
||||
else
|
||||
lexSameCtor a b
|
||||
|
||||
allChildrenLt (a b : Expr) : MetaM Bool :=
|
||||
match a with
|
||||
| Expr.proj _ _ e .. => lt e b
|
||||
| Expr.app .. =>
|
||||
a.withApp fun f args => do
|
||||
let infos := (← getFunInfoNArgs f args.size).paramInfo
|
||||
for i in [:infos.size] do
|
||||
-- We ignore instance implicit arguments during comparison
|
||||
if !infos[i].isInstImplicit then
|
||||
if !(← lt args[i] b) then
|
||||
return false
|
||||
for i in [infos.size:args.size] do
|
||||
if !(← lt args[i] b) then
|
||||
return false
|
||||
return true
|
||||
| Expr.lam _ d e .. => lt d b <&&> lt e b
|
||||
| Expr.forallE _ d e .. => lt d b <&&> lt e b
|
||||
| Expr.letE _ _ v e .. => lt v b <&&> lt e b
|
||||
| _ => return true
|
||||
|
||||
someChildGe (a b : Expr) : MetaM Bool :=
|
||||
return !(← allChildrenLt a b)
|
||||
|
||||
-- lpo is only used when `a` and `b` have the same approximate depth, and it is >= 255
|
||||
lpo (a b : Expr) : MetaM Bool := do
|
||||
-- Case 1: `a < b` if for some child `b_i` of `b`, we have `b_i >= a`
|
||||
someChildGe b a
|
||||
-- Case 2: `a < b` if `a.ctorWeight < b.ctorWeight` and for all children `a_i` of `a`, `a_i < b`
|
||||
<||> (a.ctorWeight < b.ctorWeight <&&> allChildrenLt a b)
|
||||
-- Case 3: `a < b` if `a` & `b` have the same ctor, and `a` is lexicographically smaller
|
||||
<||> (a.ctorWeight == b.ctorWeight <&&> lexSameCtor a b)
|
||||
|
||||
end
|
||||
|
||||
end ACLt
|
||||
|
||||
@[implementedBy ACLt.lt]
|
||||
constant Expr.acLt : Expr → Expr → MetaM Bool
|
||||
|
||||
end Lean.Meta
|
||||
|
|
@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Util.ACLt
|
||||
import Lean.Meta.ACLt
|
||||
import Lean.Meta.AppBuilder
|
||||
import Lean.Meta.SynthInstance
|
||||
import Lean.Meta.Tactic.Simp.Types
|
||||
|
|
@ -55,9 +55,10 @@ private def tryLemmaCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo)
|
|||
let rhs ← instantiateMVars type.appArg!
|
||||
if e == rhs then
|
||||
return none
|
||||
if lemma.perm && !Expr.acLt rhs e then
|
||||
trace[Meta.Tactic.simp.rewrite] "{lemma}, perm rejected {e} ==> {rhs}"
|
||||
return none
|
||||
if lemma.perm then
|
||||
if !(← Expr.acLt rhs e) then
|
||||
trace[Meta.Tactic.simp.rewrite] "{lemma}, perm rejected {e} ==> {rhs}"
|
||||
return none
|
||||
trace[Meta.Tactic.simp.rewrite] "{lemma}, {e} ==> {rhs}"
|
||||
return some { expr := rhs, proof? := proof }
|
||||
else
|
||||
|
|
|
|||
|
|
@ -23,4 +23,3 @@ import Lean.Util.FoldConsts
|
|||
import Lean.Util.SCC
|
||||
import Lean.Util.OccursCheck
|
||||
import Lean.Util.Paths
|
||||
import Lean.Util.ACLt
|
||||
|
|
|
|||
|
|
@ -1,110 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Expr
|
||||
|
||||
namespace Lean
|
||||
|
||||
def Expr.ctorWeight : Expr → UInt8
|
||||
| bvar .. => 0
|
||||
| fvar .. => 1
|
||||
| mvar .. => 2
|
||||
| sort .. => 3
|
||||
| const .. => 4
|
||||
| lit .. => 5
|
||||
| mdata .. => 6
|
||||
| proj .. => 7
|
||||
| app .. => 8
|
||||
| lam .. => 9
|
||||
| forallE .. => 10
|
||||
| letE .. => 11
|
||||
|
||||
namespace ACLt
|
||||
|
||||
mutual
|
||||
|
||||
/--
|
||||
An AC-compatible ordering.
|
||||
|
||||
Recall that an AC-compatible ordering if it is monotonic, well-founded, and total.
|
||||
Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of
|
||||
each expression in Lean 4, only the approximated depth (it saturates at 255).
|
||||
Thus, we use a hybrid of KBO and LPO.
|
||||
-/
|
||||
unsafe def lt (a b : Expr) : Bool :=
|
||||
if ptrAddrUnsafe a == ptrAddrUnsafe b then
|
||||
false
|
||||
-- We ignore metadata
|
||||
else if a.isMData then
|
||||
lt a.mdataExpr! b
|
||||
else if b.isMData then
|
||||
lt a b.mdataExpr!
|
||||
else if a.approxDepth < b.approxDepth then
|
||||
true
|
||||
else if a.approxDepth > b.approxDepth then
|
||||
false
|
||||
else if a.approxDepth < 255 then
|
||||
lex a b
|
||||
else
|
||||
lpo a b
|
||||
where
|
||||
ltPair (a₁ a₂ b₁ b₂ : Expr) : Bool :=
|
||||
if a₁ != b₁ then lt a₁ b₁ else lt a₂ b₂
|
||||
|
||||
lexSameCtor (a b : Expr) : Bool :=
|
||||
match a with
|
||||
-- Atomic
|
||||
| Expr.bvar i .. => i < b.bvarIdx!
|
||||
| Expr.fvar id .. => Name.quickLt id.name b.fvarId!.name
|
||||
| Expr.mvar id .. => Name.quickLt id.name b.mvarId!.name
|
||||
| Expr.sort u .. => Level.normLt u b.sortLevel!
|
||||
| Expr.const n .. => Name.quickLt n b.constName! -- We igore the levels
|
||||
| Expr.lit v .. => Literal.lt v b.litValue!
|
||||
-- Composite
|
||||
| Expr.proj _ i e .. => if i != b.projIdx! then i < b.projIdx! else lt e b.projExpr!
|
||||
| Expr.app f e .. => ltPair f e b.appFn! b.appArg!
|
||||
| Expr.lam _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
|
||||
| Expr.forallE _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
|
||||
| Expr.letE _ _ v e .. => ltPair v e b.letValue! b.letBody!
|
||||
-- See main function
|
||||
| Expr.mdata .. => unreachable!
|
||||
|
||||
lex (a b : Expr) : Bool :=
|
||||
if a.ctorWeight < b.ctorWeight then
|
||||
true
|
||||
else if a.ctorWeight > b.ctorWeight then
|
||||
false
|
||||
else
|
||||
lexSameCtor a b
|
||||
|
||||
allChildrenLt (a b : Expr) : Bool :=
|
||||
match a with
|
||||
| Expr.proj _ _ e .. => lt e b
|
||||
| Expr.app f e .. => lt f b && lt e b
|
||||
| Expr.lam _ d e .. => lt d b && lt e b
|
||||
| Expr.forallE _ d e .. => lt d b && lt e b
|
||||
| Expr.letE _ _ v e .. => lt v b && lt e b
|
||||
| _ => unreachable!
|
||||
|
||||
someChildGe (a b : Expr) : Bool :=
|
||||
!allChildrenLt a b
|
||||
|
||||
-- lpo is only used when `a` and `b` have the same approximate depth, and it is >= 255
|
||||
lpo (a b : Expr) : Bool :=
|
||||
-- Case 1: `a < b` if for some child `b_i` of `b`, we have `b_i >= a`
|
||||
someChildGe b a
|
||||
-- Case 2: `a < b` if `a.ctorWeight < b.ctorWeight` and for all children `a_i` of `a`, `a_i < b`
|
||||
|| (a.ctorWeight < b.ctorWeight && allChildrenLt a b)
|
||||
-- Case 3: `a < b` if `a` & `b` have the same ctor, and `a` is lexicographically smaller
|
||||
|| (a.ctorWeight == b.ctorWeight && lexSameCtor a b)
|
||||
|
||||
end
|
||||
|
||||
end ACLt
|
||||
|
||||
@[implementedBy ACLt.lt]
|
||||
constant Expr.acLt : Expr → Expr → Bool
|
||||
|
||||
end Lean
|
||||
22
tests/lean/run/972.lean
Normal file
22
tests/lean/run/972.lean
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
class Semigroup (M : Type u) extends Mul M where
|
||||
mul_assoc (a b c : M) : (a * b) * c = a * (b * c)
|
||||
export Semigroup (mul_assoc)
|
||||
|
||||
class CommSemigroup (M : Type u) extends Semigroup M where
|
||||
mul_comm (a b : M) : a * b = b * a
|
||||
export CommSemigroup (mul_comm)
|
||||
|
||||
class Monoid (M : Type u) extends Semigroup M, OfNat M 1 where
|
||||
mul_one (m : M) : m * 1 = m
|
||||
one_mul (m : M) : 1 * m = m
|
||||
|
||||
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
|
||||
|
||||
theorem mul_left_comm {M} [CommSemigroup M] (a b c : M) : a * (b * c) = b * (a * c) := by
|
||||
rw [← mul_assoc, mul_comm a b, mul_assoc]
|
||||
|
||||
example {M} [CommMonoid M] (a b c d : M) : a * (b * (c * d)) = (a * c) * (b * d) := by
|
||||
simp only [mul_left_comm, mul_comm, mul_assoc]
|
||||
|
||||
example {M} [CommMonoid M] (a b c d : M) : (b * (c * d)) = (c) * (b * d) := by
|
||||
simp only [mul_left_comm, mul_comm, mul_assoc]
|
||||
Loading…
Add table
Reference in a new issue