Re: [PVS-Help] The problem with self-stability example

[Sam Owre <owre@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.