|
37
|
1 -title: 関数適用による証明
|
|
|
2
|
|
|
3 A → B → A
|
|
|
4
|
|
|
5 を証明してみよう。
|
|
|
6
|
|
|
7 まず、証明する式の上に線分を引く。これは「推論して、 A → B → A を導く」ということである。
|
|
|
8
|
|
|
9 ----------------
|
|
|
10 A → B → A
|
|
|
11
|
|
|
12 まず、かっこを正しく付ける。
|
|
|
13
|
|
|
14 --------------------
|
|
|
15 A → ( B → A )
|
|
|
16
|
|
|
17 であることを思い出そう。ここで使える推論規則は、
|
|
|
18
|
|
|
19 A
|
|
|
20 :
|
|
|
21 B
|
|
|
22 ------------ →-intro
|
|
|
23 A → B
|
|
|
24
|
|
|
25 である。これのBの部分が ( B → A ) になっている。これにより、Aを仮定として使って良くなる。つまり、
|
|
|
26
|
|
|
27 A
|
|
|
28
|
|
|
29 は無条件に使って良い。
|
|
|
30
|
|
|
31 A
|
|
|
32 :
|
|
|
33 B → A
|
|
|
34 --------------------
|
|
|
35 A → ( B → A )
|
|
|
36
|
|
|
37 : の部分は自分で埋める必要がある。
|
|
|
38
|
|
|
39 B → A
|
|
|
40
|
|
|
41 の部分に集中しよう。
|
|
|
42
|
|
|
43 --------------------
|
|
|
44 B → A
|
|
|
45
|
|
|
46 となる。同じ推論規則から、
|
|
|
47
|
|
|
48 B
|
|
|
49 :
|
|
|
50 A
|
|
|
51 --------------------
|
|
|
52 B → A
|
|
|
53
|
|
|
54 となる。A は無条件に使って良かった。まとめると、
|
|
|
55
|
|
|
56 A
|
|
|
57 --------------------
|
|
|
58 B → A
|
|
|
59 --------------------
|
|
|
60 A → ( B → A )
|
|
|
61
|
|
|
62 これで証明がつながった。→-intro は二回使ったので番号を付けて区別する。
|
|
|
63 →-intro が生成した仮定には同じ番号を付けて[]を付加する。これは、
|
|
|
64 discharge と呼ばれる。
|
|
|
65
|
|
|
66 [A]1
|
|
|
67 -------------------- →-intro 2
|
|
|
68 B → A
|
|
|
69 -------------------- →-intro 1
|
|
|
70 A → ( B → A )
|
|
|
71
|
|
|
72 [B]は使ってないが、使わなくて良い。これで証明が完成した。
|
|
|
73
|
|
|
74 B
|
|
|
75 :
|
|
|
76 A
|
|
|
77 -------------------- →-intro
|
|
|
78 B → A
|
|
|
79
|
|
|
80 は、a : A があった時に、λ (x : B) → a が B → A という型を持つことに相当する。
|
|
|
81
|
|
|
82 b : B
|
|
|
83 :
|
|
|
84 a : A
|
|
|
85 -------------------------------
|
|
|
86 λ (x : B) → a : B → A
|
|
|
87
|
|
|
88 : の左側は値であり、右側が型になる。
|
|
|
89
|
|
|
90 証明すべき式は、型
|
|
|
91 f : B → A
|
|
|
92
|
|
|
93
|
|
|
94
|
|
|
95
|
|
|
96
|
|
|
97
|
|
|
98
|
|
|
99
|
|
|
100
|
|
|
101
|
|
|
102 <a href="../s02/lambda.agda"> lambda.agda </a>
|
|
|
103
|
|
|
104
|
|
|
105
|
|
|
106 module lambda ( T : Set) ( t : T ) where
|
|
|
107
|
|
|
108
|
|
|
109 A→A : (A : Set ) → ( A → A )
|
|
|
110 A→A = λ A → λ ( a : A ) → a
|
|
|
111
|
|
|
112 lemma2 : (A : Set ) → A → A
|
|
|
113 lemma2 A a = {!!}
|
|
|
114
|
|
|
115
|
|
|
116 ex1 : {A B : Set} → Set
|
|
|
117 ex1 {A} {B} = ( A → B ) → A → B
|
|
|
118
|
|
|
119 ex2 : {A : Set} → Set
|
|
|
120 ex2 {A} = A → ( A → A )
|
|
|
121
|
|
|
122 ex3 : {A B : Set} → Set
|
|
|
123 ex3 {A}{B} = A → B
|
|
|
124
|
|
|
125 ex4 : {A B : Set} → Set
|
|
|
126 ex4 {A}{B} = A → B → B
|
|
|
127
|
|
|
128 ex5 : {A B : Set} → Set
|
|
|
129 ex5 {A}{B} = A → B → A
|
|
|
130
|
|
|
131 proof5 : {A B : Set } → ex5 {A} {B}
|
|
|
132 proof5 a b = a
|
|
|
133
|
|
|
134 postulate S : Set
|
|
|
135 postulate s : S
|
|
|
136
|
|
|
137 ex6 : {A : Set} → A → S
|
|
|
138 ex6 a = s
|
|
|
139
|
|
|
140 ex7 : {A : Set} → A → T
|
|
|
141 ex7 a = t
|
|
|
142
|
