The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT lri.fr>]

Hello,

In this case, you just need to reduce, for example with the Simpl
tactic (see below). The fix is reduced because the decreasing argument
(T_cons t) starts with a constructor.

In the case where the decreasing argument does not start with a
constructor (see how' below), then the only way I know is to proceed
by case.

Cheers,
Pierre


On Thu, 31 Oct 2002 17:42:57 +0100
Lionel Elie Mamane 
<lionel AT mamane.lu>
 wrote:
....
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)).
Simpl.
Intros t hyp.
Elim hyp.
Auto.
Save


Theorem How': (t:T)(x:..) (for_all P x)  -> (Q x).
Intros t x.
Case x.
...


-- 
Courtieu Pierre     
mailto:courtieu AT lri.fr
http://www.lri.fr/~courtieu
__________________________________________