So here is it. Some formalization of/around symbolic dynamics in Coq:

Not much really. But feel free to ask questions, give advice, and/or reuse.

@amiloradovsky glad to see other folks using sourcehut \o/ out of curiosity, do you also have some trouble with low ssh performance?

@lthms I'm basically using it for the first time… The project was uploaded reasonably fast. But sure SourceHut may have less resources than say

@amiloradovsky in some case, a straightforward git push may take up to 25s :/ i don’t think this is related to resource constrain in this case (there is an unanswered issue about that)

Anyway sourcehut remains a very cool projet nonetheless!

@lthms Hmm… I haven't noticed that big delays so far.

Just added .build.yml for the CI, and been informed right in the Git output that build started, with the link to the job.
Can't this be somehow related to the delays in your case? Something in dispatch maybe? IDK, I'm still learning.

@amiloradovsky At least I was able to understand parts of the DeMorgan file...

@byllgrim Well, it's actually not used anywhere now… it's there for historic reasons, and it's got there for the sake of checking what still holds after a changes…

"Let is_identity_map {X: Type} (f: X -> X) := forall x: X, f x = x."

Do I read this as:
Now I define is_identity_map to be (btw X denotes some kinda type) a function taking an X and yielding an X, and this function shall be so that any particular X (let's call it x) stuffed into its eating hole will be shat out untouched?

@byllgrim Yes, it's a condition on endo-function.
And identity map is the map which doesn't do anything to the argument, but just passes it as-is.

@byllgrim There is, by the way, some funny difference between identity and reflexivity, often confusing:
- identity is a map, from a type to itself (type is a parameter)
- reflexivity is a relation, on a pair of a type and it again

I'm glad you shared the stuff. Finally I got an opening into #coq. Just let me know (or stop replying?) if you find my questions tedious.

Let swap {X Y Z: Type} (f: X -> Y -> Z) := fun x y => f y x.

Is this:
Defining swap (btw, here be types) as a function from types to types, if x y are functions you can input them to this function?

"X -> Y -> Z" why isn't this something like "X,Y -> Z"?

@byllgrim No, I'm glad to answer any questions about topics I'm passionate about.

This "swap" works on values of types X and Y respectively, not functions: takes a function from X and Y (in that order) and returns another, from Y and X (in that order).
There is a pair type X * Y, but it isn't as basic as just currying, and thus rarely used in practice.

Sign in to participate in the conversation
Functional Café is an instance for people interested in functional programming and languages.