Stream: math-comp users

Topic: Does mathcomp has notion of seq permutation without EqType


view this post on Zulip walker (Nov 12 2022 at 18:51):

I am strugging trying to unerstand how to use the seq permutation, and I was wondering if there is a version of it that does not require eqType and if there is, how to use it ?

view this post on Zulip Karl Palmskog (Nov 12 2022 at 19:06):

you can always use Permutation from Stdlib. I don't think there are any MathComp projects reasoning on permutations where the seq type is not an eqType.

view this post on Zulip Pierre Roux (Nov 12 2022 at 19:27):

Without eqType, nothing computable, so definitely not in the spirit of MathComp (small scale reflection).

view this post on Zulip walker (Nov 12 2022 at 19:39):

alright, a follow up question. what is example of a type that is not eqtype.

Everytype I can come up with look like eqtype, so I am trying to understand the limitations here

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:43):

nat -> bool

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:43):

quotients with undecidable relations

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:45):

type universes

view this post on Zulip Karl Palmskog (Nov 12 2022 at 19:45):

constructive reals as in CoRN don't have any decidable equality IIRC

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:47):

forgot: codata

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:54):

but there is a huge class of types where decidable equality is guaranteed, not sure how to phrase that clearly and correctly: finitely branching tree / finitary syntax / ...
Informally this should mean, if you build types from scratch and never use codata, functions from infinite domains, or elements of universes, you can't build types without decidable equality.

Even functions from finite domains can have decidable equality, but the proof requires fun_ext (thankfully, the use remains proof-irrelevant)

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:56):

(proof: https://github.com/bedrocksystems/BRiCk/blob/2933ab8d24a969679e680b1c9ca771dd60abb1c2/theories/prelude/finite.v#L24-L33)

view this post on Zulip walker (Nov 12 2022 at 19:56):

Alright, followup question 3: since I was working on library for implementing trie data structure, many of the operations require require either support from mathcomp (hence requires both key and value to be eqType) or then I will have to not use math-comp and instead use stdlib version.

At this point it is not clear what kind of limitation I am putting on myself by making everything eqtype. Ideally my goal is stuff that extracts, and my intuition is anything extractable is eqtype by definition (since it takes finite memory so it must be mem-comparable)

But on the other hand it feels wrong to restrict everything to eqType ( i think in a previous thread, I received advice not do that)

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:58):

My take is that restricting to eqType is natural for keys, and unnatural for values but maybe it's natural in math-comp?

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 19:58):

(I think I was the one objecting in the other thread, and maybe because I don't get/agree with math-comp here; different opinions are reasonable!)

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 20:00):

anything extractable is eqtype by definition (since it takes finite memory so it must be mem-comparable)

I'd bet you can extract functions from N even if they don't have decidable equality.

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 20:02):

this restriction is probably fine in most cases, it's just stricter. And I suspect some/many of the other examples are also extractable.

view this post on Zulip walker (Nov 12 2022 at 20:02):

I see, I guess I will have to use permutation then, I am really following how stdpp is doing things.

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 20:03):

of course, _implementations_ of functions use finite memory, and comparing that memory will terminate. But you can't write this in Coq, and it'll give the wrong value in many cases: fun x : nat => x and fun x : nat => x + 0 are propositionally equal (with funext) but they probably translate to different code.

view this post on Zulip walker (Nov 12 2022 at 20:03):

I guess fun ext is reasonable assumption in general ?

view this post on Zulip walker (Nov 12 2022 at 20:04):

based on my limited understanding it is a lemma in cubical type theory which is super set of MLTT/CIC in some sense

view this post on Zulip walker (Nov 12 2022 at 20:05):

but I am talking about the proof-relevant version of it here*

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 20:06):

fun_ext is true in (almost?) every foundation of maths, starting from ZFC and the ZFC-based models of Coq

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 20:06):

cubical TT lets you prove it as well

view this post on Zulip walker (Nov 12 2022 at 20:06):

when you say almost, it makes me wonder when it is false

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 20:08):

most of the time, its only problem is it won't compute, but that's seldom a problem if you're not using equalities as proof-relevant.

view this post on Zulip Kenji Maillard (Nov 12 2022 at 20:10):

