Saturday, 14 April 2018

Agda の否定

前にもやったことあるんですが、また、勉強中です。

  http://seeker-s-eye.blogspot.jp/2017/03/agda.html

<,=,> の場合分けで、その計算型goto文を使うわけですが、

 data Tri {a b c} (A : Set a) (B : Set b) (C : Set c) :
      Set (a ⊔ b ⊔ c) where
  tri< : ( a :  A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
  tri≈ : (¬a : ¬ A) ( b :  B) (¬c : ¬ C) → Tri A B C
  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :  C) → Tri A B C

なので、ばっちり否定が入っていて。こいつで、場合分けしたら、tri≈ なら、それ以外の場合は出てこないはずなんですが、場合分けは出てきてしまう。

  checkEQ ( x y : ℕ ) -> ( eq : x ≡ y ) -> compare x y ≡ tri≈ _ _ _
  checkEQ x y refl with compare x y
  ... | tri≈ _ refl _ = refl
  ... | tri> _ neq gt = ?
  ... | tri< lt neq _ = ?

みたいにしたいわけだけど。いや、 x ≡ y なんだから、tri> とかは出てこないはずだろ?

Agda での否定は、

  ¬ A = A -> ⊥

みたいに定義されていて、対偶 ( ¬ B -> ¬ A ) は、

   ( B -> ⊥ ) -> ( A -> ⊥ )

ならしい。つまり、 B -> ⊥ と A の二つの入力がある。A -> B があれば、B -> ⊥ から、三段論法で、A -> ⊥ がでる。つまり、

   contraposition : (A -> B) -> ( B -> ⊥ ) -> ( A -> ⊥ )
   contraposition f g x = g ( f x )

というわけ。この逆方向( ( ¬ B -> ¬ A ) -> ( A -> B ) ) は直観主義論理では証明できないらしいです。

そういえば、否定からはなんでも出てくるのあったなと思い出した。

  ⊥-elim : ⊥ -> _

あ、そうか。

  ... | tri> _ neq gt = ?

の neq の型は、( x ≡ y -> ⊥ ) なので、neq ( refl ) は ⊥ になる。そこから、これで生成してやればよいのか。

    ... | tri> _ neq gt = ⊥-elim (neq refl)

う、うーん。なんか、かっこわるいんだけど。こんなものかな。if 文みたいにできないのかな。
Post a Comment