Gleichheit für Elemente von sig Art in Coq

Question

Mit einem sig Typ defintion wie:

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 }. 

Ich versuche, seine Projektion zu beweisen injektiv:

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. 

An diesem Punkt weiß Coq:

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

Ich habe versucht, etwas ohne Erfolg umzuschreiben. Zum Beispiel, warum kann ich i und H nicht umschreiben, um Coq eine i0 zu geben? Darf ich fragen, was ich hier vermisse? Vielen Dank.

Answer 1

An dem Punkt, wo Sie stecken geblieben, sah Ihr Ziel in etwa wie folgt aus:

exist x i = exist x0 i0 

Wenn das Umschreiben Sie erfolgreich eingegeben, würden Sie das folgende Ziel haben erhalten:

exist x0 i = exist x0 i0 

Hier können Sie sehen, warum Coq sich beschwert: Das Umschreiben hätte einen schlecht typisierten Begriff ergeben. Das Problem ist, dass der Unterbegriff exist x0 ii als ein Ausdruck des Typs filter x0 verwendet, wenn es wirklich Typ filter x hat. Überzeugen Coq, dass dies kein Problem ist, müssen Sie Ihr Ziel ein wenig massieren, bevor Umschreiben:

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. 

Alternativ können Sie die subst Taktik verwenden, die alle redundanten Variablen im Kontext zu entfernen versucht. Hier ist eine kompaktere Version des obigen Skript:

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. 

Sie in ein anderes Problem führen könnte danach: zeigt, dass zwei Bedingungen des Typs filter x0 gleich sind. In der Regel benötigen Sie das Axiom der Beweis-Irrelevanz, um dies zeigen zu können; Da filter jedoch als eine Gleichheit zwischen zwei Termen eines Typs mit entscheidbarer Gleichheit definiert ist, können Sie diese Eigenschaft als einen Satz beweisen (was die Coq standard library bereits für Sie tut).

Als eine Randnotiz hat die mathcomp Bibliothek bereits eine generic lemma, die Ihre Eigenschaft, val_inj genannt, subsumiert. Nur um Ihnen ein Beispiel, das ist, wie man es verwenden könnte:

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.