Stream: Coq users

Topic: ✔ Just proving some lemmas...

Huỳnh Trần Khanh (Sep 25 2022 at 15:34):

To practice using Coq I proved some stuff. I'm mostly just getting used to Coq syntax. I'd like to hear your feedback. The things that I'm most interested in are

• code readability and best practices
• am I proving lemmas that are already present in the standard library? please tell the lemmas that I don't need to prove because they are already in the standard library, so next time I can just use the existing ones instead

Code: https://pastebin.com/raw/P7qr9YEj

Pierre Castéran (Sep 25 2022 at 16:22):

Looks nice!
Just a few remarks, not about already existing lemmas, but about tactics which may simplify your proofs:

Lemma bracket_t_eq_dec : forall x y : bracket_t, {x = y} + {x <> y}.
Proof. decide equality. Defined.

Lemma heads_are_equal (a b : bracket_t) (l1 l2 : list bracket_t) : a::l1 = b::l2 -> a = b.
Proof. injection 1. easy. Qed. (* same for tails *)

Lemma introduce_equal_heads (a : bracket_t) (l1 l2 : list bracket_t) : (* to use with rewrite *)
  is_prefix_dec (a::l1) (a::l2) = is_prefix_dec l1 l2.
Proof.
  funelim (is_prefix_dec (a::l1) (a::l2)); easy.
Qed.

About naming: the name is_prefix_decsuggests the statement {is_prefix l1 l2}+{~ is_prefix l1 l2} more than a boolean function: maybe is_prefixb?

Karl Palmskog (Sep 25 2022 at 16:37):

I think there are two ways to consider bool in modern Coq code:

• embrace bool fully via small-scale reflection and MathComp (write lemmas likemyP: reflect my_bool_fn my_prop_for_bool_fn)
• avoid bool and replace every use with the Decision typeclass from Std++ ("informative boolean")

Karl Palmskog (Sep 25 2022 at 16:40):

the rationale is that undisciplined code that uses bool will typically lead to a bunch of ad-hoc lemmas connecting bool and Prop. Both ssreflect and Std++ "track" the information content of bool-valued functions in a much more disciplined way (via view lemmas and typeclass instances, respectively).

Karl Palmskog (Sep 25 2022 at 16:46):

related: https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/

Notification Bot (Sep 26 2022 at 00:59):

Huỳnh Trần Khanh has marked this topic as resolved.

Notification Bot (Oct 03 2022 at 15:28):

Huỳnh Trần Khanh has marked this topic as unresolved.

Huỳnh Trần Khanh (Oct 03 2022 at 15:32):

Oh dear. Today I experimented with coq-stdpp. I want to make a decidable proposition with the Decision typeclass. I want to do something like prove the proposition is equivalent to a decision procedure of type bool to get an instance of Decision. How could I achieve that?

Karl Palmskog (Oct 03 2022 at 16:27):

I think the lemmas/instances you want are mostly here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/decidable.v (see bool stuff in that file)

Paolo Giarrusso (Oct 03 2022 at 19:18):

once you write a Decision P instance, you can use bool_decide P directly, you needn't write a separate bool version

Paolo Giarrusso (Oct 03 2022 at 19:19):

you probably can, but I've yet to need it

Paolo Giarrusso (Oct 03 2022 at 19:20):

if you want to compute with it (which is a good idea), you do need to write the Decision instance carefully so that the proofs don't reduce

Notification Bot (Oct 04 2022 at 00:40):

Huỳnh Trần Khanh has marked this topic as resolved.

Notification Bot (Oct 04 2022 at 03:21):

Huỳnh Trần Khanh has marked this topic as unresolved.

Huỳnh Trần Khanh (Oct 04 2022 at 03:22):

(deleted)

Huỳnh Trần Khanh (Oct 04 2022 at 03:46):

(deleted)

Notification Bot (Oct 04 2022 at 12:39):

Huỳnh Trần Khanh has marked this topic as resolved.

Last updated: Oct 03 2023 at 21:01 UTC