max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: avoid unnecessary whnfs at unifyEqs

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-03 08:46:05 -08:00
parent cdd79ac170
commit 69abb0a35a
2 changed files with 31 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/Lean/Meta/Tactic/Cases.lean
View file

@ -222,33 +222,37 @@ partial def unifyEqs (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) : Meta
/- Skip equality -/
unifyEqs (numEqs - 1) (← clear mvarId eqFVarId) subst
else
let a' ← whnf a
let b' ← whnf b
if a' != a || b' != b then
/- Reduced lhs/rhs of current equality -/
let prf := mkFVar eqFVarId
let aEqb' ← mkEq a' b'
let mvarId ← assert mvarId eqDecl.userName aEqb' prf
let mvarId ← clear mvarId eqFVarId
unifyEqs numEqs mvarId subst
else
let substEq (symm : Bool) := do
/- TODO: support for acyclicity (e.g., `xs ≠ x :: xs`) -/
let (substNew, mvarId) ← substCore mvarId eqFVarId symm subst
unifyEqs (numEqs - 1) mvarId substNew
match a, b with
| Expr.fvar aFVarId _, Expr.fvar bFVarId _ =>
/- x = y -/
let aDecl ← getLocalDecl aFVarId
let bDecl ← getLocalDecl bFVarId
substEq (aDecl.index < bDecl.index)
| Expr.fvar .., _ => /- x = t -/ substEq (symm := false)
| _, Expr.fvar .. => /- t = x -/ substEq (symm := true)
| _, _ =>
/- t = s -/
let substEq (symm : Bool) := do
/- TODO: support for acyclicity (e.g., `xs ≠ x :: xs`) -/
let (substNew, mvarId) ← substCore mvarId eqFVarId symm subst
unifyEqs (numEqs - 1) mvarId substNew
match a, b with
| Expr.fvar aFVarId _, Expr.fvar bFVarId _ =>
/- x = y -/
let aDecl ← getLocalDecl aFVarId
let bDecl ← getLocalDecl bFVarId
substEq (aDecl.index < bDecl.index)
| Expr.fvar .., _ => /- x = t -/ substEq (symm := false)
| _, Expr.fvar .. => /- t = x -/ substEq (symm := true)
| _, _ =>
let env ← getEnv
if a.isConstructorApp env && b.isConstructorApp env then
/- ctor_i ... = ctor_j ... -/
match (← injectionCore mvarId eqFVarId) with
| InjectionResultCore.solved => pure none -- this alternative has been solved
| InjectionResultCore.subgoal mvarId numEqsNew => unifyEqs (numEqs - 1 + numEqsNew) mvarId subst
else
let a' ← whnf a
let b' ← whnf b
if a' != a || b' != b then
/- Reduced lhs/rhs of current equality -/
let prf := mkFVar eqFVarId
let aEqb' ← mkEq a' b'
let mvarId ← assert mvarId eqDecl.userName aEqb' prf
let mvarId ← clear mvarId eqFVarId
unifyEqs numEqs mvarId subst
else
throwError! "dependent elimination failed, stuck at auxiliary equation{eqDecl.type}"
private def unifyCasesEqs (numEqs : Nat) (subgoals : Array CasesSubgoal) : MetaM (Array CasesSubgoal) :=
subgoals.foldlM (init := #[]) fun subgoals s => do

3
src/Lean/Util/Recognizers.lean
View file

@ -79,6 +79,9 @@ def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal :=
| none => none
| _ => none
def isConstructorApp (env : Environment) (e : Expr) : Bool :=
e.isConstructorApp? env $.isSome
def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × Array Expr) :=
match e with
| Expr.lit (Literal.natVal n) _ =>