The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

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