Falsoを使ってみた?

あらまし

http://twitter.com/MoCo7/status/19336249733

MoCo7さんのretweetで発見

ティンと来た！！！

http://estatis.coders.fm/falso/

なんかCoqっぽいコードがあるけど何やってるか分かりません。

Agda2で

{-# OPTIONS --universe-polymorphism #-}

module Falso where

import Level
open import Data.Nat

data ⊥ : Set0 where

absurd : {n : Level.Level}{P : Set n} -> ⊥ -> P
absurd ()

data _==_ {n : Level.Level} {A : Set n} : A -> A -> Set n where
  refl : (a : A) -> a == a

data Falso {n : Level.Level} (P : Set n) : Set n where
  falso : ⊥ -> Falso P

falso→agda2 : {n : Level.Level}{P : Set n} -> Falso P -> P
falso→agda2 (falso b) = absurd b

postulate agda2→falso : {n : Level.Level}{P : Set n} -> P -> Falso P

¬ : {n : Level.Level} (P : Set n) -> Set n
¬ p = p -> ⊥

lem : {n1 n2 : Level.Level}{P : Set n1}{Q : Set n2} ->
      ((Falso P) -> Q) -> (P -> Q)
lem p→q = (λ p' → p→q (agda2→falso p'))

1==2 : 1 == 2
1==2 = proof
  where
    assume : Falso (¬ (1 == 2)) → ⊥
    assume (falso b) = b

    ¬¬1==2 : ¬(¬(1 == 2))
    ¬¬1==2 = lem assume

    お腹空いた : Falso (¬(¬(1 == 2)))
    お腹空いた = agda2→falso ¬¬1==2

    proof : 1 == 2
    proof with お腹空いた
    ... | (falso b) = absurd b

くそ暑いんですけど・・・。あとコレであってるのかなぁ・・・。

agda2→falsoは必要だと思うんですけど。