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