The Coq mailing list

["Dimitri Hendriks" <Dimitri.Hendriks AT phil.uu.nl>]

hi,

you need to give a so-called elimination predicate (see manual) 
for this case-analysis. comp can be defined using case analysis
on f only. see the definition below.

    Reset Initial.

    Implicit Arguments On.

    Axiom obj : Set.
 
    Inductive arr: obj-> obj-> Set :=
      id: (x:obj)(arr x x)
    | ar: (x,y,z:obj)(arr y z)->(arr x z).

    Fixpoint comp [x,y,z:obj;f:(arr x y)]: (arr y z)->(arr x z) :=
    <[x,y:obj](arr y z)->(arr x z)>
    Cases f of
      (id m)       => [g:(arr m z)]g
     |(ar w a b h) => [g:(arr b z)](ar w (comp h g))
    end.

your definition returns f when g is of the form (id m),
the above definition amounts to the same thing.
instead of returning f at once, f is recursively descended
until (id m) is reached, then g is put.
thus, if g is of the form (id m'), we know that m=m', and
the result doesn't differ from the original f.
we can prove:

    Lemma f_comp_id_eq_f : (x,y:obj;f:(arr x y))(comp f (id y))=f.
    Proof.
    Induction f.
    Reflexivity.
    Intros. Simpl. Rewrite H. Reflexivity.
    Qed.

regards, dimitri