Egisonで定理証明

prover1.egins

-- Egison Version >= 3.10.0
-- $ egison -N
-- > loadFile "prover1.egins"



--
-- Matcher
--

nat := algebraicDataMatcher
  | o
  | s nat
  | x -- 変数もMatcherに登録する必要がある
  | add nat nat

bool := algebraicDataMatcher
  | falsee
  | trueee
  | eqn nat nat

expr := algebraicDataMatcher
  | ifte bool expr expr
  | b bool



--
-- Utils
--

proof x fs := match fs as list something with
  | []         -> x
  | $f :: $fss -> proof (f x) fss



--
-- Commands
--

-- X + O ≡ X
{-
input :=
  Ifte (Eqn X O)
    (B (Eqn (Add X O) X))
    (Ifte (Eqn (Add X O) X)
       (B (Eqn (Add (S X) O) (S X)))
       (B Trueee) )
-}
input := B (Eqn (Add X O) X)

-- #################### induction
induction := \match as expr with
  | b (eqn (add x o) x) -> Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B (Eqn (Add (S X) O) (S X))) (B Trueee) )
  | $z                  -> z
-- #################### induction

-- #################### add1Step
-- 実際の加法にするためには、値が変わらなくなるまでadd1Stepを適用する必要がある
add1StepNat := \match as nat with
  -- | o             -> O
  | s $n          -> S (add1StepNat n)
    -- 加法のルール
  | add o      $m -> add1StepNat m
  | add (s $n) $m -> S (Add (add1StepNat n) (add1StepNat m))
    -- 加法のルール
  | $z            -> z
add1StepBool := \match as bool with
  | eqn $n1 $n2 -> Eqn (add1StepNat n1) (add1StepNat n2)
  | $z          -> z
add1Step := \match as expr with
  | ifte $b $t $f -> Ifte (add1StepBool b) (add1Step t) (add1Step f)
  | b $b         -> B (add1StepBool b)
-- #################### add1Step

-- #################### equalIfN
equalIfNNat n1 n2 nn := match nn as nat with
  -- | #n1         -> n2 -- equalIfNBoolでやってる
  | s #n1       -> S n2
  | add #n1 #n1 -> Add n2 n2
  | add #n1 $m  -> Add n2 m
  | add $n  #n1 -> Add n n2
  | $z          -> z
equalIfNBool n1 n2 b := match b as bool with
  | eqn #n1 #n1 -> Eqn n2 n2
  | eqn #n1 $m  -> Eqn n2 (equalIfNNat n1 n2 m)
  | eqn $n  #n1 -> Eqn (equalIfNNat n1 n2 n) n2
  | eqn $n  $m  -> Eqn (equalIfNNat n1 n2 n) (equalIfNNat n1 n2 m)
  | $z          -> z
equalIfNSub n1 n2 e := match e as expr with
  | ifte $b $t $f -> Ifte b (equalIfNSub n1 n2 t) (equalIfNSub n1 n2 f)
  | b $b         -> B (equalIfNBool n1 n2 b)
equalIfN n1 n2 e := match e as expr with
  | ifte (eqn #n1 #n2) $t $f -> Ifte (Eqn n1 n2) (equalIfNSub n1 n2 t) f
  | ifte $b            $t $f -> Ifte b (equalIfN n1 n2 t) (equalIfN n1 n2 f)
  | $z                      -> z
-- #################### equalIfN

-- #################### equalSame
equalSameBool n b := match b as bool with
  | eqn #n #n -> Trueee
  | $z        -> z
equalSame n e := match e as expr with
  | ifte $b $t $f -> Ifte b (equalSame n t) (equalSame n f)
  | b $b         -> B (equalSameBool n b)
-- #################### equalSame

-- #################### ifSame
ifSame b1 e1 e := match e as expr with
  | ifte #b1 #e1 #e1 -> e1
  | ifte $b  $t  $f  -> Ifte b (ifSame b1 e1 t) (ifSame b1 e1 f)
  | $z              -> z
-- #################### ifSame



--
-- Tests
--
-- % egison -N -t prover1.egins

assertEqual "1.input"
  input
  (B (Eqn (Add X O) X))

assertEqual "2.induction"
  (induction input)
  (Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B (Eqn (Add (S X) O) (S X))) (B Trueee)))

