égalité pour les éléments de type sig en Coq

Question

Avec un type de sig défintion comme:

Inductive A: Set := mkA : nat-> A. 
Function getId (a: A) : nat := match a with mkA n => n end. 
Function filter (a: A) : bool := if (beq_nat (getId a) 0) then true else false. 
Coercion is_true : bool >-> Sortclass. 
Definition subsetA : Set := { a : A | filter a }. 

J'essaie de prouver sa projection est injective:

Lemma projection_injective : 
    forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2. 
Proof. 
destruct t1. 
destruct t2. 
simpl. 
intros. 
rewrite -> H. (* <- stuck here *) 
Abort. 

À ce stade, Coq sait:

x : A 
i : is_true (filter x) 
x0 : A 
i0 : is_true (filter x0) 
H : x = x0 

J'ai essayé de réécrire sans succès. Par exemple, pourquoi ne puis-je pas réécrire i et H pour donner à Coq un i0? Puis-je demander ce qui m'a manqué ici? Merci.

Answer 1

Au moment où vous avez été coincé, votre objectif regardé à peu près comme ceci:

exist x i = exist x0 i0 

Si la réécriture que vous avez saisi devait réussir, vous auriez obtenu l'objectif suivant:

exist x0 i = exist x0 i0 

Ici, vous pouvez voir pourquoi Coq se plaint: la réécriture aurait donné un terme mal typé. Le problème est que le sous-terme exist x0 i utilise i comme un terme de type filter x0, lorsqu'il a vraiment le type filter x. Pour convaincre Coq que ce n'est pas un problème, vous devez masser votre objectif un peu avant la réécriture:

Lemma projection_injective : 
    forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2. 
Proof. 
destruct t1. 
destruct t2. 
simpl. 
intros. 
revert i. (* <- this is new *) 
rewrite -> H. (* and now the tactic succeeds *) 
intros i. 
Abort. 

Sinon, vous pouvez utiliser la tactique subst, qui essaie de supprimer toutes les variables redondantes dans le contexte. Voici une version plus compacte du script ci-dessus:

Lemma projection_injective : 
    forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2. 
Proof. 
    intros [x1 i1] [x2 i2]; simpl; intros e. 
    subst. 
Abort. 

Vous croiserez peut-être une autre question plus tard: montrant que deux termes de type filter x0 sont égaux. En général, vous auriez besoin de l'axiome de la non-pertinence de la preuve pour pouvoir le montrer; Cependant, étant donné que filter est défini comme une égalité entre deux termes d'un type à égalité décidable, vous pouvez prouver cette propriété en tant que théorème (ce que le Coq standard library fait déjà pour vous).

En remarque, la bibliothèque mathcomp a déjà un generic lemma qui subsume votre propriété, appelé val_inj. est une tactique qui est utile lorsque les types dépendants sont impliqués

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype. 

Inductive A: Set := mkA : nat-> A. 
Function getId (a: A) : nat := match a with mkA n => n end. 
Function filter (a: A) : bool := if (Nat.eqb (getId a) 0) then true else false. 
Definition subsetA : Set := { a : A | filter a }. 

Lemma projection_injective : 
    forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2. 
Proof. 
    intros t1 t2. 
    apply val_inj. 
Qed.