PVSのこと（11）

　PVS にはカユイところに手が届く帰納法が色々と用意されています．例えば

subrange_inductions[i: int, j: upfrom(i)]: THEORY
 BEGIN
  k: VAR subrange(i, j)
  p: VAR pred[subrange(i, j)]

  subrange_induction: LEMMA
    (p(i) AND (FORALL k: k < j AND p(k) IMPLIES p(k + 1)))
        IMPLIES (FORALL k: p(k))

 END subrange_inductions

　これを用いると…

s:int
t:upfrom(s)
x:real
C:[int->real]

lem3:lemma C(s)<x & x<=C(t) => (exists(n:subrange(s,t)):C(n)<x & x<=C(n+1))

%|- lem3 : PROOF
%|- (spread (case "(forall(n:subrange(s,t)):C(n)<x)")
%|-  ((yices) (then (rewrite "subrange_induction") (yices))))
%|- QED

lem3 :  

  |-------
{1}   C(s) < x & x <= C(t) => (EXISTS (n: subrange(s, t)): C(n) < x & x <= C(n + 1))
 
Case splitting on 
   (FORALL (n: subrange(s, t)): C(n) < x), 
 we get 2 subgoals:
lem3.1 :  

{-1}  (FORALL (n: subrange(s, t)): C(n) < x)
  |-------
[1]   C(s) < x & x <= C(t) => (EXISTS (n: subrange(s, t)): C(n) < x & x <= C(n + 1))
 
Simplifying with Yices,
 This completes the proof of lem3.1.

lem3.2 :  

  |-------
{1}   (FORALL (n: subrange(s, t)): C(n) < x)
[2]   C(s) < x & x <= C(t) => (EXISTS (n: subrange(s, t)): C(n) < x & x <= C(n + 1))
 
Rewriting using subrange_induction, matching in *,
lem3.2 :  

  |-------
{1}   FORALL (k: subrange(s, t)): k < t AND C(k) < x IMPLIES C(1 + k) < x
[2]   (FORALL (n: subrange(s, t)): C(n) < x)
{3}   C(s) < x & x <= C(t) => (EXISTS (n: subrange(s, t)): C(n) < x & x <= C(1 + n))
 
Simplifying with Yices,
 This completes the proof of lem3.2.

Q.E.D.