Karl Palmskog (Jul 04 2020 at 11:45): 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.
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.
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!
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.
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: Feb 01 2023 at 13:03 UTC