[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: "<" on a subset of nat is well_founded



Mauro Gargano wrote:
>  Hi everybody,
> 
> I want to do an induction proof starting from the index "i!1+2" so
> I used the induction scheme (induct "j" :name 
> "wf_induction[upfrom(i!1+2),<]")
> 
> but I cannot get rid of the subgoal in which PVS asks me to show that 
> the "<" is wellfounded on the set upfrom(i!1 + 2):
> 
> |-------
> 
> [1]   well_founded?[upfrom(i!1 + 2)]
> 
>         (restrict[[real, real], [upfrom(i!1 + 2), upfrom(i!1 + 2)],
> 
>                   boolean]
> 
>              (<))
> 
> 
> How can I instantiate properly the wf_nat axiom?
> 
> 
> 
> 
> Thanks in advance,
> Mauro.
> 
> 

Hi,

To prove this subgoal, you can expand "well_founded?" and "restrict".
This gives:

   |-------
{1}   FORALL (p: pred[upfrom(2 + i!1)]):
         (EXISTS (y: upfrom(2 + i!1)): p(y)) IMPLIES
          (EXISTS (y: (p)): FORALL (x: (p)): (NOT (x < y)))

Then (skosimp*) will introduce predicate "p!1" and you can
finish the proof by instantiating the wf_nat axiom with
"{ n: nat | n>=2+i!1 AND p!1(n) }".


But there's an easier way of doing induction from "i!1+2",
by using the lemmas from theory "bounded_int_inductions" in
the prelude. They exist in two forms:

   upfrom_induction: LEMMA
     (pf(m) AND (FORALL jf: pf(jf) IMPLIES pf(jf + 1)))
        IMPLIES (FORALL jf: pf(jf))

   UPFROM_induction: LEMMA
     (FORALL jf: (FORALL kf: kf < jf IMPLIES pf(kf)) IMPLIES pf(jf))
       IMPLIES (FORALL jf: pf(jf))


You can do either (induct "j" :name "upfrom_induction[i!1+2]")
or (induct "j" :name "UPFROM_induction[i!1+2]") depending
on which form you want to use.

Note that (induct "j") is often all you need. PVS will
choose an induction lemma based on the type of "j".
For example, if "j" is of type "upfrom(i!1+2)"
then (induct "j") has the same effect as
(induct "j" :name "upfrom_induction[i!1+2]")

Bruno