natural-number-game

Solututions to the Natural Number Game

function.lean (1525B)

 1 example (P Q : Type) (p : P) (h : P → Q) : Q :=
 2 begin
 3   exact h(p),
 4 end
 5 
 6 example : ℕ → ℕ :=
 7 begin
 8   intro n,
 9   exact 3 * n + 2,
10 end
11 
12 example (P Q R S T U: Type)
13         (p : P)
14         (h : P → Q)
15         (i : Q → R)
16         (j : Q → T)
17         (k : S → T)
18         (l : T → U) : U :=
19 begin
20   have q := h(p),
21   have t := j(q),
22   exact l(t),
23 end
24 
25 example (P Q R S T U: Type)
26         (p : P)
27         (h : P → Q)
28         (i : Q → R)
29         (j : Q → T)
30         (k : S → T)
31         (l : T → U) : U :=
32 begin
33   have q := h(p),
34   have t := j(q),
35   exact l(t),
36 end
37 
38 example (P Q : Type) : P → (Q → P) :=
39 begin
40   intros p q,
41   exact p,
42 end
43 
44 example (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
45 begin
46   intros f g p,
47   apply f,
48   exact p,
49   apply g,
50   exact p,
51 end
52 
53 example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) :=
54   begin
55   intros f g p,
56   apply g,
57   apply f,
58   exact p,
59 end
60 
61 example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) :=
62 begin
63   intros f g p,
64   apply g,
65   apply f,
66   exact p,
67 end
68 
69 example (A B C D E F G H I J K L : Type) 
70         ( f1 : A → B) ( f2 : B → E) ( f3 : E → D) 
71         ( f4 : D → A) ( f5 : E → F) ( f6 : F → C)
72         ( f7 : B → C) ( f8 : F → G) ( f9 : G → J) 
73         (f10 : I → J) (f11 : J → I) (f12 : I → H) 
74         (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L :=
75 begin
76   intro a,
77   apply f15,
78   apply f11,
79   apply f9,
80   apply f8,
81   apply f5,
82   apply f2,
83   apply f1,
84   exact a,
85 end
86