Idrisでラムゼーの有名なやつ、しかし…… - コラッツ予想がとけたらいいな2

失敗の記録です。

ラムゼーの有名なやつ　とは

「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」
というものです。

グラフ理論の言葉で言うと、
「完全6点グラフの各辺を赤か青に彩色したとき、どんな塗り分けに対しても、
赤一色の三角形か、青一色の三角形が存在する」
となります。

完全6点グラフの辺15本と、その論理式15個を引数にとり、
赤色三角形か青色三角形が存在する、というtheoremにした。

module Ramsey03

%default total


-- 頂点は A, B, C, D, E, F の6つ
data Vertex = A | B | C | D | E | F

-- 辺は未定義関数で、2つの頂点を取り、Bool値を返す
postulate edge : (v1, v2 : Vertex) -> Bool

syntax "RED" = False
syntax "BLUE" = True


lemma1 : edge A B = RED -> edge A C = RED -> edge A D = RED
  -> (b06, b10, b07 : Bool)
    -> edge B C = b06 -> edge C D = b10 -> edge B D = b07
      -> (v1 ** (v2 ** (v3 ** ((edge v1 v2) = (edge v2 v3), (edge v2 v3) = (edge v1 v3)) )))
-- A-B, A-C and B-C is RED.
lemma1 eAB eAC eAD  RED b10 b07  eBC eCD eBD  = (A ** (B ** (C ** (lemma1_1 eAB eBC, lemma1_2 eBC eAC) )))
  where
    lemma1_1 : edge A B = RED -> edge B C = RED -> edge A B = edge B C
    lemma1_1 eAB eBC = rewrite eAB in rewrite eBC in Refl
    lemma1_2 : edge B C = RED -> edge A C = RED -> edge B C = edge A C
    lemma1_2 eBC eAC = rewrite eBC in rewrite eAC in Refl
lemma1 eAB eAC eAD  BLUE b10 b07  eBC eCD eBD = ?lrhs_2

-- Aから出ている5本の辺(b01~b05)がどんな色でも、赤一色か青一色の三角形が存在する
ramsey : (b01, b02, b03, b04, b05,  b06, b07, b08, b09, b10, b11, b12, b13, b14, b15 : Bool)
  -> edge A B = b01 -> edge A C = b02 -> edge A D = b03 -> edge A E = b04 -> edge A F = b05
                    -> edge B C = b06 -> edge B D = b07 -> edge B E = b08 -> edge B F = b09
                                      -> edge C D = b10 -> edge C E = b11 -> edge C F = b12
                                                        -> edge D E = b13 -> edge D F = b14
                                                                          -> edge E F = b15
    -> (v1 ** (v2 ** (v3 ** ((edge v1 v2) = (edge v2 v3), (edge v2 v3) = (edge v1 v3)) )))
      -- A-B, A-C, A-D is RED.
ramsey RED RED RED b04 b05  b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = lemma1 eAB eAC eAD  b06 b10 b07  eBC eCD eBD
ramsey RED RED BLUE b04 b05   b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = ?rhs_2
ramsey RED BLUE b03 b04 b05     b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = ?rhs_3
ramsey BLUE b02 b03 b04 b05       b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = ?rhs_4

途中まで作ったところでギブした。
全部作ったらこの5倍以上のコード量になるだろう。
これはあかんでしょ。

Egisonでは数十行でできたのに、なんでや？！
設計方針が悪いのかなあ。
.
.

ラムゼーの有名なやつ とは

ラムゼーの有名なやつ　とは