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

fix: preserve arrow binder names and info at simp

Browse source 
We use the idiom `revert; simp; ...; intro` in a few places. Some of
the reverted hypotheses manifest themselves as arrows in the target.
Before this commit, `simp` would lose the binder names and info when
simplifying an arrow, and we would get inaccessible names when
reintroducing them.
This commit is contained in:
Leonardo de Moura 2022-02-20 16:27:40 -08:00
parent 4ccab41819
commit 33b1d2fd98
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -45,8 +45,8 @@ def mkCongr (r₁ r₂ : Result) : MetaM Result :=
| none, some h => return { expr := e, proof? := (← Meta.mkCongrArg r₁.expr h) }
| some h₁, some h₂ => return { expr := e, proof? := (← Meta.mkCongr h₁ h₂) }
private def mkImpCongr (r₁ r₂ : Result) : MetaM Result := do
let e ← mkArrow r₁.expr r₂.expr
private def mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaM Result := do
let e := src.updateForallE! r₁.expr r₂.expr
match r₁.proof?, r₂.proof? with
| none, none => return { expr := e, proof? := none }
| _, _ => return { expr := e, proof? := (← Meta.mkImpCongr (← r₁.getProof) (← r₂.getProof)) } -- TODO specialize if bootleneck
@ -490,12 +490,12 @@ where
withSimpTheorems s do
let rq ← simp q
match rq.proof? with
| none => mkImpCongr rp rq
| none => mkImpCongr e rp rq
| some hq =>
let hq ← mkLambdaFVars #[h] hq
return { expr := (← mkArrow rp.expr rq.expr), proof? := (← mkImpCongrCtx (← rp.getProof) hq) }
return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← mkImpCongrCtx (← rp.getProof) hq) }
else
mkImpCongr rp (← simp q)
mkImpCongr e rp (← simp q)
simpForall (e : Expr) : M Result := withParent e do
trace[Debug.Meta.Tactic.simp] "forall {e}"