# Re: [PVS-Help] Non empty finite set induction

```Jerry,
I'm cc'ing the list to try and get our conversation back over
there. I've attached a dump of the original 'curry' theory, as well as
the 'dualton' theory you were working on, for background.

>I started working on these tonight, but only had time to prove the
>first two.  Maybe one of those will be enough to get you out of your
>current spot, though.  See the attached.  Also, "dualton" is a stupid
>name. :-)

The first two don't really help; I think the third one has potential
though. One that I'm working on is:

sets_lemmas_ext[T: TYPE]: THEORY
BEGIN
a, b: VAR T
A: VAR non_empty_finite_set[T]

doubleton?(A): bool = singleton?(rest(A))

remove_is_element: LEMMA
FORALL (a, b: (A) | a /= b): doubleton?(A) IMPLIES
remove(a, A) = singleton(b) AND remove(b, A) = singleton(a)
END sets_lemmas_ext

Does this make sense? I get some dead-ends when trying to prove it, so
I may be missing something. Essentially, however, in the curry_x proof
it would be ideal to bring something like this in and instantiate it
with "k!1" and "choose(U!1)".

jerome
```
```%% PVS Version 4.1 - CMU Common Lisp 19d (19D)
%% 19d (19D)
\$\$\$curry.pvs
finite_sets_inductions_ext[T: TYPE]: THEORY
BEGIN
IMPORTING finite_sets[T]

SS,U : VAR non_empty_finite_set
P : VAR pred[finite_set]
n : VAR nat

nonempty_finite_set_induction_gen: THEOREM
(FORALL U:
(FORALL SS: card(SS) < card(U) IMPLIES P(SS)) IMPLIES P(U))
IMPLIES (FORALL U: P(U))

END finite_sets_inductions_ext

curry[R: TYPE, o: FUNCTION[R, R -> R]]: THEORY
BEGIN
ASSUMING
comm: ASSUMPTION commutative?(o)
assc: ASSUMPTION associative?(o)
ENDASSUMING

index:   TYPE = posnat
myset:   TYPE = ARRAY[index -> R]
indices: TYPE = non_empty_finite_set[index]

IMPORTING finite_sets@finite_sets_inductions[index]

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)

IMPORTING finite_sets_inductions_ext[index]

curry_singleton: LEMMA
FORALL (s: myset, k: index): curry(s, singleton(k)) = s(k)

curry_x: LEMMA
FORALL (s: myset, K: indices, k: index):
member(k, K) AND NOT singleton?(K) IMPLIES
curry(s, K) = s(k) o curry(s, remove(k, K))

END curry

\$\$\$curry.prf
(|finite_sets_inductions_ext|
(|nonempty_finite_set_induction_gen| 0
(|nonempty_finite_set_induction_gen-1| NIL 3420945053 NIL
("" (SKOSIMP)
(("" (CASE "FORALL n, U: card(U) = n IMPLIES P!1(U)")
(("1" (SKOLEM!) (("1" (INST -1 "card(U!1)" "U!1") NIL)))
("2" (HIDE 2)
(("2" (INDUCT "n" + "NAT_induction")
(("2" (SKOSIMP*)
(("2" (INST -3 "U!1")
(("2" (ASSERT)
(("2" (SKOSIMP)
(("2" (INST -1 "card(SS!1)")
(("2" (ASSERT)
(("2" (INST -1 "SS!1") NIL))))))))))))))))))))
NIL)
PROVED
((|real_lt_is_strict_total_order| NAME-JUDGEMENT
"(strict_total_order?[real])" |real_props| NIL)
(|NAT_induction| FORMULA-DECL NIL |naturalnumbers| NIL)
(|pred| TYPE-EQ-DECL NIL |defined_types| NIL)
(|card| CONST-DECL "{n: nat | n = Card(S)}" |finite_sets| NIL)
(|Card| CONST-DECL "nat" |finite_sets| NIL)
(= CONST-DECL "[T, T -> boolean]" |equalities| NIL)
(IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL)
(|non_empty_finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
(|empty?| CONST-DECL "bool" |sets| NIL)
(NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
(|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
(|is_finite| CONST-DECL "bool" |finite_sets| NIL)
(|set| TYPE-EQ-DECL NIL |sets| NIL)
(T FORMAL-TYPE-DECL NIL |finite_sets_inductions_ext| NIL)
(|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL)
(>= CONST-DECL "bool" |reals| NIL)
(|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
(|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
(|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
(|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
(|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
(|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
(|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
(|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
(|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
(|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL))
NIL NIL NIL NIL)))
(|curry|
(|curry_TCC1| 0
(|curry_TCC1-1| NIL 3420944664 3420945128
("" (GRIND :EXCLUDE "choose") NIL NIL) PROVED
((|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
(|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
(NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
(|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
(|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
(|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
(|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
(|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
(|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
(|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
(|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
(|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(>= CONST-DECL "bool" |reals| NIL)
(|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(> CONST-DECL "bool" |reals| NIL) (|index| TYPE-EQ-DECL NIL |curry| NIL)
(|set| TYPE-EQ-DECL NIL |sets| NIL)
(|is_finite| CONST-DECL "bool" |finite_sets| NIL)
(|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
(|indices| TYPE-EQ-DECL NIL |curry| NIL)
(|injective?| CONST-DECL "bool" |functions| NIL)
(|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL)
(|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])"
|real_props| NIL)
(|real_gt_is_strict_total_order| NAME-JUDGEMENT
"(strict_total_order?[real])" |real_props| NIL)
(|choose| CONST-DECL "(p)" |sets| NIL)
(|nonempty?| CONST-DECL "bool" |sets| NIL)
(|finite_remove| APPLICATION-JUDGEMENT "finite_set[index]" |curry| NIL)
(|singleton?| CONST-DECL "bool" |sets| NIL)
(|rest| CONST-DECL "set" |sets| NIL)
(/= CONST-DECL "boolean" |notequal| NIL)
(|member| CONST-DECL "bool" |sets| NIL)
(|remove| CONST-DECL "set" |sets| NIL)
(|empty?| CONST-DECL "bool" |sets| NIL))
832 126 T NIL))
(|curry_TCC2| 0
(|curry_TCC2-1| NIL 3420944664 3420945155
("" (SKOSIMP) (("" (REWRITE "card_rest") (("" (ASSERT) NIL NIL)) NIL)) NIL)
PROVED
((|int_minus_int_is_int| APPLICATION-JUDGEMENT "int" |integers| NIL)
(|card_rest| FORMULA-DECL NIL |finite_sets| NIL)
(|set| TYPE-EQ-DECL NIL |sets| NIL)
(|is_finite| CONST-DECL "bool" |finite_sets| NIL)
(|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
(NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
(|empty?| CONST-DECL "bool" |sets| NIL)
(|indices| TYPE-EQ-DECL NIL |curry| NIL)
(|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
(|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
(|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
(|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
(|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
(|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
(|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
(|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
(|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
(|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
(>= CONST-DECL "bool" |reals| NIL)
(|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(> CONST-DECL "bool" |reals| NIL) (|index| TYPE-EQ-DECL NIL |curry| NIL)
(|real_lt_is_strict_total_order| NAME-JUDGEMENT
"(strict_total_order?[real])" |real_props| NIL))
758 28 T NIL))
(|curry_singleton| 0
(|curry_singleton-1| NIL 3420945323 3420945381
("" (SKOLEM!)
(("" (TYPEPRED "the(singleton(k!1))")
(("" (EXPAND "curry")
(("" (REWRITE "singleton")
(("" (REWRITE "the") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
PROVED
((|nonempty_singleton_finite| APPLICATION-JUDGEMENT
"non_empty_finite_set[index]" |curry| NIL)
(|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
(|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
(NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
(|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
(|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
(|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
(|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
(|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
(> CONST-DECL "bool" |reals| NIL)
(|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
(|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
(|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
(|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(>= CONST-DECL "bool" |reals| NIL)
(|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(|index| TYPE-EQ-DECL NIL |curry| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL)
(|singleton?| CONST-DECL "bool" |sets| NIL)
(|the| CONST-DECL "(p)" |sets| NIL)
(|singleton| CONST-DECL "(singleton?)" |sets| NIL)
(|real_gt_is_strict_total_order| NAME-JUDGEMENT
"(strict_total_order?[real])" |real_props| NIL)
(|curry| DEF-DECL "R" |curry| NIL))
5718 10 T SHOSTAK))
(|curry_x_TCC1| 0
(|curry_x_TCC1-1| NIL 3420944664 3420945312 ("" (SUBTYPE-TCC) NIL NIL) PROVED
((|empty?| CONST-DECL "bool" |sets| NIL)
(|remove| CONST-DECL "set" |sets| NIL)
(/= CONST-DECL "boolean" |notequal| NIL)
(|singleton?| CONST-DECL "bool" |sets| NIL)
(|member| CONST-DECL "bool" |sets| NIL)
(|finite_remove| APPLICATION-JUDGEMENT "finite_set[index]" |curry| NIL)
(|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])"
|real_props| NIL)
(|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL)
(|real_gt_is_strict_total_order| NAME-JUDGEMENT
"(strict_total_order?[real])" |real_props| NIL)
(|injective?| CONST-DECL "bool" |functions| NIL)
(|indices| TYPE-EQ-DECL NIL |curry| NIL)
(|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
(|is_finite| CONST-DECL "bool" |finite_sets| NIL)
(|set| TYPE-EQ-DECL NIL |sets| NIL) (|index| TYPE-EQ-DECL NIL |curry| NIL)
(> CONST-DECL "bool" |reals| NIL)
(|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(>= CONST-DECL "bool" |reals| NIL)
(|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
(|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
(|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
(|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
(|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
(|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
(|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
(|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
(|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
(NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
(|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
(|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL))
158 158 T NIL))
(|curry_x| 0
(|curry_x-2| NIL 3420945537 3420945585
("" (INDUCT "K" :NAME "nonempty_finite_set_induction_gen")
(("1" (TYPEPRED "K!1") (("1" (PROPAX) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (EXPAND "curry" 3 1)
(("2" (SMASH)
(("2" (COPY -1)
(("2" (INST -2 "rest(U!1)")
(("2" (INST -1 "remove(k!1, U!1)")
(("2" (REWRITE "card_rest")
(("2" (REWRITE "card_remove")
(("2" (REWRITE "member")
(("2" (ASSERT)
(("2" (INST -1 "s!1" "choose(U!1)")
(("2" (INST -2 "s!1" "k!1")
(("2" (GROUND)
(("1"
(CASE-REPLACE
"remove(choose(U!1), remove(k!1, U!1)) = remove(k!1, rest(U!1))")
(("1" (REPLACE -3)
(("1" (REPLACE -2)
(("1" (LEMMA "assc")
(("1" (EXPAND "associative?")
(("1" (COPY -1)
(("1"
(INST -1 "s!1(choose(U!1))"
"s!1(k!1)"
"curry(s!1, remove(k!1, rest(U!1)))")
(("1"
(INST -2 "s!1(k!1)"
"s!1(choose(U!1))"
"curry(s!1, remove(k!1, rest(U!1)))")
(("1" (REPLACE -1 :DIR RL)
(("1" (REPLACE -2 :DIR RL)
(("1" (LEMMA "comm")
(("1"
(EXPAND "commutative?")
(("1"
(INST -1
"s!1(choose(U!1))"
"s!1(k!1)")
(("1" (REPLACE -1)
(("1" (PROPAX) NIL
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (HIDE-ALL-BUT 1)
(("2" (GRIND-WITH-EXT :EXCLUDE "choose") NIL
NIL))
NIL))
NIL)
("2" (GRIND :EXCLUDE "curry") NIL NIL)
("3" (HIDE -2)
(("3" (REWRITE "rest")
(("3" (POSTPONE) NIL NIL)) NIL))
NIL)
("4" (GRIND :EXCLUDE "choose") NIL NIL)
("5" (GRIND :EXCLUDE "curry") NIL NIL)
("6" (GRIND :EXCLUDE "choose") NIL NIL)
("7" (HIDE -1)
(("7" (REWRITE "rest")
(("7" (POSTPONE) NIL NIL)) NIL))
NIL)
("8" (GRIND :EXCLUDE "curry") NIL NIL)
("9" (REWRITE "rest") (("9" (POSTPONE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("3" (SKOSIMP*) (("3" (GRIND :EXCLUDE "curry") NIL NIL)) NIL))
NIL)
UNFINISHED NIL 4703 397 NIL NIL)))

```
```%% PVS Version 4.1 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Oct 30, 2007 14:52)
%% 8.1 [Linux (x86)] (Oct 30, 2007 14:52)
\$\$\$dualton.pvs
%-------------------------------------------------------------------------
%
%  Sets with exactly two elements
%
%  For PVS version 4.1.  May 28, 2008
%  ---------------------------------------------------------------------
%      Author: Jerry James <loganjerry@xxxxxxxxx>
%
%-------------------------------------------------------------------------
dualton[T: TYPE]: THEORY
BEGIN

IMPORTING sets[T]

t, u, v: VAR T
S: VAR set

% A set with exactly two elements
dualton?(S): bool = EXISTS t, u: t /= u AND S = ({v | v = t OR v = u})

dualton(t: T, u: {v | t /= v}): (dualton?) = {v | v = t OR v = u}

D: VAR (dualton?)

dualton_nonempty: JUDGEMENT (dualton?) SUBTYPE_OF (nonempty?)

dualton_remove: LEMMA
FORALL t, D: member(t, D) IMPLIES singleton?(remove(t, D))

dualton_rest: LEMMA FORALL D: singleton?(rest(D))

dualton_choose: LEMMA
FORALL t, u:
t /= u IMPLIES
(choose(dualton(t, u)) = t AND rest(dualton(t, u)) = singleton(u))
OR
(choose(dualton(t, u)) = u AND rest(dualton(t, u)) = singleton(t))

END dualton

\$\$\$dualton.prf
(dualton
(dualton_TCC1 0
(dualton_TCC1-1 nil 3421022779 3421023157 ("" (subtype-tcc) nil nil)
proved
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil dualton nil)
(/= const-decl "boolean" notequal nil)
(dualton? const-decl "bool" dualton nil))
66 40 nil nil))
(dualton_nonempty 0
(dualton_nonempty-1 nil 3421023156 3421023157
("" (judgement-tcc) nil nil) proved
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(dualton? const-decl "bool" dualton nil)
(/= const-decl "boolean" notequal nil)
(T formal-type-decl nil dualton nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
117 80 nil nil))
(dualton_remove 0
(dualton_remove-1 nil 3421022787 3421023157
("" (grind :if-match nil)
(("1" (inst + "u!1")
(("1" (grind-with-ext) nil nil) ("2" (grind-with-ext) nil nil))
nil)
("2" (inst + "t!2")
(("1" (grind-with-ext) nil nil) ("2" (grind-with-ext) nil nil))
nil))
nil)
proved
((t!2 skolem-const-decl "T" dualton nil)
(D!1 skolem-const-decl "(dualton?)" dualton nil)
(u!1 skolem-const-decl "T" dualton nil)
(remove const-decl "set" sets nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(dualton? const-decl "bool" dualton nil)
(singleton? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(T formal-type-decl nil dualton nil))
337 260 t shostak))
(dualton_rest 0
(dualton_rest-1 nil 3421022975 3421023688
("" (skolem-typepred)
(("" (expand "rest")
(("" (ground)
(("1" (use "dualton_nonempty")
(("1" (expand "nonempty?") (("1" (propax) nil nil)) nil))
nil)
("2" (use "dualton_remove")
(("2" (expand "member") (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
proved
((rest const-decl "set" sets nil)
(dualton_remove formula-decl nil dualton nil)
(choose const-decl "(p)" sets nil)
(member const-decl "bool" sets nil)
(dualton_nonempty judgement-tcc nil dualton nil)
(nonempty? const-decl "bool" sets nil)
(dualton? const-decl "bool" dualton nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil dualton nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
69345 100 t shostak))
(dualton_choose 0
(dualton_choose-1 nil 3421023602 3421023733
("" (skosimp) (("" (postpone) nil nil)) nil) unfinished nil 12238 10
t shostak)))

```