The Coq mailing list

[Jacek Chrząszcz <chrzaszcz AT mimuw.edu.pl>]

If you enter
Set Printing All.
Show.
Then you will see that (v1 (fin_zero n)) in your goal looks different
than "the same" term in H0 - some coercions between sig and sigT
slipped in. You have two choices:

1) reduce the coercions by proving and applying a quick lemma:

Lemma sigsigT : forall A (P:A->Prop) (s : sig P), sig_of_sigT
(sigT_of_sig s) = s.
  destruct s; trivial.
Qed.

now:

rewrite sigsigT in H0.

and your

rewrite H0.

works!


2) replace projT1 with proj1_sig in your definition aux3 and you will
have no coercions and rewrite H0 will just work!

Bests,

Jacek

2014-06-04 22:24 GMT+02:00 Ilmārs Cīrulis 
<ilmars.cirulis AT gmail.com>:
> Definition fin limit := {n | n <= limit}.
> Definition vect A limit := fin limit -> A.
>
> Definition fin_zero limit: fin limit.
>  exists O; induction limit; auto.
> Defined.
>
> Definition aux3 {n} (v1 v2: vect bool n):
>   (forall i, projT1 i <= O -> v1 i = false \/ v2 i = false) -> andb (v1
> (fin_zero n)) (v2 (fin_zero n)) = false.
>  intros. destruct (H (fin_zero n) (le_n O)).
>  rewrite H0.
>
> (* Error: Found no subterm matching "v1 (fin_zero n)" in the current goal.
> *)
> (* Goal: (v1 (fin_zero n) && v2 (fin_zero n))%bool = false *)
>