为何Coq无法识别`None = Some v`为假？证明问题咨询

我定义了如下递归函数：

Fixpoint eval (fuel : nat) (env : environment) (e : exp) := 
  match fuel with 
    | 0       => None 
    | S fuel' => (...)
  end

在证明该函数的性质时，当前有如下假设：

IHfuel : eval 0 env (IfThenElse e1 e2 e3) = Some v -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

执行simpl in IHfuel.策略后，假设变为：

IHfuel : None = Some v -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

我原以为None = Some v显然是False，因此这个蕴含式应该是trivially成立的，但Coq并不认可这一点。我尝试用destruct (Some v)策略，结果生成了两个目标：

第一个目标：

IHfuel : None = Some v0 -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

第二个目标：

IHfuel : None = None -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

我很困惑，为什么Some v会被拆分成Some v0和None？

问题解析 #

• Coq中option类型的构造子None和Some是不相交的，但默认不会自动识别这种矛盾，需要你手动触发相关策略。None = Some v本身是矛盾命题，蕴含式False -> P虽然永真，但Coq不会自动应用这个逻辑，得明确调用策略处理。
• 你用destruct (Some v)出现异常结果的原因是：destruct是对项的构造子做拆分，但Some v本身就是option的一个构造子实例，正确的操作应该针对等式None = Some v。比如使用discriminate IHfuel.策略——它专门处理构造子不相交导致的矛盾等式，能直接利用None和Some的互斥性，证明前提为假，从而让整个蕴含式成立，直接完成当前子目标；或者用inversion IHfuel.，它会深入分析等式的矛盾结构，同样能解决问题。

内容的提问来源于stack exchange，提问作者mell_o_tron