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

*To*: Mauro Gargano <mauro@wjpserver.cs.uni-sb.de>*Subject*: Re: "<" on a subset of nat is well_founded*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Thu, 13 Feb 2003 10:22:56 -0800*CC*: pvs-help@csl.sri.com*References*: <3E4A7324.5000707@wjp.cs.uni-sb.de>*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/20020529

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

**References**:**"<" on a subset of nat is well_founded***From:*Mauro Gargano <mauro@wjpserver.cs.uni-sb.de>

- Prev by Date:
**Dependent types lost in reduce combinators** - Next by Date:
**Proof of override expressions** - Prev by thread:
**"<" on a subset of nat is well_founded** - Next by thread:
**intersection, implication, predicate problem, specific exampleproblem** - Index(es):