[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [work] [PVS-Help] question about the list adt
The following is a proof script (in ProofLite format) that discharges
this lemma using the length function.
%|- putative3_1 : PROOF
%|- (then (skosimp)
%|- (spread (case "length(cons(a!1, s!1)) = length(s!1)")
%|- ((grind) (assert))))
There are many ways to prove this lemma. Note, for example, that << is
well_founded order and that s << cons(x,s), therefore s /= cons(x,s).
Hope that this helps,
On Thu, 2007-04-12 at 16:07, Robert Goldman wrote:
> I was playing around with the list adt in something I was doing, and
> expected to be able to prove the following lemma:
> putative3_1 : LEMMA ( cons(a, s) /= s )
> ... but was unable to do so.
> Question: have I just failed to be able to prove something because of my
> lack of ability with PVS, or is this not a valid consequence of the list
> I believe that this should be a consequence of the theory, since
> length(s) = n implies length(cons(a, s) = n + 1.
> But I don't see where the list_adt theory makes it impossible that the
> cons operator should have an identity.
> Thank you for any guidance,
Cesar A. Munoz H., Senior Staff Scientist mailto:email@example.com
National Institute of Aerospace mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way, Room 214 http://research.nianet.org/~munoz
Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6 1A18 6000 89F5 C114 E6C4