The Coq mailing list

[Bernard Hurley<bernard AT marcade.biz>]

Hi all,

Given code like:

==================================

Inductive Formula: Set :=
    θ
  | F_join: Formula -> Formula -> Formula.

Notation "x ! y"  := (F_join x y)
  (at level 20, no associativity).

===================================

Is there any way of defining a predicate Subformula so that, for instance,

(Subformula  (θ!θ)  ((θ!θ)!θ))) is True whereas:
(Subformula  (θ!(θ!θ))  ((θ!θ)!θ))) is False?

Intuitively the predicate can be defined inductively by:

(Subformula A B!C) <-> (Subformula A B) \/ (Subformula A C),

but I can't find any way of actually doing it coq. I think it should be fairly
obvious what I mean by a subformula. Thanks in advance for any help.

Bernard.