Stream: Coq users

Topic: ssreflect how bool value true can became Prop?

Andrey Klaus (Apr 03 2021 at 17:07):

well, quite simple code below can not be compiled (which is correct because bool value true is not from Prop)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive test : forall a: Prop, Prop :=
| testconstr : test true.

Print test.

but when I add From mathcomp Require Import ssrbool. it compiles. And Check true. still reports true : bool.
Could anybody give me a small explanation about what is going on? Or a link where to read about it. Or both, if possible :)

From mathcomp Require Import ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive test : forall a: Prop, Prop :=
| testconstr : test true.

Print test.

Enrico Tassi (Apr 03 2021 at 17:25):

There is an automatic cast from bool to Prop called is_true. Set Printing Coercions will show it. See https://zenodo.org/record/4457887#.YGikvRKxW8Q page 112

Andrey Klaus (Apr 03 2021 at 18:05):

Thank you!

Andrey Klaus (Apr 03 2021 at 19:59):

o wow, Enrico, quite interesting book! I added to my read list. Thanks for the book!

Andrey Klaus (Apr 03 2021 at 20:11):

Thanks to the both authors.

Last updated: Apr 19 2024 at 20:01 UTC