blob: be0e8ae8ba2a307965846e2d8e722da2f814b4d7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
(* 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.
|
