## 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

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

Looks nice!

``````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_dec`suggests 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 like`myP: 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).

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

(deleted)

(deleted)

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

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

Last updated: Jun 15 2024 at 08:01 UTC