The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This particular confusion will be fixed in two ways in Coq 8.5.  First, proj1_sig (sig_of_sigT x) will unify with projT1 x, and projT1 (sigT_of_sig x) will unify with proj1_sig x (this is by a patch I submitted: https://coq.inria.fr/bugs/show_bug.cgi?id=3043).  Second, sigT_of_sig and sig_of_sigT will no longer be coercions.

-Jason

On Thu, Jun 5, 2014 at 9:59 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

(Sorry for the previous empty mail if it reached the coq mailing list)

Sometimes, I prefer to deal with types defined recursively rather than sigma types.

For instance, for your "fin" definition, I tend to prefer to use:

Inductive emptySet : Type := . (*Such a constant is already defined, but I am not sure of the case.*)

Fixpoint fin (n : nat) : Type :=
  option (match n with
             | O => emptySet
             | S n => option (fin n)
             end).

I do not pretend it to be better than the one you used, as it strongly depends on what you want to prove, and what libraries you want to use, but it has some nice properties:
→ The definition of fin_zero would become: "Definition fin_zero limit : fin limit := None." (or maybe "Definition fin_zero limit : fin limit := match limit with O => None | S _ => None end.")
→ Induction becomes easier as you do not have to destruct/reconstruct terms

An other way to define this type is through inductive types:

Inductive fin : nat -> Type :=
  | Last : forall n, fin n
  | Deeper : forall n, fin n -> fin (S n)
  .

But I find it often less convenient as you may need to do dependant induction, and inversions.

Here again, fin_zero is easy and readable to define: "Definition fin_zero limit : fin limit := Last limit."

2014-06-05 10:13 GMT+02:00 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\...

--
.../Sedrikov\...