walker said:

when you say almost, it makes me wonder when it is false

In some intensional models (exceptional MLTT + parametricity, or the model of polynomial functors)

view this post on Zulip Paolo Giarrusso (Nov 12 2022 at 20:26):

intuitively, when funext is false, it's because the interpretation of a function in the model contains some thing extra beyond its input-output behavior; typically it's the function "code" (that's what "intensional model" means), but https://hal.inria.fr/hal-01445835/document shows a relatively simple model which stores less extra data (just booleans).

view this post on Zulip Meven Lennon-Bertrand (Nov 14 2022 at 10:15):

One issue of the "×bool" model is that it also breaks η-laws for functions, which at least in MLTT is usually included. You need the extra data of the fancier models to negate function extensionality while retaining η

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 10:22):

Indeed, · × bool is nasty because functions are not really functions anymore. In call-by-name η laws for fun types should hold.

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 10:22):

but interestingly parametric exceptional TT and polynomial functors break funext for somewhat distinct reasons

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 10:23):

the first one breaks it because there are "junk" inhabitants of types (exceptions) that do not exist at toplevel but exist transiently in the model, so that in practice e.g. for unit -> unit there are two distinct inhabitants, the identity and the constant functions. They do not behave the same on junk inhabitants, hence breaking funext.

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 10:24):

the latter breaks it for more fundamental reasons, namely that it exposes details about the way arguments are used

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 10:25):

polynomial functors are basically a variant of Dialectica, and that means that you can get real intensional content out of functions.

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 10:25):

a not-so-wrong way to picture is that this gives you the O(f n) of the runtime of the function

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 10:26):

In a complexity-aware type theory, two functions can compute the same graph but have wildly different algorithmic complexities. As such they can't be equal, hence breaking funext.

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 11:18):

Karl Palmskog said:

you can always use Permutation from Stdlib. I don't think there are any MathComp projects reasoning on permutations where the seq type is not an eqType.

In FCSL-PCM we have https://github.com/imdea-software/fcsl-pcm/blob/master/core/seqperm.v

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 11:22):

This comes in handy for reasoning on heap predicates sometimes.

view this post on Zulip walker (Nov 14 2022 at 12:30):

@Alexander Gryzlov side question: If I wanted to learn about pcms in general, would there be a specific paper that in your opinion is a must read?

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 12:34):

walker said:

Alexander Gryzlov side question: If I wanted to learn about pcms in general, would there be a specific paper that in your opinion is a must read?

Depends on what you want to do with them, in the context of proving things about single-threaded heap-based programs in SSReflect probably a good starting point is Nanevski, Vafeiadis, Berdine, [2010] "Structuring the verification of heap-manipulating programs"

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 12:38):

Scaling this to concurrency requires quite a few generalizations to this base idea, my current hypothesis that I'm working on is that there are some middle grounds between classical "tree-like" separation logic proofs and full-blown concurrent SL featuring linearizability.

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 12:39):

Specifically that the ideas from the latter can be motivated by working on proofs for graph- and array-manipulating programs

view this post on Zulip walker (Nov 14 2022 at 12:51):

so what you are saying is that PCM is analogous to Hoare-logic, and what you are trying to do is to generalize PCMs to handle concurrency the same way CSL is generalization of hoare logic, is my understanding correct ?

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 12:54):

Well we are also using some form of Hoare logic, the idea is that we work directly with models of state (PCMs) instead of axiomatizing it on a logical level with things like separating conjuction/implication.

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 12:58):

So basically instead of viewing HL/SL as a sort of logical API that you can use to construct your proofs with, we say it's like a bridge that allows to generate a bunch of PCM equations from the syntax of your stateful program and use algebraic-style reasoning on them.

view this post on Zulip Alexander Gryzlov (Nov 14 2022 at 12:59):

For single-threaded heaps (and tree-like structures built on top of them) the difference between two styles is not that big but they really start to diverge once you go into concurrency.

view this post on Zulip Paolo Giarrusso (Nov 14 2022 at 20:11):

Re the side question, just to see if I understand (but I haven't used FCSL, only Iris):


Last updated: Jan 29 2023 at 18:03 UTC