証明コンストラクタは次のように誘導定義とCoqの

Question

で部分的な機能です：のためにそうすること、を証明するのは簡単ですが

Lemma constructor_functional : 
forall i1 i2, mkA i1 <> mkA i2 -> i1 <> i2. 

：

Inductive A := 
mkA : nat -> A. 

実証コンストラクタは、部分的な機能をとしてエンコードすることができていますすべての定義されたタイプは奇妙に聞こえる。

このプロパティをエンコードする方法はありますか？あるいは、図書館で同等のものがありますか？私は(_ <> _)を検索してssreflectで何も見つけられませんでした。

Answer 1

Coq関数ごとにこの結果を包含する総称補題を指定できます。 mkAのようなコンストラクタは単なる関数なので、その結果も同様に適用されます。

Lemma function_functional : 
    forall (X Y : Type) (f : X -> Y) (x1 x2 : X), 
    f x1 <> f x2 -> x1 <> x2. 
Proof. 
    intros X Y f x1 x2 H1 H2. 
    apply H1. 
    now rewrite H2. 
Qed. 

このステートメントは、実際には標準ライブラリの次のものと重複しません。

Lemma f_equal : 
    forall (X Y : Type) (f : X -> Y) (x1 x2 : X), 
    x1 = x2 -> f x1 = f x2.