The Coq mailing list

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