Lean4
/-- Prove the functor laws and derive `LawfulFunctor`. -/
def deriveLawfulFunctor (m : MVarId) : TermElabM Unit := do
let rules (l₁ : List (Name × Bool)) (l₂ : List (Name)) (b : Bool) : MetaM Simp.Context := do
let mut s : SimpTheorems := { }
s ← l₁.foldlM (fun s (n, b) => s.addConst n (inv := b)) s
s ← l₂.foldlM (fun s n => s.addDeclToUnfold n) s
if b then
let hs ← getPropHyps
s ← hs.foldlM (fun s f => f.getDecl >>= fun d => s.add (.fvar f) #[] d.toExpr) s
Simp.mkContext (simpTheorems := #[s])
let .app (.app (.const ``LawfulFunctor _) F) _ ← m.getType >>= instantiateMVars |
failure
let some n := F.getAppFn.constName? |
failure
let [mcn, mim, mcm] ← m.applyConst ``LawfulFunctor.mk |
failure
let (_, mcn) ← mcn.introN 2
mcn.refl
let (#[_, x], mim) ← mim.introN 2 |
failure
let (some mim, _) ← dsimpGoal mim (← rules [] [``Functor.map] false) |
failure
let xs ← mim.induction x (mkRecName n)
xs.forM fun ⟨mim, _, _⟩ =>
mim.withContext do
if let (some (_, mim), _)← simpGoal mim (← rules [(``Functor.map_id, false)] [.mkStr n "map"] true) then
mim.refl
let (#[_, _, _, _, _, x], mcm) ← mcm.introN 6 |
failure
let (some mcm, _) ← dsimpGoal mcm (← rules [] [``Functor.map] false) |
failure
let xs ← mcm.induction x (mkRecName n)
xs.forM fun ⟨mcm, _, _⟩ =>
mcm.withContext do
if let (some (_, mcm), _)← simpGoal mcm (← rules [(``Functor.map_comp_map, true)] [.mkStr n "map"] true) then
mcm.refl
