@Paolo G. Giarrusso can you give an example of a relatively short lemma (12-20 lines of Ltac) which uses idiomatic stdpp? Preferably with some structure in the proof (subcases, etc.)

Uh! I hope so, but can you give some context for the question? Also, can it be a lemma _from_ stdpp?

my presentation at the workshop tomorrow will show some different styles of Coq code as motivation. I don't mind if it's from stdpp itself.

That helps! "Short" and "12-20 lines" contradict each other, given the stdpp style, but what about one of these? If not I'm happy to try again

```
Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
Proof.
split.
- induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
- intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
inversion Hin; subst. by left. right; auto.
Qed.
```

```
Lemma Forall_forall l : Forall P l ↔ ∀ x, x ∈ l → P x.
Proof.
split; [induction 1; inversion 1; subst; auto|].
intros Hin; induction l as [|x l IH]; constructor; [apply Hin; constructor|].
apply IH. intros ??. apply Hin. by constructor.
Qed.
```

OK, then maybe you could try to find one that is "long" by stdpp standards (note that both CompCert and MathComp has plenty of lemmas with 100+ Ltac lines, so that's my measure of "long")

unfortunately, 4 Ltac lines for stdpp is a bit too short for me to convey the differences

the handling of subcases often resembles math-comp's style using terminators, or at best `{...}`

as in the following:

```
Lemma bsteps_ind_r (P : nat → A → Prop) (x : A)
(Prefl : ∀ n, P n x)
(Pstep : ∀ n y z, bsteps R n x y → R y z → P n y → P (S n) z) :
∀ n z, bsteps R n x z → P n z.
Proof.
cut (∀ m y z, bsteps R m y z → ∀ n,
bsteps R n x y → (∀ m', n ≤ m' ∧ m' ≤ n + m → P m' y) → P (n + m) z).
{ intros help ?. change n with (0 + n). eauto. }
induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
intros n p1 H. rewrite <-plus_n_Sm.
apply (IH (S n)); [by eauto using bsteps_r |].
intros [|m'] [??]; [lia |]. apply Pstep with x'.
- apply bsteps_weaken with n; intuition lia.
- done.
- apply H; intuition lia.
Qed.
```

which is about

```
(** Reductions of at most [n] steps. *)
Inductive bsteps : nat → relation A :=
| bsteps_refl n x : bsteps n x x
| bsteps_l n x y z : R x y → bsteps n y z → bsteps (S n) x z.
```

`bsteps_ind_r`

looks great, thanks!

or even

```
Lemma list_find_app_Some l1 l2 i x :
list_find P (l1 ++ l2) = Some (i,x) ↔
list_find P l1 = Some (i,x) ∨
length l1 ≤ i ∧ list_find P l1 = None ∧ list_find P l2 = Some (i - length l1,x).
Proof.
split.
- intros ([?|[??]]%lookup_app_Some&?&Hleast)%list_find_Some.
+ left. apply list_find_Some; eauto using lookup_app_l_Some.
+ right. split; [lia|]. split.
{ apply list_find_None, Forall_lookup. intros j z ??.
assert (j < length l1) by eauto using lookup_lt_Some.
naive_solver eauto using lookup_app_l_Some with lia. }
apply list_find_Some. split_and!; [done..|].
intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
by rewrite lookup_app_r, minus_plus by lia.
- intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
+ apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
assert (i < length l1) by eauto using lookup_lt_Some.
intros j y ?%lookup_app_Some; naive_solver eauto with lia.
+ rewrite list_find_Some, lookup_app_Some. split_and!; [by auto..|].
intros j y [?|?]%lookup_app_Some ?; [|naive_solver auto with lia].
by eapply (Forall_lookup_1 (not ∘ P) l1); [by apply list_find_None|..].
Qed.
```

ah, that one had much less UTF8, which apparently lstlistings chokes on

Karl Palmskog said:

my presentation at the workshop tomorrow will show some different styles of Coq code as motivation. I don't mind if it's from stdpp itself.

a bit orthogonal but will the slides or presentation be distributed after the workshop? I'd be interested in seeing, if so :)

yes, we definitely plan to put the slides online at the workshop website, but it may take until Monday

no rush...as a new user myself though I've definitely struggled with the preponderance of proof styles, libraries, etc. will be a nice resource to chip away at that ignorance :)

On this front, "how to choose a style" is also something I'm curious on, even with some more experience :-)

Last updated: Jun 18 2024 at 10:02 UTC