読者です 読者をやめる 読者になる 読者になる

HOL Light vs PVS (3)

g `!n. 8 <= n ==> (?x y. n = 3 * x + 5 * y)` ;;
e( INDUCT_TAC );;
e( ARITH_TAC );;
e( REWRITE_TAC [LE] THEN REPEAT STRIP_TAC );;
e( EXISTS_TAC `1` THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC );;
e( FIRST_X_ASSUM (fun t -> FIRST_ASSUM (MP_TAC o (MATCH_MP t))) THEN STRIP_TAC );;
e( ASM_CASES_TAC `y = 0` );;
e( EXISTS_TAC `x - 3` THEN EXISTS_TAC `2` THEN ASM_ARITH_TAC );;
e( EXISTS_TAC `x + 2` THEN EXISTS_TAC `y - 1` THEN ASM_ARITH_TAC );;
f01:lemma
forall(n:nat): 8 <= n => exists(x,y:nat): n = 3 * x + 5 * y

%|- f01 : PROOF
%|- (spread (induct "n" 1)
%|-  ((ground)
%|-   (then (skeep*)
%|-    (spread (split)
%|-     ((then (skeep*)
%|-       (spread (case "y = 0")
%|-        ((spread (inst + "x - 3" "2") ((ground) (ground)))
%|-         (spread (inst + "x + 2" "y - 1") ((ground) (ground))))))
%|-      (then (inst 2 "1" "1") (ground)))))))
%|- QED

カットオフされない為の場合分け(y=0 のとき3<=x,および,not(y=0) のとき1<=y)について,HOL Light は黙って判ってくれますが,PVSは

f01.2.1.1.2 (TCC):   

[-1]  y = 0
[-2]  j = 3 * x + 5 * y
[-3]  8 <= j + 1
  |-------
{1}   x - 3 >= 0
f01.2.1.2.2 (TCC):   

[-1]  j = 3 * x + 5 * y
[-2]  8 <= j + 1
  |-------
{1}   y - 1 >= 0
[2]   y = 0

のように確認してきます.