walker (Oct 25 2022 at 09:27): 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