The Coq mailing list

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

Dear all,

Apologies for that possible trivial question and for the possible non 
appropriate for the question subject.

I'll try to describe a problem I'm addressing lately. I won't write down 
the entire model, just a brief description of it. I hope it's enough, 
otherwise I'll write down more information in a future email. I wouldn't 
like to tire you with much code, that's why I'm trying it in that way.

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

I really can't think of a way of using the constructor Cx as a Hint to 
solve the goal, which I reckon should be the way of addressing the 
problem.  Any help please?

Thanks a lot in advance,
Theo.

--
| Theodoros G. Tsokos                                      |
| http://www.cs.bham.ac.uk/~txt                            ;|
| School of Computer Science, The University of Birmingham |
| Edgbaston, Birmingham, B15 2TT, United Kingdom           |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "The freedom of speech includes the freedom to shut up"  |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "Democracy: the freedom to say whatever one wants and    |
| the capital to implement whatever it wants"              |
--