The Coq mailing list

[Fabian Kunze <fabian.kunze AT cs.uni-saarland.de>]

Hi Jerome,

Note that no amount of evaluation can simplify "True /\ X" to X, as this 
expression is of type Prop, i.e. a logical proposition and not a 
computational boolean. "/\" is not a function defined by it's 
computational rules, but an inductive type whose values can be 
established by the 'conj' constructor:

''''
Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B
where "A /\ B" := (and A B) : type_scope.
'''

On the other hand, booleans correspond to what you might have in mind: 
boolean conjunction "andb true x" will reduce to `x`.

Best,
Fabian
Am 4/21/2021 um 18:21 schrieb Jerome Hugues:
> I still end up with terms like
>
> = False /\
>
>         ([] = [] /\
>
>          (Feature (Ident "a_feature") inF eventPort
>
>             (Component (Ident "") null (Ident "") [] [] [] []) [] =
>
>           Feature (Ident "a_feature") inF eventPort
>
>             (Component (Ident "") null (Ident "") [] [] [] []) [] \/ 
> False) \/
>
>          False)
>
>       : Prop
>
> And I believe an evaluation strategy would reduce those basic terms to 
> either True or False without intervention. But I fail to establish one. 
> It works in some cases, but not on other and I am trying to understand 
> the pattern behind those.
>
> Generally speaking, all my definitions are based on equality of some 
> inductive types based on nat or lists of other inductive types. So the 
> use case is rather narrow.
>
> Thanks,
>
> *From: *<coq-club-request AT inria.fr> on behalf of Jean-Christophe 
> Léchenet <jean-christophe.lechenet AT inria.fr>
> *Reply-To: *"coq-club AT inria.fr" <coq-club AT inria.fr>
> *Date: *Wednesday, April 21, 2021 at 4:26 AM
> *To: *"coq-club AT inria.fr" <coq-club AT inria.fr>
> *Subject: *Re: [Coq-Club] Qed opacity and Coq standard library
>
> Hi Jerome,
>
> Two blog posts that are relevant to this topic :
> - http://gallium.inria.fr/blog/coq-eval/ 
> <http://gallium.inria.fr/blog/coq-eval/>
> - https://gmalecha.github.io/reflections/2017/qed-considered-harmful 
> <https://gmalecha.github.io/reflections/2017/qed-considered-harmful>
>
> Not sure if that will help in your case, though.
>
> Best,
>
> Jean-Christophe
>
> Le 20/04/2021 à 15:48, Jerome Hugues a écrit :
>
>     Hi,
>
>     At some point in my project, I use Defined rather than Qed to have
>     transparent proofs and use the Compute mechanisms to evaluate some
>     statements. This works nicely for my own theorems, but I am stuck
>     when this involves theorems provided by the Coq standard library,
>     NoDup_dec in my case, but ultimately this might extend to more
>     situations.
>
>     One quick and dirty work-around is to copy/paste the code, change
>     Qed into Defined and voila! But this is not satisfactory.
>
>     I could find some blog posts like this one
>     https://plv.csail.mit.edu/blog/computing-with-opaque-proofs.html
>     <https://plv.csail.mit.edu/blog/computing-with-opaque-proofs.html>
>     by Clément Pit-Claudel on this topic, but again it seems this
>     imposes some rework.
>
>     I understand Qed and Defined are different for a reason, I am just
>     curious whether there is a systematic way to change Qed into Defined
>     on a case by case basis, or if we are forced to this type of
>     modifications.
>
>     Is there some suggested readings on this topic?
>
>     Thanks