The Coq mailing list

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

Hello,

The following proof script only has definitions of type transformations and 
functions by induction on nat. Also the proof of the last lemma is by 
induction on nat. How can it be that the final Qed is not accepted but gives 
me the error message

Error: The term
 "fun (n : nat) (A : k0) =>
  eq_ind_r
    (fun l : list (Pow Bush n A) =>
     flat_map (fun x : Pow Bush n A => BushnToList n A x) l = nil)
    (refl_equal nil) (BushToList_bnil (Pow Bush n A))" has type
 "forall (n : nat) (A : k0),
  (fun l : list (Pow Bush n A) =>
   flat_map (fun x : Pow Bush n A => BushnToList n A x) l = nil)
    (BushToList (bnil (Pow Bush n A)))" while it is expected to have type
 "forall (n : nat) (A : k0), BushnToList (S n) A (bnil (Pow Bush n A)) = nil"

?

Thank you in advance,     Ralph
http://www.irit.fr/~Ralph.Matthes/


The script is as follows and has been tested for version 8.1pl3:

Set Implicit Arguments.
Require Import List.

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 Bush: k1.
Parameter BushToList: forall (A:k0), Bush A ->  list A.

Definition BushnToList (n:nat)(A:k0)(t:Pow Bush n A): list A.
Proof.
  intros.
  induction n.
  exact (t::nil).
  simpl in t.
  exact (flat_map IHn (BushToList t)).   (* flat_map from List *)
Defined.

Parameter bnil : forall (A:k0), Bush A.
Axiom BushToList_bnil: forall (A:k0), BushToList (bnil A) = nil(A:=A).

Lemma BushnToList_bnil (n:nat)(A:k0):
  BushnToList (S n) A (bnil (Pow Bush n A)) = nil.
Proof.
  intros.
  simpl.
  rewrite BushToList_bnil.
  simpl.
  reflexivity.
Qed.