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

*To*: lingzhao <maolzh@xxxxxxxxx>*Subject*: Re: [PVS-Help] The problem with self-stability example*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Mon, 28 Apr 2008 15:15:06 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to lingzhao <maolzh@gmail.com> message dated "Sun, 27 Apr 2008 22:22:20 +0800."*In-reply-to*: <1209306140.9353.17.camel@lzh>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <1209306140.9353.17.camel@lzh>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi lingzhao, This is an old proof; apply-extensionality had a bug where it was not generating TCCs as it should. But there seems to be a bug in that grind should still get the main branch without leaving 6 TCCs. We are looking into this. In the meantime, the following does prove it in PVS 4.1. Regards, Sam ("" (skosimp*) (expand "update_P") (flatten) (case "active(s1!1)(p!1)") (("1" (hide 1) (prop) (("1" (lemma "mod_inc" ("u" "s0!1(0)")) (grind :exclude "mod")) ("2" (grind :exclude "mod")))) ("2" (apply-extensionality :hide? t) (("1" (lemma "mod_lt_nat" ("n" "x!1" "m" "N")) (grind :exclude "mod" :rewrites "mod_eq_arg") (("1" (case-replace "1+p!1 = N") (("1" (assert)) ("2" (assert)))) ("2" (case-replace "1+p!1 = N") (("1" (assert)) ("2" (assert)))) ("3" (case-replace "1+p!1 = N") (("1" (assert)) ("2" (assert)))) ("4" (case-replace "1+p!1 = N") (("1" (assert)) ("2" (assert)))) ("5" (case-replace "1+p!1 = N") (("1" (assert)) ("2" (assert)))) ("6" (case-replace "1+p!1 = N") (("1" (assert)) ("2" (assert)))))) ("2" (flatten) (rewrite "mod_pos")) ("3" (rewrite "mod_pos")) ("4" (rewrite "mod_pos")))))) lingzhao <maolzh@xxxxxxxxx> wrote: > Hi, > > I'm learning the self-stability example which was downloaded from the > link: ftp://ftp.csl.sri.com/pub/pvs/examples/self-stability/ ,and I try > to prove the "update_active" Lemma in the stability THEORY. I follow the > steps in stability.dmp file,but I find that I can not complete the > proof,I don't know why, who can help me or tell me how what's the > problem? thanks. > > > (|update_active| > "" > (SKOSIMP*) > (("" > (EXPAND "update_P") > (("" > (FLATTEN) > (("" > (CASE > "active(s1!1)(p! > 1)") > (("1" > (HIDE 1) > (("1" > (PROP) > (("1" > (LEMMA > "mod_inc" > ("u" "s0! > 1(0)")) > (("1" > (GRIND > :EXCLUDE > "mod") > NIL))) > ("2" > (GRIND > :EXCLUDE > "mod") > NIL))))) > > > This completes the proof of update_active.1. > > > ("2" > > (APPLY-EXTENSIONALITY > :HIDE? > T) > > > but after I apply (apply-extensionality :hide? t) command, it yields > 4 subgoals, and the proof can not be completed with the commands shows > below, so what's the problem? thanks in advance. > > > (("2" > (LEMMA > "mod_lt_nat" > ("n" > "x!1" > "m" > "N")) > (("2" > (GRIND > :EXCLUDE > "mod" > :REWRITES > > "mod_eq_arg") > > NIL))))))))))))) > > > > lingzhao > Best Regards.

**References**:**[PVS-Help] The problem with self-stability example***From:*lingzhao

- Prev by Date:
**[PVS-Help] The problem with self-stability example** - Next by Date:
**[PVS-Help] loop in PVS** - Previous by thread:
**[PVS-Help] The problem with self-stability example** - Next by thread:
**[PVS-Help] loop in PVS** - Index(es):