Add update-nth book to std/lists

[ragerdl]

From rage...@gmail.com on April 30, 2013 14:46:11

It would be helpful to have a defbounded-list, which would be a way of taking a list where each element satisfies a particular predicate (say, integer32-p) and requiring that the list always be of length 24. defbounded-list would provide nice lemmas about using nth and update-nth to access/modify slots of the list.

Then again, maybe we should be using alists or a different approach.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=60

[ragerdl]

From rage...@gmail.com on April 30, 2013 13:22:55

Maybe a :length-limit flag could be added to cutil::deflist. Here are the two lemmas we needed in our work to do it. Defprimitive can basically be thought of as a defnd with a bell or whistle.

;; Use this in stclear data to allow access from indexes 0..23 (defprimitive tpmx-pcrvalue-list (x) (and (tpm-pcrvalue-list-p x) (equal (len x) tpmx-num-pcrs)) :default (make-list tpmx-num-pcrs :initial-element (make-tpm-pcrvalue)) :parents (tpm-structures))

(defthm weneedthis (implies (and (<= 0 n) (< n tpmx-num-pcrs) (tpmx-pcrvalue-list-p x)) (tpm-pcrvalue-p (nth n x))) :hints (("Goal" :in-theory (enable tpmx-pcrvalue-list-p))))

(defthm weneedthistoo (implies (and (<= 0 n) (< n tpmx-num-pcrs) (tpmx-pcrvalue-list-p lst) (tpm-pcrvalue-p val)) (tpmx-pcrvalue-list-p (update-nth n val lst))) :hints (("Goal" :in-theory (enable tpmx-pcrvalue-list-p))))

[ragerdl]

From jared.c....@gmail.com on June 17, 2013 07:01:32

I am inclined to mark this as WontFix.

Cutil::deflist already provides lemmas about nth, and lemmas about len-of-update-nth should eventually be put somewhere into, e.g., std/lists.

Together, this would seem sufficient to prove things about tpmx-pcrvalue-list by just leaving it enabled?

If you disagree please let me know, otherwise we can close this.

Owner: ja...@centtech.com
Cc: rage...@gmail.com
Labels: Type-Enhancement Component-CUTIL Priority-Low

[ragerdl]

From rage...@gmail.com on June 17, 2013 08:03:26

I know that I tried including std/lists, and I still needed to manually write the lemmas. It seems important enough to me that we should wait to close this topic until std/lists has it. Feel free to rename it in the meantime if you like.

[ragerdl]

From jared.c....@gmail.com on June 17, 2013 10:19:15

Renaming topic to "Add update-nth book to std/lists"

Summary: Add update-nth book to std/lists (was: [cutil::defbounded-list] Create it)
Labels: -Component-CUTIL Usability

[ragerdl]

From jared.c....@gmail.com on October 18, 2013 08:40:54

Labels: Component-Std

[ragerdl]

From jared.c....@gmail.com on October 18, 2013 08:41:30

Owner: jared.c....@gmail.com

[ragerdl]

From jared.c....@gmail.com on January 13, 2014 10:54:29

This issue was closed by revision r2419 .

Status: Fixed