The Coq mailing list

["Theodoros G. Tsokos" <T.Tsokos AT cs.bham.ac.uk>]

Adam Chlipala wrote:
> I don't think your lemma is true, going on just the information you've 
> provided so far.  While you could prove the goal [f (v1 + v2)] from [f 
> v1] and [f v2], the hypothesis of [f (a1 + a2)] does not imply [f a1] 
> or [f a2], because a natural number can be decomposed into multiple 
> distinct sums.  (And this is ignoring the potential further 
> confounding influences of the [f] constructors you haven't included.)
>
> Theodoros G. Tsokos wrote:
> > Assuming I want to solve the following goal in a Lemma:
> >
> > H1: f a1 -> f v1
> > H2: f a2 -> f v2
> > ============
> > f (a1+ a2) -> f (v1+v2)
> >
> > Where in the inductive definition of f, one of its constructors is:
> >
> > Inductive f :  ... :=
> > ...
> > | ...
> > | Cx : forall x y, f x -> f y -> f(x+y)
> > | ...
> > .
Well, let me be more precise, as I think that my example wasn't the most 
appropriate one.

Assuming that I have *op_and* defined, as the logical operator between 
two terms b1 b2. Let *FF* be an inductive definition:

Inductive FF:  env->term->type->Prop :=
....
| C4:  forall G b1 b2, FF G b1 expr -> FF G b2 expr -> FF G (op_and b1 
b2) expr
....

And assuming that in my Lemma, I want to prove the following subgoal:

...
G : env
b1: term
b2: term
v1: bool
v2: bool
t: type
...

 H1 : FF G b1 t -> FF G v1 t
 H2 : FF G b2 t -> FF G v2 t
================================
  FF G (op_and b1 b2) t -> FF G (v1 && v2) t


Is is possible to prove it? I think it should be, as I proved this lemma 
on paper properly.

Thanks again,
Theo.