|
(* simpl performs eta expansion *)
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)).
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.
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
