**Pierre Roux**
(7762b81f)
*
at
13 Mar 17:37
*

Update examples/case_study/usual_functions.v

**Pierre Roux**
(f098ebc3)
*
at
22 Feb 15:24
*

[tutorial] Add make rule for generating PDF

**Pierre Roux**
(049df491)
*
at
21 Feb 14:35
*

[tutorial] Avoid introducing the `{...} syntax

*
... and
29 more commits
*

**Pierre Roux**
(c25a2d14)
*
at
21 Feb 14:17
*

[tutorial] Avoid introducing the `{...} syntax

*
... and
29 more commits
*

**Pierre Roux**
(6ac74eb9)
*
at
21 Feb 13:51
*

[tutorial] Avoid introducing the `{...} syntax

*
... and
184 more commits
*

**Pierre Roux**
(5fa21410)
*
at
14 Feb 08:57
*

[CI] Don't recompile mathcomp solvable and field

*
... and
263 more commits
*

**Pierre Roux**
(6bd62cde)
*
at
08 Nov 10:45
*

@bbb CI green

This fixes compilation with current Coq master.

We discovered compilation with Coq master was broken in https://github.com/coq/opam-coq-archive/pull/2374 This should fix it, I'll then reopen a PR on opam-coq-archive to update the coq-prosa.dev OPAM package.

**Pierre Roux**
(6bd62cde)
*
at
08 Nov 09:52
*

*
... and
250 more commits
*

Sorry for the late answer. While !243 (merged) is certainly a very nice improvement (congrats @kbedarka by the way!) I still think using a more appropriate level of abstraction for sets rather than sequences (along with proofs of non duplication) would be an improvement. However this requires some work which I won't be able to make in the coming months so indeed closing looks like a good solution. I'll can always reopen when I get back to it.

Sorry for the late answer, just a few thoughts about the `e*`

and `have`

tactics.

Writing proof scripts is often a trade off between conciseness and robustness. The `e*`

tactics often enable to write short proofs but may, by definition, implicitly introduce existential variables which may make the proof harder to maintain (if one more (or less) existential variable becomes generated in some future evolution of the code, it may only be detected later in the proof, thus making the proof painful to fix). In constrast `have`

tends to make proofs larger (since one has to explicitly describe an intermediate proof step) but, by introducing a cut (in the logical sense of the term https://en.wikipedia.org/wiki/Cut_rule ) it breaks the proof in smaller parts making it easier to maintain as future changes are likely to incur more local failures, that are easier to fix.

To sum up, the choice is a trade off. For instance something like `by edestruct; <proof remaining in a single line>.`

is usually fine and can save a few lines but `edestruct. <10 lines long proof>`

is probably asking for future troubles.

In my own proofs, I most often avoid the `e*`

tactics (`apply:`

and `rewrite`

often do most of the work) and use `have`

as soon as a sub proofs takes a few lines or is reused multiple times. (quite unrelated: I also tend to prefer `have`

above `tactic in hyp`

modifiers, for instance I find `have {}hyp := lemma hyp`

more readable than `apply lemma in hyp`

, one can also use the ssreflect notations in have, for instance `have [e /andP[einA einB]] : exists e, e \in A && e \in B`

or `have [xlty|//|xgty] := ltngtP.`

to do a case distinction on some `n <= m`

in the goal)

Anyway, congrats @sbozhko for completing this merge request!