Lean4
/-- Prove the traversable laws and derive `LawfulTraversable`. -/
def deriveLawfulTraversable (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 { failIfUnchanged := false, unfoldPartialApp := true } (simpTheorems := #[s])
let .app (.app (.const ``LawfulTraversable _) F) _ ← m.getType >>= instantiateMVars |
failure
let some n := F.getAppFn.constName? |
failure
let [mit, mct, mtmi, mn] ← m.applyConst ``LawfulTraversable.mk |
failure
let defEqns : MetaM Simp.Context := rules [] [.mkStr n "map", .mkStr n "traverse"] true
traversableLawStarter mit n defEqns fun _ _ m => m.refl
traversableLawStarter mct n defEqns fun _ _ m => do
if let (some (_, m), _)←
simpFunctorGoal m (← rules [] [.mkStr n "map", .mkStr n "traverse", ``Function.comp] true) then
m.refl
traversableLawStarter mtmi n defEqns fun _ _ m => do
if let (some (_, m), _)← simpGoal m (← rules [(``Traversable.traverse_eq_map_id', false)] [] false) then
m.refl
traversableLawStarter mn n defEqns fun _ _ m => do
if let (some (_, m), _)← simpGoal m (← rules [(``Traversable.naturality_pf, false)] [] false) then
m.refl
