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.

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...

so I would doubt MathComp proofs would address this perception

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

that, Martin should have way less problems

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

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