The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Damien Andrew Tamburri a écrit :
> Hello CoqClubbers!
>
>     I am having difficulty in including the context for rules in 
> Natural Deduction, within a structure representing Natural Deduction 
> Trees themselves (see attached file).. I keep getting the "The term 
> "In a X" has type "Prop" which is not a (co-)inductive type." error 
> for the last three constructors of type NDTree.. can anyone explain me 
> if and how I can use the construct "if..then..else" in this way? what 
> other context alternatives are there?
>
>       many thanks!
>
>         Damian Andrew Tamburri
>
> ------------------------------------------------------------------------
> Click less, mail more: Hotmail on the new MSN homepage! 
> <http://go.microsoft.com/?linkid=9677402>

In fact, you should use something like:

   (*in the following rule context handling is needed*)
   | impi1 : forall (X : list Formula), forall (a b : Formula),
                       NDTree X b -> NDTree X ( logimp a b )

   (*in the following rule context handling is needed*)
   | impi2 : forall (X : list Formula), forall (a b : Formula), ~In a X ->
                       NDTree X ( logimp a b )

I don't know if you want classical or intuitionnistic logic, but I am a 
little puzzled by your rules:

why don't you use "logimp a logcont" for "lognot a"? (+excluded middle rule)
I think you should also be able to add and remove hypothesis in other 
rules than ore (andi for example),
or use the same hypothesis for all and define NDTree with

Inductive NDTree (X : list Formula) : Formula -> Set :=
instead of
Inductive NDTree : list Formula -> Formula -> Set :=

which is far more convenient for inversion and other things

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay