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 文みたいにできないのかな。