The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi,

We are currently working on Mtac, a tactic language for Coq in Coq, which makes this sort of problems very easy to encode. Below you can find the translation function written in Mtac. And it can also handle binders! 

If you're interested, here is an outdated version of the tutorial:
http://www.mpi-sws.org/~beta/mtac/mtac_tutorial.html

We hope to release the first version soon, with various examples and a technical report explaining the details. Stay tuned!

----8<---- code ----8<----

Definition trans :=
  mfix f [p : Prop] : T Prop :=
  mmatch p return T Prop with
  | [A B] A \/ B =>
     l <- f A;
     r <- f B;
     ret (~~ (l \/ r))

  | [A B] A /\ B =>
     l <- f A;
     r <- f B;
     ret (l /\ r)
  | _ => ret p
  end.

Definition test := run (trans (True /\ (False \/ True))).

On Thu, Feb 28, 2013 at 7:30 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

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