3*3魔方陣は1種類しか存在しない

magicSquare-N.egi

;; > egison -N
;; > loadFile("magicSquare-N.egi")

;; 3*3 Magic square
;; a b c
;; d e f
;; g h i

input =
  matchAll 1..9 as multiset(integer)
    | $xs <++> $ys -> [xs, ys]

;; ----- no use -----
filterFive =
  matchAll input as multiset(list(list(integer)))
    | ((
         (loop($i, (1, [5], _), <cons $z_i ...>, <nil>) and $xs)
         <:> ($ys <:> _)
       ) <:> _) -> [xs, ys]
pattOK =
  8#patternFunction([h],
    (?(15 == %1 + %2 + %3) and
     ?(15 == %4 + %5 + %6) and
     ?(15 == %7 + 'h + %8) and
     ?(15 == %1 + %4 + %7) and
     ?(15 == %2 + %5 + 'h) and
     ?(15 == %3 + %6 + %8) and
     ?(15 == %1 + %5 + %8) and
     ?(15 == %3 + %5 + %7))
  )
;; ----- no use -----

ok?(a, b, c, d, e, f, g, h, i) =
  if ((15 == a + b + c) &&
      (15 == d + e + f) &&
      (15 == g + h + i) &&
      (15 == a + d + g) &&
      (15 == b + e + h) &&
      (15 == c + f + i) &&
      (15 == a + e + i) &&
      (15 == c + e + g)) then #t else #f

;; 1時間走らせても終わらない……
makeMagic =
  unique(
    matchAll input as multiset(list(multiset(integer)))
      | ((
            (loop($i, (1, [5], _), <cons $z_i ...>, <nil>) and $xs)
            <:> (
                  (($b <:> ($d <:> ($f <:> ($h <:> <nil>)))) and $ys)
  ;;                (($b <:> ($d <:> ($f <:> (pattOK(z_2, b, z_3, d, z_1, f, z_4, z_5)[$h] <:> <nil>)))) and $ys)
                <:> _)
         ) <:> _) -> if ok?(z_2, b, z_3, d, z_1, f, z_4, h, z_5) then [xs, ys] else []
  )

MagicSquare.hs

module MagicSquare where

import Data.List (permutations)


{--
    3*3 Magic square
    a b c
    d e f
    g h i
--}

makeMagic :: [[Int]] -> [[Int]]
makeMagic = filter isMatch
  where
    isMatch xs =
      (15 == a + b + c) &&
      (15 == d + e + f) &&
      (15 == g + h + i) &&
      (15 == a + d + g) &&
      (15 == b + e + h) &&
      (15 == c + f + i) &&
      (15 == a + e + i) &&
      (15 == c + e + g)
        where
          a = head xs
          b = xs !! 1
          c = xs !! 2
          d = xs !! 3
          e = xs !! 4
          f = xs !! 5
          g = xs !! 6
          h = xs !! 7
          i = xs !! 8

-- *MagicSquare> answer1
-- [[2,9,4,7,5,3,6,1,8],[2,7,6,9,5,1,4,3,8],[8,3,4,1,5,9,6,7,2],[8,1,6,3,5,7,4,9,2],[4,9,2,3,5,7,8,1,6],[4,3,8,9,5,1,2,7,6],[6,7,2,1,5,9,8,3,4],[6,1,8,7,5,3,2,9,4]]
answer1 :: [[Int]]
answer1 = (makeMagic . permutations) [1..9]

-- ----- 回転・鏡映を同一視する(二面体群D4) -----
newtype D4 = D4 { getD4 :: (Int, Int, Int, Int, Int, Int, Int, Int, Int) } deriving (Show)

instance Eq D4 where
  D4 (a, b, c, d, e, f, g, h, i) == D4 (a', b', c', d', e', f', g', h', i') =
    (a == a' && b == b' && c == c' && d == d' && e == e' && f == f' && g == g' && h == h' && i == i') || -- 単位元　　を施したもの
    (a == c' && b == f' && c == i' && d == b' && e == e' && f == h' && g == a' && h == d' && i == g') || --  90°回転 を施したもの
    (a == i' && b == h' && c == g' && d == f' && e == e' && f == d' && g == c' && h == b' && i == a') || -- 180°回転 を施したもの
    (a == g' && b == d' && c == a' && d == h' && e == e' && f == b' && g == i' && h == f' && i == c') || -- 270°回転 を施したもの
    (a == c' && b == b' && c == a' && d == f' && e == e' && f == d' && g == i' && h == h' && i == g') || -- 鏡映1　　 を施したもの
    (a == i' && b == f' && c == c' && d == h' && e == e' && f == b' && g == g' && h == d' && i == a') || -- 鏡映2　　 を施したもの
    (a == g' && b == h' && c == i' && d == d' && e == e' && f == f' && g == a' && h == b' && i == c') || -- 鏡映3　　 を施したもの
    (a == a' && b == d' && c == g' && d == b' && e == e' && f == h' && g == c' && h == f' && i == i')    -- 鏡映4　　 を施したもの

toD4 :: [Int] -> D4
toD4 (a:b:c:d:e:f:g:h:i:_) = D4 (a, b, c, d, e, f, g, h, i)

checkD4 :: D4 -> Bool
checkD4 x = D4 (2, 9, 4, 7, 5, 3, 6, 1, 8) == x

-- *MagicSquare> answer2
-- [True,True,True,True,True,True,True]
answer2 :: [Bool]
answer2 = map (checkD4 . toD4) $ tail answer1

MagicSquare.idr

module MagicSquare

%default total


-- 参考記事：https://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q1399517918
{--
    3*3 Magic square
    a b c
    d e f
    g h i
--}


namespace Y
  postulate a : Nat
  postulate b : Nat
  postulate c : Nat
  postulate d : Nat
  postulate e : Nat
  postulate f : Nat
  postulate g : Nat
  postulate h : Nat
  postulate i : Nat

postulate fif1 : Y.a + Y.b + Y.c = 15
postulate fif2 : Y.d + Y.e + Y.f = 15
postulate fif3 : Y.g + Y.h + Y.i = 15
postulate fif4 : Y.a + Y.d + Y.g = 15
postulate fif5 : Y.b + Y.e + Y.h = 15
postulate fif6 : Y.c + Y.f + Y.i = 15
postulate fif7 : Y.a + Y.e + Y.i = 15
postulate fif8 : Y.c + Y.e + Y.g = 15

-- 登場回数appearC, appearN
appearC : Char -> Nat
appearC c = length $ elemIndices c
  ['a','b','c', 'd','e','f', 'g','h','i',  'a','d','g', 'b','e','h', 'c','f','i',  'a','e','i', 'c','e','g']

appearN : Nat -> Nat
appearN x = length $ elemIndices x
  [2,9,4, 7,5,3, 6,1,8,  2,7,6, 9,5,1, 4,3,8,  2,5,8, 4,5,6]

-- appearPostu2, appearPostu3で回転と鏡映を封じる
postulate appearPostu1 : appearC 'e' = 4 -> appearN 5 = 4 -> Y.e = 5
postulate appearPostu2 : appearC 'a' = 3 -> appearN 2 = 3 -> Y.a = 2
postulate appearPostu3 : appearC 'c' = 3 -> appearN 4 = 3 -> Y.c = 4


-- ----- proof -----
decisionE : Y.e = 5
decisionE = appearPostu1 Refl Refl

decisionA : Y.a = 2
decisionA = appearPostu2 Refl Refl

decisionC : Y.c = 4
decisionC = appearPostu3 Refl Refl

decisionB : Y.a + Y.b + Y.c = 15 -> Y.b = 9
decisionB =
  rewrite decisionA in
    rewrite decisionC in
      rewrite plusCommutative b 4 in
        \prf=> succInjective b 9 $
          succInjective (S b) 10 $
            succInjective (S (S b)) 11 $
              succInjective (S (S (S b))) 12 $
                succInjective (S (S (S (S b)))) 13 $
                  succInjective (S (S (S (S (S b))))) 14 prf

decisionI : Y.a + Y.e + Y.i = 15 -> Y.i = 8
decisionI =
  rewrite decisionA in
    rewrite decisionE in
      \prf=> succInjective i 8 $
        succInjective (S i) 9 $
          succInjective (S (S i)) 10 $
            succInjective (S (S (S i))) 11 $
              succInjective (S (S (S (S i)))) 12 $
                succInjective (S (S (S (S (S i))))) 13 $
                  succInjective (S (S (S (S (S (S i)))))) 14 prf

decisionG : Y.c + Y.e + Y.g = 15 -> Y.g = 6
decisionG =
  rewrite decisionC in
    rewrite decisionE in
      \prf=> succInjective g 6 $
        succInjective (S g) 7 $
          succInjective (S (S g)) 8 $
            succInjective (S (S (S g))) 9 $
              succInjective (S (S (S (S g)))) 10 $
                succInjective (S (S (S (S (S g))))) 11 $
                  succInjective (S (S (S (S (S (S g)))))) 12 $
                    succInjective (S (S (S (S (S (S (S g))))))) 13 $
                      succInjective (S (S (S (S (S (S (S (S g)))))))) 14 prf

decisionD : Y.a + Y.d + Y.g = 15 -> Y.d = 7
decisionD =
  rewrite decisionA in
    rewrite decisionG fif8 in
      rewrite plusCommutative d 6 in
        \prf=> succInjective d 7 $
          succInjective (S d) 8 $
            succInjective (S (S d)) 9 $
              succInjective (S (S (S d))) 10 $
                succInjective (S (S (S (S d)))) 11 $
                  succInjective (S (S (S (S (S d))))) 12 $
                    succInjective (S (S (S (S (S (S d)))))) 13 $
                      succInjective (S (S (S (S (S (S (S d))))))) 14 prf

decisionF : Y.c + Y.f + Y.i = 15 -> Y.f = 3
decisionF =
  rewrite decisionC in
    rewrite decisionI fif7 in
      rewrite plusCommutative f 8 in
        \prf=> succInjective f 3 $
          succInjective (S f) 4 $
            succInjective (S (S f)) 5 $
              succInjective (S (S (S f))) 6 $
                succInjective (S (S (S (S f)))) 7 $
                  succInjective (S (S (S (S (S f))))) 8 $
                    succInjective (S (S (S (S (S (S f)))))) 9 $
                      succInjective (S (S (S (S (S (S (S f))))))) 10 $
                        succInjective (S (S (S (S (S (S (S (S f)))))))) 11 $
                          succInjective (S (S (S (S (S (S (S (S (S f))))))))) 12 $
                            succInjective (S (S (S (S (S (S (S (S (S (S f)))))))))) 13 $
                              succInjective (S (S (S (S (S (S (S (S (S (S (S f))))))))))) 14 prf

decisionH : Y.b + Y.e + Y.h = 15 -> Y.h = 1
decisionH =
  rewrite decisionE in
    rewrite decisionB fif1 in
      \prf=> succInjective h 1 $
        succInjective (S h) 2 $
          succInjective (S (S h)) 3 $
            succInjective (S (S (S h))) 4 $
              succInjective (S (S (S (S h)))) 5 $
                succInjective (S (S (S (S (S h))))) 6 $
                  succInjective (S (S (S (S (S (S h)))))) 7 $
                    succInjective (S (S (S (S (S (S (S h))))))) 8 $
                      succInjective (S (S (S (S (S (S (S (S h)))))))) 9 $
                        succInjective (S (S (S (S (S (S (S (S (S h))))))))) 10 $
                          succInjective (S (S (S (S (S (S (S (S (S (S h)))))))))) 11 $
                            succInjective (S (S (S (S (S (S (S (S (S (S (S h))))))))))) 12 $
                              succInjective (S (S (S (S (S (S (S (S (S (S (S (S h)))))))))))) 13 $
                                succInjective (S (S (S (S (S (S (S (S (S (S (S (S (S h))))))))))))) 14 prf

answer : (Y.a = 2, Y.b = 9, Y.c = 4, Y.d = 7, Y.e = 5, Y.f = 3, Y.g = 6, Y.h = 1, Y.i = 8)
answer =
  (decisionA, decisionB fif1, decisionC, decisionD fif4, decisionE, decisionF fif6, decisionG fif8, decisionH fif5, decisionI fif7)

magicSquare3-N.egi

;; > egison -N
;; > loadFile("magicSquare3-N.egi")

;; 3*3 Magic square
;; a b c
;; d e f
;; g h i

fif?(x, y, z) = x + y + z == 15

;; ## 第一段階
fifteen = matchAll 1..9 as multiset(integer)
  | $x <:> $y <:> (?fif?(x, y, $) and $z) <:> _ -> [x, y, z]

;; ## 第二段階
fifTriple = matchAll fifteen as multiset(list(integer))
  | $xs <:> $ys <:> $zs <:> _ -> [xs, ys, zs]

mMSub?(a, b, c, d, e, f, g, h, i) =
  (a + d + g == 15) &&
  (b + e + h == 15) &&
  (c + f + i == 15) &&
  (a + e + i == 15) &&
  (c + e + g == 15) &&
  (not (a == d)) && (not (a == e)) && (not (a == f)) &&
  (not (a == g)) && (not (a == h)) && (not (a == i)) &&
  (not (d == g)) && (not (d == h)) && (not (d == i))

;; ## 第三段階
makeMagic = matchAll fifTriple as multiset(list(list(integer)))
  | ((($a <:> $b <:> $c <:> <nil>) <:>
      ($d <:> $e <:> $f <:> <nil>) <:>
      ($g <:> $h <:> ?mMSub?(a, b, c, d, e, f, g, h, $) <:> <nil>) <:>
      <nil>) and $xs) <:> _ -> xs

magicSquare4-N.egi

;; > egison -N
;; > loadFile("magicSquare4-N.egi")

;; 3*3 Magic square
;; a b c
;; d e f
;; g h i


;; ## 第一段階
def fif? = 3#(%1 + %2 + %3 == 15)
def fifteen = unique/m(multiset(integer),
  matchAll 1..9 as multiset(integer)
    | $x <:> $y <:> (?fif?(x, y, $) and $z) <:> _ -> [x, y, z] )


;; ## 第二段階
def myMultiset(a) = matcher
  | <triCons $ $ $ $> as (a, a, a, myMultiset(a)) ->
    | $tgt -> matchAll tgt as multiset(a)
                | ($x <:> $y <:> $z <:> $ts) -> (x, y, z, ts)
  | $ as (something) ->
    | $tgt -> {tgt}

def mMSub?(a, b, c, d, e, f, g, h, i) =
  (a + d + g == 15) &&
  (b + e + h == 15) &&
  (c + f + i == 15) &&
  (a + e + i == 15) &&
  (c + e + g == 15) &&
  (not (a == d)) && (not (a == e)) && (not (a == f)) &&
  (not (a == g)) && (not (a == h)) && (not (a == i)) &&
  (not (d == g)) && (not (d == h)) && (not (d == i))

;; > loadFile("magicSquare4-N.egi")
;; > makeMagic
;; {{{8 1 6} {3 5 7} {4 9 2}} {{6 1 8} {7 5 3} {2 9 4}} {{6 7 2} {1 5 9} {8 3 4}} {{2 7 6} {9 5 1} {4 3 8}}
;;  {{4 9 2} {3 5 7} {8 1 6}} {{2 9 4} {7 5 3} {6 1 8}} {{8 3 4} {1 5 9} {6 7 2}} {{4 3 8} {9 5 1} {2 7 6}}}
def makeMagic =
  matchAll fifteen as myMultiset(multiset(integer))
    | <triCons
        ($a <:> $b <:> $c <:> <nil>)
        ($d <:> $e <:> $f <:> <nil>)
        ($g <:> $h <:> (?mMSub?(a, b, c, d, e, f, g, h, $) and $i) <:> <nil>) _> ->
          [[a, b, c], [d, e, f], [g, h, i]]