The Coq mailing list

[Ralph Matthes <Ralph.Matthes AT irit.fr>]

Hello,

Using observations by Ulrich Schöpp on my original question of yesterday, the
problem can be simplified as follows and more clearly points to the error 
introduced by simpl:

(no import statement needed, no implicit arguments used)

Definition k0 := Set.
Definition k1 := k0 -> k0.

(** iterating X n times *)
Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
  match k with 0 => fun X => X
             |  S k' => fun A => X (Pow X k' A)   
  end.

Parameter T M: k1.
Parameter TToM: forall (A:k0), T A ->  M A.
Parameter ret: forall A:k0, A -> M A.
Parameter bind: forall(A B:k0), (A -> M B) -> M A -> M B.

Definition TnToM (n:nat)(A:k0)(t:Pow T n A): M A.
Proof.
  intros.
  induction n.
  exact (ret A t).
  exact (bind (Pow T n A) A IHn (TToM (Pow T n A) t)).
Defined.

Lemma TnToMSn (n:nat)(A:k0)(t:Pow T (S n) A):
  TnToM (S n) A t = bind (Pow T n A) A (fun x : Pow T n A => TnToM n A x)
  (TToM (Pow T n A) t).
Proof.
  intros.
(* unfold TnToM. *)
  simpl.
  reflexivity.
Qed.   (* fails! *)

(* If one does the unfold TnToM before simpl, it becomes clear
    that there is an additional eta-expansion in the right-hand side. 
    Is this related to the bug discussed at
    http://pauillac.inria.fr/pipermail/coq-club/2004/001317.html
    ?
*)