-title: 関数適用による証明

    A → B → A

を証明してみよう。

まず、証明する式の上に線分を引く。これは「推論して、 A → B → A を導く」ということである。

 ----------------
    A → B → A

まず、かっこを正しく付ける。

 --------------------
    A → ( B → A )

であることを思い出そう。ここで使える推論規則は、

      A
      :
      B
 ------------ →-intro
    A →  B

である。これのBの部分が ( B → A ) になっている。これにより、Aを仮定として使って良くなる。つまり、

     A

は無条件に使って良い。

         A
         :
       B → A 
 --------------------
    A → ( B → A )

: の部分は自分で埋める必要がある。

       B → A 

の部分に集中しよう。

 --------------------
       B → A 

となる。同じ推論規則から、

         B
         :
         A
 --------------------
       B → A 

となる。A は無条件に使って良かった。まとめると、

         A
 --------------------
       B → A 
 --------------------
    A → ( B → A )

これで証明がつながった。→-intro は二回使ったので番号を付けて区別する。
→-intro が生成した仮定には同じ番号を付けて[]を付加する。これは、
discharge と呼ばれる。

        [A]1
 -------------------- →-intro 2
       B → A 
 -------------------- →-intro 1
    A → ( B → A )

[B]は使ってないが、使わなくて良い。これで証明が完成した。

         B 
         :
         A 
 -------------------- →-intro 
       B → A

は、a : A があった時に、λ (x : B) → a が B → A という型を持つことに相当する。

     b : B 
         :
     a :  A 
 ------------------------------- 
     λ (x : B) → a :  B → A

: の左側は値であり、右側が型になる。

証明すべき式は、型
    f :  B → A










<a href="../s02/lambda.agda"> lambda.agda </a>



module lambda ( T : Set) ( t : T ) where


A→A : (A : Set ) → ( A → A )
A→A = λ A → λ ( a : A ) → a

lemma2 : (A : Set ) →  A → A 
lemma2 A a = {!!}


ex1 : {A B : Set} → Set 
ex1 {A} {B} = ( A → B ) → A → B

ex2 : {A : Set} → Set 
ex2 {A}  =  A → ( A  → A )

ex3 : {A B : Set} → Set 
ex3 {A}{B}  =  A → B

ex4 : {A B : Set} → Set 
ex4 {A}{B}  =  A → B → B

ex5 : {A B : Set} → Set 
ex5 {A}{B}  =  A → B → A

proof5 : {A B : Set } → ex5 {A} {B}
proof5 a b = a 

postulate S : Set
postulate s : S

ex6 : {A : Set} → A → S
ex6 a = s

ex7 : {A : Set} → A → T
ex7 a = t