The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 28 Feb 2013 17:06:30 +0100,
Giovanni Birolo 
<giovanni.birolo AT gmail.com>
 a écrit :

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

That is not reinventing the wheel.
You only want to work with a subset of Prop, so you need to tell Coq
what subset you consider.

Think of it as if you want to pattern match of coq terms:

Definition optimize (f : A -> B) : A -> B :=
  match f with (* and not in! *)
  | id => …
  | comp f g => …
  | (fun x => t) => …
  …

Or more correctly if you want to pattern match on types (Prop is just
a collection of types after all):

Definition currify (t : Type) := match t with
  | (A*C) -> B => currify (A -> (currify (C -> B)))
  | nat -> x => nat -> x
  | bool -> x => bool -> x
  | nat => nat
  | bool => bool
  …

It is not possible. All you have to do is to define a reification of
the type you consider.

Inductive type :=
| Nat
| Bool
| Prod : type -> type -> type
| Arrow : type -> type -> type.

Just to justify it, imagine, someone defines a new prop:

Inductive and2 (P Q : Prop) := conj2 : P -> Q -> and2 P Q.

then 'and' & 'and2' are completely isomorphic, but your function could
not take it into account (and2 has been defined after your function
after all).

> Also if i could work directly with Prop i could write
> something like:
> 
> Theorem fact1 : forall F : Prop, F -> trans F.
> 
> But this is not possible if i have to define a custom type for
> formulas. Is my understanding correct?
> 
> Thanks.

You still can do something like:

Theorem fact1 : forall F : MyProp, interp F -> interp (trans F).

Which is not that bad after all…