|
266
|
1 module lambda ( A B : Set) (a : A ) (b : B ) where
|
|
138
|
2
|
|
266
|
3 -- λ-intro
|
|
|
4 --
|
|
|
5 -- A
|
|
|
6 -- -------- id
|
|
|
7 -- A
|
|
|
8 -- -------- λ-intro ( = λ ( x : A ) → x )
|
|
|
9 -- A → A
|
|
|
10
|
|
|
11 A→A : A → A
|
|
|
12 A→A = λ ( x : A ) → x
|
|
|
13
|
|
|
14 A→A'' : A → A
|
|
|
15 A→A'' = λ x → x
|
|
138
|
16
|
|
266
|
17 A→A' : A → A
|
|
|
18 A→A' x = x
|
|
|
19
|
|
|
20 lemma2 : (A : Set ) → A → A -- これは A → ( A → A ) とは違う
|
|
330
|
21 lemma2 = ?
|
|
|
22
|
|
|
23 lemma3 : {A B : Set } → B → ( A → B ) -- {} implicit variable
|
|
|
24 lemma3 b = λ _ → b -- _ anonymous variable
|
|
266
|
25
|
|
330
|
26 -- λ-intro
|
|
|
27 --
|
|
|
28 -- a : A
|
|
|
29 -- : f : A → B
|
|
|
30 -- b : B
|
|
|
31 -- ------------- f
|
|
|
32 -- A → B
|
|
139
|
33
|
|
266
|
34 -- λ-elim
|
|
|
35 --
|
|
330
|
36 -- a : A f : A → B
|
|
|
37 -- ------------------------ λ-elim
|
|
|
38 -- f a : B
|
|
266
|
39
|
|
|
40 →elim : A → ( A → B ) → B
|
|
139
|
41 →elim a f = f a
|
|
138
|
42
|
|
|
43 ex1 : {A B : Set} → Set
|
|
266
|
44 ex1 {A} {B} = {!!} -- ( A → B ) → A → B
|
|
138
|
45
|
|
|
46 ex2 : {A : Set} → Set
|
|
|
47 ex2 {A} = A → ( A → A )
|
|
|
48
|
|
141
|
49 proof2 : {A : Set } → ex2 {A}
|
|
266
|
50 proof2 {A} = {!!} where
|
|
|
51 p1 : {!!} --- ex2 {A} を C-C C-N する
|
|
|
52 p1 = {!!}
|
|
138
|
53
|
|
266
|
54 ex3 : A → B -- インチキの例
|
|
141
|
55 ex3 a = {!!}
|
|
138
|
56
|
|
266
|
57 ex4 : {A B : Set} → A → (B → B) -- 仮定を無視してる
|
|
|
58 ex4 {A}{B} a b = b
|
|
|
59
|
|
|
60 --- [A]₁ not used --- a
|
|
|
61 --- ────────────────────
|
|
|
62 --- [B]₂ --- b
|
|
|
63 --- ──────────────────── (₂)
|
|
|
64 --- B → B
|
|
|
65 --- ──────────────────── (₁) λ-intro
|
|
|
66 --- A → (B → B)
|
|
|
67
|
|
|
68
|
|
|
69 ex4' : A → (B → B) -- インチキできる / 仮定を使える
|
|
|
70 ex4' = {!!}
|
|
138
|
71
|
|
141
|
72 ex5 : {A B : Set} → A → B → A
|
|
|
73 ex5 = {!!}
|
|
138
|
74
|
|
|
75
|
|
|
76
|
|
141
|
77 postulate
|
|
266
|
78 Domain : Set -- Range Domain : Set
|
|
|
79 Range : Set -- codomain Domain → Range, coRange ← coDomain
|
|
141
|
80 r : Range
|
|
|
81
|
|
|
82 ex6 : Domain → Range
|
|
138
|
83 ex6 a = {!!}
|
|
|
84
|
|
|
85
|
|
266
|
86 --- A → B
|
|
|
87 -- :
|
|
|
88 --- A → B
|
|
|
89 --- ───────────────────────────
|
|
|
90 --- ( A → B ) → A → B
|
|
|
91 ---
|
|
|
92 --- [A]₁ [A → B ]₂
|
|
|
93 --- ─────────────────────────── λ-elim
|
|
|
94 --- B
|
|
|
95 --- ─────────────────────────── ₁
|
|
|
96 --- A → B
|
|
|
97 --- ─────────────────────────── ₂
|
|
|
98 --- ( A → B ) → A → B
|
|
|
99
|
|
|
100 --
|
|
|
101 -- 上の二つの図式に対応する二つの証明に対応するラムダ項がある
|
|
|
102 --
|
|
|
103 ex11 : ( A → B ) → A → B
|
|
|
104 ex11 = {!!}
|
|
138
|
105
|
|
|
106 ex12 : (A B : Set) → ( A → B ) → A → B
|
|
|
107 ex12 = {!!}
|
|
|
108
|
|
|
109 ex13 : {A B : Set} → ( A → B ) → A → B
|
|
|
110 ex13 {A} {B} = {!!}
|
|
|
111
|
|
|
112 ex14 : {A B : Set} → ( A → B ) → A → B
|
|
|
113 ex14 x = {!!}
|
|
|
114
|
|
|
115
|