assertEqual "3.add1Step_1"
  (add1Step (induction input))
  (Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B (Eqn (S (Add X O)) (S X))) (B Trueee)))

assertEqual "4.equalIfN_1"
  (equalIfN (Add X O) X (add1Step (induction input)))
  (Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B (Eqn (S X) (S X))) (B Trueee)))

assertEqual "5.equalSame_1"
  (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))
  (Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B Trueee) (B Trueee)))

assertEqual "6.ifSame_1"
  (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))
  (Ifte (Eqn X O) (B (Eqn (Add X O) X)) (B Trueee))

assertEqual "7.equalIfN_2"
  (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))))
  (Ifte (Eqn X O) (B (Eqn (Add O O) O)) (B Trueee))

assertEqual "8.add1Step_2"
  (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))))
  (Ifte (Eqn X O) (B (Eqn O O)) (B Trueee))

assertEqual "9.equalSame_2"
  (equalSame O (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))))))
  (Ifte (Eqn X O) (B Trueee) (B Trueee))

assertEqual "10.ifSame_2"
  (ifSame (Eqn X O) (B Trueee) (equalSame O (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))))))
  (B Trueee)

assertEqual "11.all"
  (proof (B (Eqn (Add X O) X))
    [induction,
     add1Step,
     (\e -> equalIfN (Add X O) X e),
     (\e -> equalSame (S X) e),
     (\e -> ifSame (Eqn (Add X O) X) (B Trueee) e),
     (\e -> equalIfN X O e),
     add1Step,
     (\e -> equalSame O e),
     (\e -> ifSame (Eqn X O) (B Trueee) e)])
  (B Trueee)

prover2_1.egins

-- > Egison Version == 3.10.0
-- > egison -N
-- > loadFile "prover2_1.egins"



--
-- Matcher
--

-- オリジナルのMatcher
nat := algebraicDataMatcher
  | o
  | s nat
  | x -- 変数もMatcherに登録する必要がある

listnat := algebraicDataMatcher
  | nil
  | cons nat listnat
  | l
  | rev listnat
  | snoc listnat nat
-- オリジナルのMatcher

-- オリジナルのMatcherを作った時は、omに追加する
om := algebraicDataMatcher
  | f string (list om)
  | n nat
  | ln listnat
-- オリジナルのMatcherを作った時は、omに追加する

bool := algebraicDataMatcher
  | falsee
  | trueee
  | eq om om

expr := algebraicDataMatcher
  | iff bool expr expr
  | b bool



--
-- Utils
--

proof x fs := match fs as list something with
  | []         -> x
  | $f :: $fss -> proof (f x) fss



--
-- Commands
--

-- rev (rev l) ≡ l
input := B (Eq (F "add" [N X, N O]) (N X))
-- input := B (Eql (Rev (Rev L)) L)

