@[simp, grind .] theorem optimize_equiv (p : Policy) (req : Request) : evaluate (optimize p) req = evaluate p req := byp:Policyreq:Request⊢ evaluate (optimize p) req = evaluate p req simp only [evaluate, optimize]p:Policyreq:Request⊢ denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) (List.filter (fun rule => rule.outcome != Decision.notApplicable) p)) = denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) p) induction p with | nil =>nilreq:Request⊢ denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) (List.filter (fun rule => rule.outcome != Decision.notApplicable) [])) = denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) []) rflAll goals completed! 🐙 | cons rule rest ih =>consreq:Requestrule:Rulerest:List Ruleih:denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) (List.filter (fun rule => rule.outcome != Decision.notApplicable) rest)) = denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) rest)⊢ denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) (List.filter (fun rule => rule.outcome != Decision.notApplicable) (rule :: rest))) = denyOverrides (List.filterMap (fun rule => if rule.equivalent req = true then some rule.outcome else none) (rule :: rest)) grindAll goals completed! 🐙