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.