Stream: math-comp users

Topic: ssreflect unfold In but I don't want it to?

walker (Oct 25 2022 at 09:27):

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.

Enrico Tassi (Oct 25 2022 at 09:36):

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

Enrico Tassi (Oct 25 2022 at 09:36):

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

Enrico Tassi (Oct 25 2022 at 09:37):

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.

walker (Oct 25 2022 at 09:41):

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 ?

Enrico Tassi (Oct 25 2022 at 11:48):

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

Enrico Tassi (Oct 25 2022 at 11:49):

I mean, the type int of math-comp plays the role of Z, and it is built using some notion of positive number

Enrico Tassi (Oct 25 2022 at 11:49):

I don't recall if it is a custom one

Enrico Tassi (Oct 25 2022 at 11:51):

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

Enrico Tassi (Oct 25 2022 at 11:52):

The difference is that positive from PArith are efficient in computations, less in reasoning. Do you need to run computations inside Coq?

walker (Oct 25 2022 at 11:53):

I need to extract code with efficient computations.

walker (Oct 25 2022 at 11:55):

I checked int, it uses nat, which is different from positive, I actually need positive because of it is binary representation.

walker (Oct 25 2022 at 11:56):

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

Cyril Cohen (Oct 25 2022 at 12:19):

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

walker (Oct 25 2022 at 12:37):

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.

walker (Oct 25 2022 at 12:37):

thanks a lot everyone

Last updated: Feb 08 2023 at 07:02 UTC