The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Bernard,

If you have the property you're asking for then A can only
be a base formula. If what you are really looking for is
something like

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

then the following inductive definition should do the trick:
defining a subformula amounts to describing a path from
the root of the big formula down to the root of the small
one.

Inductive SubFormula (f : Formula) : Formula -> Set :=
  | here : SubFormula f f
  | left : forall g h, SubFormula f g -> SubFormula f (g ! h)
  | right : forall g h, SubFormula f h -> SubFormula f (g ! h)
.

Cheers,

--
guillaume



On 6 April 2012 10:59, Bernard Hurley 
<bernard AT marcade.biz>
 wrote:
> Hi all,
>
> Given code like:
>
> ==================================
>
> Inductive Formula: Set :=
>    &#952;
>  | 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  (&#952;!&#952;)  ((&#952;!&#952;)!&#952;))) is True whereas:
> (Subformula  (&#952;!(&#952;!&#952;))  ((&#952;!&#952;)!&#952;))) 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.