减少配以鉴于假设</p> <pre><code>H0 : n <> 0 </code></pre> <p>在COQ

Question

自然数条件如何减少术语

... 
if match n with 
    | 0 => false 
    | S m' => n =? m' 
    end 
then 
... 

在目标？

Answer 1

你也应该看看答案following question on destruct and case_eq

战术destruct n as [|p]将引领你在正确的方向。这将产生两个目标，一个与

H0 : 0 <> 0 
========== 
if false then ... 

一个与

H0 : S p <> 0 
========== 
    if n =? p then ... 

第一目标应该是可以解决的由case H0。