The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-06-05 1:59 GMT+02:00 Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>:

I found such solution just now:

Definition aux3 {n} (v1 v2: vect bool n):

  (forall (i: fin n), 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.
(* Now it works! *)


I added type to variable "i". Now it's fin n or { n0: nat | n0 <= n}, and that's different from {n0 : nat & n0 <= n}. (sig and sigT)


Thank you,
Ilmars

On Thu, Jun 5, 2014 at 2:41 AM, Jacek Chrząszcz <chrzaszcz AT mimuw.edu.pl> wrote:

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 *)
>

--
.../Sedrikov\...