Stream: math-comp users

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


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 25 2022 at 09:36):

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

view this post on Zulip Enrico Tassi (Oct 25 2022 at 09:36):

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

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip Enrico Tassi (Oct 25 2022 at 11:48):

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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 25 2022 at 11:49):

I don't recall if it is a custom one

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip walker (Oct 25 2022 at 11:53):

I need to extract code with efficient computations.

view this post on Zulip 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.

view this post on Zulip walker (Oct 25 2022 at 11:56):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip walker (Oct 25 2022 at 12:37):

thanks a lot everyone


Last updated: Feb 08 2023 at 07:02 UTC