Two question:

First how to prevent the following behaviour:

```
From Coq Require Import List.
From mathcomp Require Import all_ssreflect.
Goal forall A (a: A) b l, a <> b ->
In a (b :: l) ->
In a l.
Proof.
move => A a b l ab_neq [].
```

The second goal looks like this:

```
(fix In (a0 : A) (l0 : seq A) {struct l0} : Prop :=
match l0 with
| [::] => False
| b0 :: m => b0 = a0 \/ In a0 m
end) a l -> In a l
```

what I expected to see is

```
In a l -> In a l
```

My second question is is `In`

the predicate we are expected to use in ssreflect or is there ssreflect/mathcom version of it that we should use.

You should use membership, look at the header of the file `seq.v`

https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html

It is written `x \in l`

, and you have a lot of lemmas about it. It requires `A`

to be an `eqType`

since it tests (with a boolean test) the membership.

alright, a follow up question, I was using also `positive`

type from `PArith`

, but I didn't see trace of it in math comp, is there an alternative for this one as well ?

yes, but I don't recall where it is , @Cyril Cohen surely knows it.

I mean, the type `int`

of math-comp plays the role of `Z`

, and it is built using some notion of positive number

I don't recall if it is a custom one

OK, now I recall. For positive we use nat and a moral +1, see https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssrint.v#L68

The difference is that `positive`

from PArith are efficient in computations, less in reasoning. Do you need to run computations inside Coq?

I need to extract code with efficient computations.

I checked `int`

, it uses `nat`

, which is different from `positive`

, I actually need `positive`

because of it is binary representation.

and the fact that it started from one and not zero.

This is why we originally developped CoqEAL (cf https://github.com/coq-community/coqeal/blob/master/refinements/pos.v)

mmm, I was thinking of positive compatiable library, but thanks! I see that coqEAL will help with many cases, but in my case, I was implementing a data structure where I need to like match on binary bits of positive, I think I will have to stick PArith.

thanks a lot everyone

Cyril Cohen has marked this topic as resolved.

Last updated: Jul 25 2024 at 16:02 UTC