The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi Guillame

On Fri, Apr 06, 2012 at 11:50:10AM +0100, gallais @ ensl.org wrote:

> 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

Yes this is what I am looking for!

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

Thanks!!

Bernard.