蕴涵律实战：约束从IF...THEN...到SQL CHECK的映射

[[逻辑蕴涵的形式化本质与自然语言直觉的偏离]]和[[表达式变换法则工具箱]]的 最基础应用：约束”红色零件必须存放在London”，形式化为IF COLOR='Red' THEN CITY='London'，SQL没有直接的IF…THEN…语法，用蕴涵律改写为 (NOT(COLOR='Red'))OR(CITY='London')，进一步用NOT(a=b)等价于a<>b 化简、去掉多余括号，得到可以直接作为基表CHECK约束书写的形式 CHECK(COLOR<>'Red' OR CITY='London')。这条变换有一个更一般的通用配方： 逻辑蕴涵IF p THEN q也可以直接映射到SQL的CASE表达式 CASE WHEN p' THEN q' ELSE TRUE END（p’、q’是p、q各自的SQL对应写法）—— 两条路径（蕴涵律改写成OR，或CASE表达式）殊途同归，都能把”若p则q”这种SQL 原生不支持的结构转换成合法SQL；ELSE TRUE这个分支不能省略，因为 CASE WHEN p' THEN q' END在p’为假时默认落到隐式的ELSE NULL分支（呼应 [[避免null的实践规则NOT_NULL约束与COALESCE]]中CASE表达式若省略ELSE分支 的隐患），而蕴涵在前件为假时理应恒为真，用NULL替代TRUE会破坏这条语义。