从自然转化为不等于

Question

我有函数，其输出是一些自然数。我证明了一个引理，该函数的输出不能为零。这意味着输出等于某个自然数S m。我想转换上述引理。

Theorem greater:forall (m :nat)(l:list nat),
 m=?0=false ->
 0=? (f1 + m)=false-> 
 (f1 + m)= S m.

Answer 1

您输入的语句不输入校验。无论如何，我看不出它如何保持-例如，如果用l表示f1 : nat，则该语句将暗示3 = 2。

Require Import Coq.Arith.Arith.

Theorem greater:forall (m :nat)(f1:nat),
 m=?0=false ->
 0=? (f1 + m)=false->
 (f1 + m)= S m.
Admitted.

Lemma contra : False.
Proof.
pose proof (greater 1 2 eq_refl eq_refl).
easy.
Qed.

证明不为零的东西可以作为后继者：

Require Import Coq.Arith.Arith.

Lemma not_zero_succ :
  forall n, n <> 0 ->
  exists m, n = S m.
Proof. destruct n as [|n]; eauto; easy. Qed.