/-- `deny` is the absorbing top: it wins on either side. -/ @[simp, grind =] theorem combine_deny_left (d : Decision) : combine .deny d = .deny := byd:Decision⊢ combine Decision.deny d = Decision.deny grindAll goals completed! 🐙 @[simp, grind =] theorem combine_deny_right (d : Decision) : combine d .deny = .deny := byd:Decision⊢ combine d Decision.deny = Decision.deny grindAll goals completed! 🐙 /-- `notApplicable` is the identity: silence on either side changes nothing. -/ @[simp, grind =] theorem combine_na_left (d : Decision) : combine .notApplicable d = d := byd:Decision⊢ combine Decision.notApplicable d = d cases dpermit⊢ combine Decision.notApplicable Decision.permit = Decision.permitdeny⊢ combine Decision.notApplicable Decision.deny = Decision.denynotApplicable⊢ combine Decision.notApplicable Decision.notApplicable = Decision.notApplicable <;>permit⊢ combine Decision.notApplicable Decision.permit = Decision.permitdeny⊢ combine Decision.notApplicable Decision.deny = Decision.denynotApplicable⊢ combine Decision.notApplicable Decision.notApplicable = Decision.notApplicable rflAll goals completed! 🐙 @[simp, grind =] theorem combine_na_right (d : Decision) : combine d .notApplicable = d := byd:Decision⊢ combine d Decision.notApplicable = d cases dpermit⊢ combine Decision.permit Decision.notApplicable = Decision.permitdeny⊢ combine Decision.deny Decision.notApplicable = Decision.denynotApplicable⊢ combine Decision.notApplicable Decision.notApplicable = Decision.notApplicable <;>permit⊢ combine Decision.permit Decision.notApplicable = Decision.permitdeny⊢ combine Decision.deny Decision.notApplicable = Decision.denynotApplicable⊢ combine Decision.notApplicable Decision.notApplicable = Decision.notApplicable rflAll goals completed! 🐙 @[simp, grind =] theorem denyOverrides_nil : denyOverrides [] = .notApplicable := rfl @[simp, grind =] theorem denyOverrides_cons (d : Decision) (rest : List Decision) : denyOverrides (d :: rest) = combine d (denyOverrides rest) := rfl @[simp, grind =] theorem denyOverrides_deny (rest : List Decision) : denyOverrides (.deny :: rest) = .deny := byrest:List Decision⊢ denyOverrides (Decision.deny :: rest) = Decision.deny grindAll goals completed! 🐙 /-- The headline behaviour of `notApplicable`: a silent vote at the head just disappears. This is *why* `optimize` is sound. -/ @[simp, grind =] theorem denyOverrides_na (rest : List Decision) : denyOverrides (.notApplicable :: rest) = denyOverrides rest := byrest:List Decision⊢ denyOverrides (Decision.notApplicable :: rest) = denyOverrides rest grindAll goals completed! 🐙