The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Feb 28, 2013 at 9:37 AM, Pierre Courtieu
<pierre.courtieu AT gmail.com>
 wrote:
> 2013/2/28 Giovanni Birolo 
> <giovanni.birolo AT gmail.com>:
>> Hello,
>>
>> i have been trying to define some variants of the double-negation
>> translation for formulas. Since Coq represent formulas as terms of type
>> Prop, my first thought was defining a function from Prop to Prop.
>> Unfortunately this appears to be impossible since Prop is not defined
>> inductively and thus functions cannot be defined by induction on the
>> structure of the formula. For example the following does not work:
>>
>> Definition trans (F : Prop) : Prop := match F in
>>   | A \/ B => ~~ (trans A \/ trans B)
>>   | A /\ B => trans A /\ trans B
>>   ...
>>
>> How should i proceed? The only alternative seems to be defining my own
>> inductive type of formulas, but this feels a bit like reinventing the 
>> wheel.
>
> Hi,
> Indeed you cannot write this kind of function. Yes the usual approach is
> to perform a deep embedding of the kind of formula you want to deal with
> (that is reinventing the wheel). Then for convenience you can use reflection
> to go back to Prop. Using proved theorems like:
>
> Lemma ok: forall F:Prop, f f': formulas,
>    interp f = F ->
>    simplify f = f' ->
>    F <-> interp f'.
>
> where interp is the function from formula to Prop and "and" is the
> formula constructor for conjonction. Then from a property F you still
> need to "guess" f, which you cannot do in Coq. But one can in Ltac (in
> simple cases) or ocaml. The reverse function (interp) is easy to write
> in Coq.
>
> There are plenty of references on internet about reflection in Coq.

It's also easy to write typeclasses to do this type of thing.  For example:

Class DoubleNegTrans (P:Prop) : Type :=
| double_neg_trans : Prop.

(* Make P an explicit argument of double_neg_trans. *)
Arguments double_neg_trans P [DoubleNegTrans].

Instance def_double_neg_trans (P:Prop) : DoubleNegTrans P | 5 :=
  ~~P.

Instance and_double_neg_trans (P Q:Prop)
  `{!DoubleNegTrans P} `{!DoubleNegTrans Q} : DoubleNegTrans (P /\ Q) :=
(double_neg_trans P) /\ (double_neg_trans Q).

Instance or_double_neg_trans (P Q:Prop)
  `{!DoubleNegTrans P} `{!DoubleNegTrans Q} : DoubleNegTrans (P \/ Q) :=
~~ ((double_neg_trans P) \/ (double_neg_trans Q)).

Instance neg_double_neg_trans (P:Prop) : DoubleNegTrans (~P) :=
~P.

Instance impl_double_neg_trans (P Q:Prop) `{!DoubleNegTrans Q} :
  DoubleNegTrans (P -> Q) :=
P -> double_neg_trans Q.

Compute (fun P Q R:Prop => double_neg_trans ((P /\ Q) \/ R)).
-- 
Daniel Schepler