The Coq mailing list

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

Yves Bertot wrote:
> Theodoros G. Tsokos wrote:
> ...
> > 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.
> What you are showing is still confusing as it looks to be not well-typed.
> Is there a coercion from bool to term?  Are there other constructors 
> in the definition of FF that conclude
> with "op_and ..."?
>
> Yves
Yes, there is a coercion from bool to term after the definition of term:

---------------------------------------------------------------------
Inductive term: Set :=
...
| term_bool (_ : bool)

...
.

Coercion term_bool : bool >-> term.
---------------------------------------------------------------------

Also, there 're no other constructors in the definition of FF that 
conclude with "op_and ... ".

Trying not to bore you and not to have a huge email, I might be missing 
some important parts for your comprehension.

Regards,
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"              |
--