Stream: Coq users

Topic: Idiomatic stdpp


view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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")

view this post on Zulip 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

view this post on Zulip 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.

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.

view this post on Zulip Karl Palmskog (Jul 04 2020 at 11:55):

bsteps_ind_r looks great, thanks!

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jul 04 2020 at 12:00):

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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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: Feb 01 2023 at 13:03 UTC