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

fix: ac_rfl in subgoal

Browse source 
Closes #1202
This commit is contained in:
pcpthm 2022-08-11 13:16:15 +09:00 • committed by Leonardo de Moura
parent dda1fd27c4
commit cbe9adbe9e
2 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/AC/Main.lean
View file

@ -145,7 +145,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
congrTheorems := (← getSimpCongrTheorems)
config := Simp.neutralConfig
}
let tgt ← mvarId.getType
let tgt ← instantiateMVars (← mvarId.getType)
let res ← Simp.main tgt simpCtx (methods := { post })
let newGoal ← applySimpResultToTarget mvarId tgt res
newGoal.refl

16
tests/lean/run/1202.lean Normal file
View file

@ -0,0 +1,16 @@
opaque f : Bool → Bool → Bool
axiom f_comm (a b : Bool) : f a b = f b a
axiom f_assoc (a b c : Bool) : f (f a b) c = f a (f b c)
instance : Lean.IsCommutative f := ⟨f_comm⟩
instance : Lean.IsAssociative f := ⟨f_assoc⟩
example (a b c : Bool) : f (f a b) c = f (f a c) b :=
by ac_rfl -- good
example (a b c : Bool) : (f (f a b) c = f (f a c) b) ∧ true :=
And.intro (by ac_rfl) rfl -- good
example (a b c : Bool) : (f (f a b) c = f (f a c) b) ∧ true := by
apply And.intro
. ac_rfl
. rfl