constructeurs Proving sont des fonctions partielles en Coq

Question

Avec une définition inductive comme:

Inductive A := 
mkA : nat -> A. 

constructeurs Proving sont des fonctions partielles peuvent être codées comme:

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

Bien qu'il soit trivial de prouver, le faire pour chaque type défini sonne bizarre.

Existe-t-il une tactique pour encoder cette propriété? Ou un équivalent dans une bibliothèque? Je n'ai rien trouvé dans ssreflect cependant en recherchant (_ <> _).

Answer 1

Vous pouvez indiquer un lemme générique qui subsume ce résultat pour chaque fonction Coq. Puisque les constructeurs comme votre mkA ne sont que des fonctions, le résultat s'applique à eux aussi.

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. 

Cette déclaration est en fait la contrapositive de la suivante de la bibliothèque standard.

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