Stream: math-comp users

Topic: Little porting puzzle


view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2022 at 13:55):

Hi folks, I was reading this twitter thread https://twitter.com/DomLW/status/1489585554496933888 and indeed I can understand Martin's comment "Coq tactics make me dizzy" as indeed I look at the file and I get dizzy too.

@EscardoMartin Checked that one can indeed prove this in Coq: ∀ (X Y : Type) (f : X → Y) (g : Y → X), injective f → injective g → (∃ l : list X, ∀ x : X, x ∈ l) → (∃ fi : Y → X, inverse f fi) ∧ (∃ gi : X → Y, inverse g gi) See here for a proof https://github.com/DmxLarchey/PHP-short/blob/main/php.v

- Dominique Larchey-W. (@DomLW)

Would the file https://github.com/DmxLarchey/PHP-short/blob/main/php.v maybe look much better using math-comp? I'd bet. I'd love to do the porting myself, but I have -1 cycles left so posting here in case anyone would like to pick the challenge up.

view this post on Zulip Karl Palmskog (Feb 05 2022 at 13:58):

it seems to me Escardo is heavily into Agda, and I think many people in the Coq community find Agda proofs similar to how he finds Coq proofs...

view this post on Zulip Karl Palmskog (Feb 05 2022 at 13:59):

so I would doubt MathComp proofs would address this perception

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2022 at 14:01):

Karl Palmskog said:

so I would doubt MathComp proofs would address this perception

I know what you mean, but I disagree, in the sense that a proper math-comp proof should look very close to a pen-and-paper proof in latex

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2022 at 14:01):

that, Martin should have way less problems

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2022 at 14:01):

I'm not an Adga user and I can't read that proof either

view this post on Zulip Michael Soegtrop (Feb 06 2022 at 08:48):

I know what you mean, but I disagree, in the sense that a proper math-comp proof should look very close to a pen-and-paper proof in latex

It all depends on what you are used to. If you are an expert in a specific field, you like more condensed/implicit notations, because more verbose/explicit notations give detail you know anyway and obscure the view on the bigger picture (you can't see the forest cause of the many trees). If you are not an expert in the field, you might prefer more explicit notations. And depending on what your background is, you might be used to completely different notations for the same thing as people with a different background.

IMHO interfaces to Coq developments, which might be used by non experts should be easy to understand also by non experts and not too notation heavy. Elaborate proofs one can't easily understand anyway can use more elaborate notations, because one can expect people need to dig deeper into the material anyway.

In my experience mathcomp notations are usually well readable by non experts, but it also comes with some notations which decorate standard constructs (like functions) in very non obvious ways. E.g. I frequently do "Close Scope set_scope" after importing mathcomp stuff to get e.g. in QuickChick:

forAll =
fun (A prop : Type) (H : Checkable prop) (H0 : Show A) (gen : G A) (pf : A -> prop)
=> bindGen gen (fun x : A => printTestCase (show x ++ newline) (pf x))
     : forall A prop : Type,
       Checkable prop -> Show A -> G A -> (A -> prop) -> Checker

instead of the mathcomp preferred notation:

forAll =
[set A | [set prop | [set H | [set H0 | [set gen | [set pf |
bindGen gen [set x | printTestCase (show x ++ newline) (pf x)]]]]]]]
     : forall A prop : Type,
       Checkable prop -> Show A -> G A -> (A -> prop) -> Checker

which I don't find very understandable.


Last updated: Feb 08 2023 at 07:02 UTC