blob: 7f6bca59d27080cf016c96eca47914c6961128dd (
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
Require Export Crypto.Util.FixCoqMistakes.
Section tower_nd.
Context (A : Type).
Section with_B.
Context (B : Type).
Fixpoint tower_nd (n : nat)
:= match n with
| 0 => B
| S n' => A -> tower_nd n'
end.
End with_B.
Section with_B2.
Context (B B' : Type) (f : B -> B').
Fixpoint impl_under_tower_nd (n : nat)
: tower_nd B n -> tower_nd B' n
:= match n with
| 0 => f
| S n' => fun t x => impl_under_tower_nd n' (t x)
end.
End with_B2.
End tower_nd.
Definition apply4 {AK BK PA PB ARR}
(F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B))
{A0 A1 A2 A3 : AK} {B : BK}
(f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PB B)
: PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 B)))).
Proof.
repeat (apply F; intro); apply f; assumption.
Defined.
Definition apply4_nd {BK PA PB ARR}
(F : forall (B : BK), (PA -> PB B) -> PB (ARR B))
{B : BK}
(f : tower_nd PA (PB B) 4)
: PB (ARR (ARR (ARR (ARR B))))
:= @apply4 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F)
tt tt tt tt B f.
Definition apply9 {AK BK PA PB ARR}
(F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B))
{A0 A1 A2 A3 A4 A5 A6 A7 A8 : AK} {B : BK}
(f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PA A4 -> PA A5 -> PA A6 -> PA A7 -> PA A8 -> PB B)
: PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 (ARR A4 (ARR A5 (ARR A6 (ARR A7 (ARR A8 B))))))))).
Proof.
repeat (apply F; intro); apply f; assumption.
Defined.
Definition apply9_nd {BK PA PB ARR}
(F : forall (B : BK), (PA -> PB B) -> PB (ARR B))
{B : BK}
(f : tower_nd PA (PB B) 9)
: PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B)))))))))
:= @apply9 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F)
tt tt tt tt tt tt tt tt tt B f.
|
