The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

I feel this is a basic question, but I've gone over the tactics index
in the reference manual and I have found no inspiration there. Thanks
in advance for any help.

How, in Coq, do I make use of the basic property of a fixpoint, i.e.,
for some term Trm, if Fc is the term (Fix F {F/1:Tp->Prop := [t:Tp]
Trm}), then Trm[F:=Fc] equals Fc.

An example of what I want to do:


Inductive T:Type := T_cons: T -> T | T_Leaf:T.
Parameter P:T->Prop.

Definition for_all :=    (Fix F0
          {F0 [myP:(T->Prop); t2:T] : Prop :=
             Cases t2 of
               (T_cons t) => (F0 myP t)/\(myP t2)
              | T_Leaf => True
             end}).

Theorem How: (t:T) (for_all P (T_cons t)) -> (P (T_cons t)).

All I need is replacing "(for_all P (T_cons t))" by "(for_all P t) /\
(P t)" (footnote 1), but I don't know, and didn't find in the manual,
how to do this step. It is some kind of beta-reduction, but "Cbv Beta"
doesn't do it.


Thank you very much for your help,

Footnote 1: Or its beta-expansion (([t2:T] Cases t2 of
               (T_cons t) => (for_all P t)/\(P t2)
              | T_Leaf => True
             end) (T_cons t))

-- 
Lionel

Attachment: pgpo09R8t5bdz.pgp
Description: PGP signature