Equality for elements of sig type in Coq

With a sig type defintion like:

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

I try to prove its projection is 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.

At this point, Coq knows:

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

I tried some rewrite without success. For example, why can't I rewrite of i and H to give Coq a i0? May I ask what did I miss here? Thanks.

Solution

At the point where you got stuck, your goal looked roughly like this:

exist x i = exist x0 i0

If the rewrite you typed were to succeed, you would have obtained the following goal:

exist x0 i = exist x0 i0

Here, you can see why Coq is complaining: rewriting would have yielded an ill-typed term. The problem is that the subterm exist x0 i is using i as a term of type filter x0, when it really has type filter x. To convince Coq that this is not a problem, you need to massage your goal a little bit before rewriting:

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.

Alternatively, you could use the subst tactic, which tries to remove all redundant variables in the context. Here is a more compact version of the above script:

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.

You might run into another issue afterwards: showing that any two terms of type filter x0 are equal. In general, you would need the axiom of proof irrelevance to be able to show this; however, since filter is defined as an equality between two terms of a type with decidable equality, you can prove this property as a theorem (which the Coq standard library already does for you).

As a side note, the mathcomp library already has a generic lemma that subsumes your property, called val_inj. Just to give you an example, this is how one might use it:

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.