higher-order prover のこと（２）

という訳で，高階論理自動定理証明界のホープ Satallax の登場です．

echo 'thf(type_x,type,x : $tType).
  thf(type_y,type,y : $tType).
  thf(f,type,f : x > y).
  thf(gl,conjecture, ((! [X1 : x, X2 : x] : (((f @ X1) = (f @ X2)) => (X1=X2))) <=>
    (? [G : y > x] : ! [X : x] : ((G @ (f @ X)) = X ) ))).'> demo1.p
satallax -p coqscript -c ./demo1.v ./demo1.p

のように，単射であることと左逆写像を持つこととが等価という性質を与えると，直ちに

% SZS status Theorem
% mode188 

と答えます．SZS status については

http://www.cs.miami.edu/~tptp/TPTP/TPTPTParty/2007/PositionStatements/GeoffSutcliffe_SZS.html

また，mode とは /usr/local/CAS/satallax-2.7/modes/（このパスは下記のリンクのようにインストールした場合のもの）に収められているストラテジーのことです．

そして，生成される Coq の証明スクリプトも

cat ./demo1.v

ご覧の通りです．

Add LoadPath "/usr/local/CAS/satallax-2.7/coq".
Require Import stttab.
Section SatallaxProblem.
Variable x:SType.
Variable y:SType.
Variable f : x --> y.
Theorem gl : (forall (X1:x) (X2:x), f X1 = f X2 -> X1 = X2) <-> (exists G:y --> x, forall (X:x), G (f X) = X).

tab_start H0.
tab_negiff H0 H1 H2.
 tab_negex H2 (fun (X1:y) => @Sepsilon x (fun (X2:x) => f X2 = X1)) H3.
 tab_negall H3 __1 H4.
 tab_all H1 (@Sepsilon x (fun (X1:x) => f X1 = f __1)) H5.
 tab_all H5 (__1) H6.
 tab_imp H6 H7.
  tab_choice x (fun (X1:x) => f X1 = f __1) H8.
   tab_all H8 (__1) H9.
   tab_refl H9.
   tab_conflict H8 H7.
  tab_conflict H7 H4.
 tab_negall H1 __2 H10.
 tab_negall H10 __3 H11.
 tab_negimp H11 H12 H13.
 tab_ex H2 __4 H14.
 tab_all H14 (__3) H15.
 tab_all H14 (__2) H16.
 tab_con H15 H13 H17 H18.
  tab_con H16 H17 H19 H20.
   tab_dec H19 H21.
    tab_conflict H12 H21.
   tab_conflict H16 H19.
  tab_conflict H15 H17.
Qed.
End SatallaxProblem.

Satallax のインストールなどは

http://www.knoppix-math.org/wiki/index.php?Satallax

に書きました．