PropCoqのエビデンスなどについて混乱しています。それをどのように証明し(n = n) = (m = m)ますか？
私の意図は、これがどういうわけかであることを示すことですTrue=True。しかし、これは正しい定式化ですか？
私がこれまでに試したことは次のとおりです。
Theorem test: forall m n:nat, (n = n) = (m = m).
Proof. intros. simpl.
しかしsimpl.、何もしませreflexivityん。これは単なる例です。一般に、X可能であればどのタイプでもこれを証明する必要があります。
n = nとm = mはどちらもpropsitionであるため、 sortPropではなく sortSetです。これは基本的にn = n、 のようなものではなく、(証明する必要がある) ステートメントのようなものであることを意味しtrue : booleanます。
代わりに、次のようなものを証明してみることができます:または、与えられた自然を bool にマップするn-n = m-m関数を定義してから、 を証明することができます。nat_equal : nat -> boolnat_equal n = nat_equal m
ステートメントが等しいことを本当に主張したい場合は、命題拡張性が必要になります。
追加の公理を想定せずに、求めていることを証明することはできません。参照。この答え。