PVSのこと（10）

　うらなりに見える Yices ですが．．．
http://d.hatena.ne.jp/ehito/searchdiary?word=%C3%E6%B4%D6%C3%CD
の例です．

lem1:lemma A(0)<x & (exists m:x<=A(m)) => (exists n:A(n)<x & x<=A(n+1))

%|- lem1 : PROOF
%|- (then (skosimp*)
%|-  (spread (case "(forall(n:nat):A(n)<x)")
%|-   ((yices) (then (induct "n" 1) (yices)))))
%|- QED

lem1 :  

  |-------
{1}   A(0) < x & (EXISTS m: x <= A(m)) => (EXISTS n: A(n) < x & x <= A(n + 1))
 
Repeatedly Skolemizing and flattening,
 this simplifies to:
lem1 :  

{-1}  A(0) < x
{-2}  x <= A(m!1)
  |-------
{1}   (EXISTS n: A(n) < x & x <= A(n + 1))
 
Case splitting on 
   (FORALL (n: nat): A(n) < x), 
 we get 2 subgoals:
lem1.1 :  

{-1}  (FORALL (n: nat): A(n) < x)
[-2]  A(0) < x
[-3]  x <= A(m!1)
  |-------
[1]   (EXISTS n: A(n) < x & x <= A(n + 1))
 
Simplifying with Yices,
 This completes the proof of lem1.1.

lem1.2 :  

[-1]  A(0) < x
[-2]  x <= A(m!1)
  |-------
{1}   (FORALL (n: nat): A(n) < x)
[2]   (EXISTS n: A(n) < x & x <= A(n + 1))
 
Inducting on n on formula 1,
lem1.2 :  

[-1]  A(0) < x
[-2]  x <= A(m!1)
  |-------
{1}   FORALL j: A(j) < x IMPLIES A(j + 1) < x
[2]   (EXISTS n: A(n) < x & x <= A(n + 1))
 
Simplifying with Yices,
 This completes the proof of lem1.2.

Q.E.D.

　最後の処理はさすがにlogic+arithといった所でしょう．

勿論，one line proof も出来ます．

% (then (case "(forall(n:nat):A(n)<x)") (yices) (induct-and-simplify "n" 1))

lem1 :  

  |-------
{1}   A(0) < x & (EXISTS m: x <= A(m)) => (EXISTS n: A(n) < x & x <= A(n + 1))
 
Case splitting on 
   (FORALL (n: nat): A(n) < x), 
 we get 2 subgoals:
lem1.1 :  

{-1}  (FORALL (n: nat): A(n) < x)
  |-------
[1]   A(0) < x & (EXISTS m: x <= A(m)) => (EXISTS n: A(n) < x & x <= A(n + 1))
 
Simplifying with Yices,
 This completes the proof of lem1.1.

lem1.2 :  

  |-------
{1}   (FORALL (n: nat): A(n) < x)
[2]   A(0) < x & (EXISTS m: x <= A(m)) => (EXISTS n: A(n) < x & x <= A(n + 1))
 
By induction on n, and by repeatedly rewriting and simplifying,
 This completes the proof of lem1.2.

Q.E.D.