ゲーデル・パズル in Idris

GoedelPuzzle.idr

-- 参考記事：https://qiita.com/41semicolon/items/530c0e5e4785728f7295
--
-- $ idris
-- > :l GoedelPuzzle
module GoedelPuzzle

%default total
%hide (++)


||| Append two lists
(++) : List a -> List a -> List a
(++) []      right = right
(++) (x::xs) right = x :: (xs ++ right)

namespace Gp1
  data Gsym = P | N | LP | RP | Neg
  Uninhabited (Gp1.Neg = Gp1.P) where
    uninhabited Refl impossible
  Gexp : Type
  Gexp = List Gsym
  Printer : Type
  Printer = Nat -> Gexp
  Printable : (p : Printer) -> (e : Gexp) -> Type
  Printable p e = (n : Nat ** p n = e)

  data EvalR : (p : Printer) -> (s : Gexp) -> Bool -> Type where
    TP1   : (e : Gexp) -> s =       [P,LP]++e++[RP] ->       Printable p e                  -> EvalR p s True
    TP2   : (e : Gexp) -> s =       [P,LP]++e++[RP] -> Not $ Printable p e                  -> EvalR p s False
    TPN1  : (e : Gexp) -> s =     [P,N,LP]++e++[RP] ->       Printable p (e++[LP]++e++[RP]) -> EvalR p s True
    TPN2  : (e : Gexp) -> s =     [P,N,LP]++e++[RP] -> Not $ Printable p (e++[LP]++e++[RP]) -> EvalR p s False
    TnP1  : (e : Gexp) -> s =   [Neg,P,LP]++e++[RP] ->       Printable p e                  -> EvalR p s False
    TnP2  : (e : Gexp) -> s =   [Neg,P,LP]++e++[RP] -> Not $ Printable p e                  -> EvalR p s True
    TnPN1 : (e : Gexp) -> s = [Neg,P,N,LP]++e++[RP] ->       Printable p (e++[LP]++e++[RP]) -> EvalR p s False -- この文s =「¬PN(e)」 が真でないが e(e) が印字可能であることを意味する
    TnPN2 : (e : Gexp) -> s = [Neg,P,N,LP]++e++[RP] -> Not $ Printable p (e++[LP]++e++[RP]) -> EvalR p s True

  -- 「文s を印字するならそれは全て True である」⇔「 False となる文は絶対に印字しない」
  -- はここ（かしこいプリンタ）で与えられる、としておこう
  CorrectPrinter : (p : Printer) -> Type
  CorrectPrinter p = (n : Nat) -> Not $ EvalR p (p n) False

  g : Gexp
  g = [Neg, P, N, LP, Neg, P, N, RP]

  -- lemma
  gTrueUnprintable : (p : Printer) -> CorrectPrinter p
    -> (Not $ Printable p Gp1.g, EvalR p Gp1.g True)
  gTrueUnprintable p cor = (\pt=> sub pt, (TnPN2 [Neg, P, N] Refl (\pt=> sub pt))) where
    sub pt with (pt)
      | (n ** eq) =
          let cor2 = replace {P=(\x=>(EvalR p x False -> Void))} eq (cor n) in cor2 (TnPN1 [Neg, P, N] Refl pt)
          -- 「かしこいプリンタ」に、引数から取り出した pt : Printable p g を食わせる

  -- theorem
  printerIncompleteness : (p : Printer) -> CorrectPrinter p
    -> (s : Gexp ** (Not $ Printable p s, EvalR p s True))
  printerIncompleteness p cor = (g ** (gTrueUnprintable p cor))


  -------------------- 補足 --------------------
  g0 : Gexp
  g0 = [P, N, LP, Neg, P, N, RP]

  aux : (p : Printer) -> CorrectPrinter p
    -> (e : Gexp) -> EvalR p (Neg::e) True -> EvalR p e False
  aux _ _ _ (TP1   _  eq _ ) = let inj = consInjective eq in absurd (fst inj)
  aux _ _ _ (TPN1  _  eq _ ) = let inj = consInjective eq in absurd (fst inj)
  aux _ _ _ (TnP2  e2 eq pt) = let inj = consInjective eq in TP2  e2 (snd inj) pt
  aux _ _ _ (TnPN2 e2 eq pt) = let inj = consInjective eq in TPN2 e2 (snd inj) pt

  -- 決定不能命題であることの証明
  gImpliesUndecidability : (p : Printer) -> CorrectPrinter p
    -> (Not $ Printable p Gp1.g0, Not $ Printable p (Neg::Gp1.g0))
  gImpliesUndecidability p cor = (\pt=> sub pt, (fst (gTrueUnprintable p cor))) where
    sub pt with (pt)
      | (n ** eq) =
          let cor2 = replace {P=(\x=>(EvalR p x False -> Void))} eq (cor n) in
          let aux2 = aux p cor g0 (snd (gTrueUnprintable p cor)) in cor2 aux2