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

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

suggests the statement `{is_prefix l1 l2}+{~ is_prefix l1 l2} `

more than a boolean function: maybe `is_prefixb`

?

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

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

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

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

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

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?

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)

once you write a `Decision P`

instance, you can use `bool_decide P`

directly, you needn't write a separate `bool`

version

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

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

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

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

(deleted)

(deleted)

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

Last updated: Jun 15 2024 at 08:01 UTC