-- #################### induction
induction := \match as expr with
  | b (eq (f #"add" (n x :: n o :: [])) (n x))
      -> Iff (Eq (N X) (N O)) (B (Eq (F "add" [N X, N O]) (N X))) (Iff (Eq (F "add" [N X, N O]) (N X)) (B (Eq (F "add" [N (S X), N O]) (N (S X)))) (B Trueee) )
  | b (eql (rev (rev l)) l) -> Iff (Eqn X O) (B (Eqn (Add X O) X)) (Iff (Eqn (Add X O) X) (B (Eqn (Add (S X) O) (S X))) (B Trueee) )
  | $z                      -> z
-- #################### induction

add := \match as om with
  | f #"add" (n o       :: n $m2 :: []) -> N (add m2)
  | f #"add" (n (s $m1) :: n $m2 :: []) -> N (S (F "add" [N (add m1), N (add m2)]))
  | $z                                  -> z

-- #################### func1Step
func1StepBool ff b := match b as bool with
  | eq $o1 $o2 -> Eq (ff o1) (ff o2)
  | $z         -> z
func1Step ff e := match e as expr with
  | iff $b $t $f -> Iff (func1StepBool ff b) (func1Step ff t) (func1Step ff f)
  | b $b         -> B (func1StepBool ff b)
-- #################### func1Step

-- #################### equalIf
{-
equalIfNatを書くのだが、
例えばListの中のNatを書き換えるには、
(Ln $l)のlに潜らないといけない
-}
equalIfBool o1 o2 b := match b as bool with
  | eq #o1 #o1 -> Eq o2 o2
  | eq #o1 $m  -> Eq o2 m
  | eq $l  #o1 -> Eq l o2
  | $z         -> z
equalIfSub o1 o2 e := match e as expr with
  | iff $b $t $f -> Iff b (equalIfSub o1 o2 t) (equalIfSub o1 o2 f)
  | b $b         -> B (equalIfBool o1 o2 b)
equalIf o1 o2 e := match e as expr with
  | iff (eq #o1 #o2) $t $f -> Iff (Eq o1 o2) (equalIfSub o1 o2 t) f
  | iff $b           $t $f -> Iff b (equalIf o1 o2 t) (equalIf o1 o2 f)
  | $z                     -> z
-- #################### equalIf

-- #################### equalSame
equalSameBool o b := match b as bool with
  | eq #o #o -> Trueee
  | $z       -> z
equalSame o e := match e as expr with
  | iff $b $t $f -> Iff b (equalSame o t) (equalSame o f)
  | b $b         -> B (equalSameBool o b)
-- #################### equalSame

-- #################### ifSame
ifSame b1 e1 e := match e as expr with
  | iff #b1 #e1 #e1 -> e1
  | iff $b  $t  $f  -> Iff b (ifSame b1 e1 t) (ifSame b1 e1 f)
  | $z              -> z
-- #################### ifSame



--
-- Tests
--
-- > egison -N -t prover2_1.egins

assertEqual "1.input"
  input
  (B (Eq (F "add" [N X, N O]) (N X)))

assertEqual "2.induction"
  (induction input)
  (Iff (Eq (N X) (N O)) (B (Eq (F "add" [N X, N O]) (N X))) (Iff (Eq (F "add" [N X, N O]) (N X)) (B (Eq (F "add" [N (S X), N O]) (N (S X)))) (B Trueee)))

assertEqual "3.func1Step_1"
  (func1Step add (induction input))
  (Iff (Eq (N X) (N O))
    (B (Eq (F "add" [N X, N O]) (N X)))
    (Iff (Eq (F "add" [N X, N O]) (N X)) (B (Eq (N (S (F "add" [N X, N O]))) (N (S X)))) (B Trueee)) )

-- NG
assertEqual "4.equalIfN_1"
  (equalIf (F "add" [N X, N O]) (N X) (func1Step add (induction input)))
  (Iff (Eqn X O) (B (Eqn (Add X O) X)) (Iff (Eqn (Add X O) X) (B (Eqn (S X) (S X))) (B Trueee)))

assertEqual "5.equalSame_1"
  (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))
  (Iff (Eqn X O) (B (Eqn (Add X O) X)) (Iff (Eqn (Add X O) X) (B Trueee) (B Trueee)))

assertEqual "6.ifSame_1"
  (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))
  (Iff (Eqn X O) (B (Eqn (Add X O) X)) (B Trueee))

assertEqual "7.equalIfN_2"
  (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))))
  (Iff (Eqn X O) (B (Eqn (Add O O) O)) (B Trueee))

assertEqual "8.add1Step_2"
  (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))))
  (Iff (Eqn X O) (B (Eqn O O)) (B Trueee))

assertEqual "9.equalSame_2"
  (equalSame O (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))))))
  (Iff (Eqn X O) (B Trueee) (B Trueee))

assertEqual "10.ifSame_2"
  (ifSame (Eqn X O) (B Trueee) (equalSame O (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))))))
  (B Trueee)

assertEqual "11.all"
  (proof (B (Eqn (Add X O) X))
    [induction,
     add1Step,
     (\e -> equalIfN (Add X O) X e),
     (\e -> equalSame (S X) e),
     (\e -> ifSame (Eqn (Add X O) X) (B Trueee) e),
     (\e -> equalIfN X O e),
     add1Step,
     (\e -> equalSame O e),
     (\e -> ifSame (Eqn X O) (B Trueee) e)])
  (B Trueee)