Stream: Coq users

Topic: Idiomatic stdpp

Karl Palmskog (Jul 04 2020 at 11:45):

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

Paolo Giarrusso (Jul 04 2020 at 11:46):

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

Karl Palmskog (Jul 04 2020 at 11:47):

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.

Paolo Giarrusso (Jul 04 2020 at 11:52):

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

Karl Palmskog (Jul 04 2020 at 11:54):

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")

Karl Palmskog (Jul 04 2020 at 11:55):

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

Paolo Giarrusso (Jul 04 2020 at 11:55):

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

``````  (** 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.
``````

Karl Palmskog (Jul 04 2020 at 11:55):

`bsteps_ind_r` looks great, thanks!

Paolo Giarrusso (Jul 04 2020 at 11:56):

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

Karl Palmskog (Jul 04 2020 at 12:00):

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

jco (Jul 04 2020 at 12:32):

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 :)

Karl Palmskog (Jul 04 2020 at 12:41):

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

jco (Jul 04 2020 at 12:54):

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 :)

Paolo Giarrusso (Jul 04 2020 at 13:38):

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