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

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Non empty finite set induction*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Wed, 14 May 2008 21:18:56 -0700*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.4.1i

I've defined a generic binary operator over sets that I'm trying to prove things about. It's very similar to what's done in finite_sets sum and prod(uct), however, the actual operator is variable: example[R: TYPE, o: FUNCTION[R, R -> R]]: THEORY BEGIN ASSUMING comm: ASSUMPTION commutative?(o) assoc: ASSUMPTION associative?(o) ENDASSUMING IMPORTING finite_sets@finite_sets_inductions[posnat] myset: TYPE = ARRAY[posnat -> R] indices: TYPE = non_empty_finite_set[posnat] curry(s: myset, K: indices): RECURSIVE R = IF singleton?(K) THEN s(the(K)) ELSE s(choose(K)) o curry(s, rest(K)) ENDIF MEASURE card(K) curry_add: LEMMA FORALL (s: myset, K: indices, k: posnat): NOT member(k, K) IMPLIES curry(s, add(k, K)) = s(k) o curry(s, K) END example I've worked it out on paper, but unfortunately can't carry it over to PVS. Most of my trouble comes from trying to reason about set operations. The idea is to induct on K: the base case being where K is singleton; the inductive step where K has an additional (arbitrary) element. My proof so far is as follows: curry_add : |------- {1} FORALL (s: myset, K: indices, k: posnat): NOT member(k, K) IMPLIES curry(s, add(k, K)) = s(k) o curry(s, K) Rule? (INDUCT "K" :NAME "nonempty_finite_set_induct") Using instance finite_sets@finite_sets_inductions[posnat].nonempty_finite_set_induct Inducting on K on formula 1 using induction scheme nonempty_finite_set_induct, this yields 2 subgoals: curry_add.1 : |------- {1} FORALL (e: posnat): FORALL (s: myset, k: posnat): NOT member(k, singleton(e)) IMPLIES curry(s, add(k, singleton(e))) = s(k) o curry(s, singleton(e)) Rule? (SKOSIMP*) Repeatedly Skolemizing and flattening, this simplifies to: curry_add.1 : |------- {1} member(k!1, singleton(e!1)) {2} curry(s!1, add(k!1, singleton(e!1))) = s!1(k!1) o curry(s!1, singleton(e!1)) Rule? (EXPAND "curry" 2 1) Expanding the definition of curry, this simplifies to: curry_add.1 : |------- [1] member(k!1, singleton(e!1)) {2} IF singleton?(add(k!1, singleton(e!1))) THEN s!1(the(add(k!1, singleton(e!1)))) ELSE s!1(choose(add(k!1, singleton(e!1)))) o curry(s!1, rest(add(k!1, singleton(e!1)))) ENDIF = s!1(k!1) o curry(s!1, singleton(e!1)) Rule? (SMASH) Repeatedly simplifying with BDDs, decision procedures, rewriting, and if-lifting, this yields 2 subgoals: curry_add.1.1 : {-1} singleton?(add(k!1, singleton(e!1))) |------- [1] member(k!1, singleton(e!1)) {2} s!1(the(add(k!1, singleton(e!1)))) = s!1(k!1) o curry(s!1, singleton(e!1)) Rule? (HIDE 2) Hiding formulas: 2, this simplifies to: curry_add.1.1 : [-1] singleton?(add(k!1, singleton(e!1))) |------- [1] member(k!1, singleton(e!1)) Rule? ... And this is where is gets dicey for me. [-1] implying [1] seems perfectly reasonable, but every attempt I've tried at proving it hasn't worked out. Any comments on that, my overall proof structure, or even the theory itself are welcomed. Thanks. jerome

- Prev by Date:
**Re: [PVS-Help] Determinism of choose** - Next by Date:
**Re: [PVS-Help] Non empty finite set induction** - Prev by thread:
**Re: [PVS-Help] Ask for help on a proof** - Next by thread:
**Re: [PVS-Help] Non empty finite set induction** - Index(es):