Looking for a non-simplifying extensionality rule

[Kai Engelhardt]

I'm hitting problems proving simple things involving sets. Here's a somewhat canonical example:

```

[-1]  is_finite(A!1)
[-2]  nonempty?(A!1)
  |-------
{1}   ({y: finite_set[D] |
          EXISTS (x: (powerset(rest(A!1)))): y = add(choose(A!1), x)})
       =
       {y: (nonempty?[D]) |
          EXISTS (x: (powerset(rest(A!1)))): y = add(choose(A!1), x)}

```

Using extensionality leads to unprovable obligations including

```
[-1]  is_finite(A!1)
[-2]  nonempty?(A!1)
  |-------
{1}   FORALL (x: set[D]): nonempty?[D](x) IFF is_finite[D](x)

```

So, how does one avoid this "simplification" and prove the original goal?

[Mariano Moscato]

Hi, Kai.

Actually, the issue is not the extensionality rule, but the way in which the formula {1} is expressed. If you ask PVS to show the expanded version of the sequent, you will see that it infers that such equality is a predicate on elements of type finite_sets[D].

equalities[[finite_sets[D].finite_set -> booleans.boolean]].=
          ({y: finite_sets[D].finite_set |
              EXISTS (x: (sets[D].powerset(sets[D].rest(A!1)))):
                equalities[sets[D].set].=
                    (y, sets[D].add(sets[D].choose(A!1), x))},
           {y: (sets[D].nonempty?) |
              EXISTS (x: (sets[D].powerset(sets[D].rest(A!1)))):
                equalities[sets[D].set].=
                    (y, sets[D].add(sets[D].choose(A!1), x))})

Internally, the proof command apply-extensionality uses such inferred type to instantiate the "extensionality" lemma (defined in the sets_lemmas theory, in the prelude). When it instantiates the second set, the unprovable TCC is generated.

A possible workaround is to restate this equality indicating explicitly a more general type. For instance,

equalities[[set[D] -> booleans.boolean]].=
 ( ... , ... )

I hope this helps. Feel free to follow up.

Kindly,
Mariano.

[Kai Engelhardt]

Thanks for the hint! Hopefully I'll remember that next time. I ended up proving some semi-useful lemmas such as
```
weak_ext2[T: TYPE+, A: TYPE FROM T, B: TYPE FROM T]: THEORY
BEGIN
P: VAR pred[T]
a: VAR A
b: VAR B
x: VAR T

weak_ext_half: LEMMA
  (FORALL a: P(a) => B_pred(a)) =>
  subset?({x | A_pred(x) AND P(x)}, {x | B_pred(x) AND P(x)})

weak_ext: LEMMA
  (FORALL a: P(a) => B_pred(a)) AND (FORALL b: P(b) => A_pred(b)) =>
  {x | A_pred(x) AND P(x)} = {x | B_pred(x) AND P(x)}

set_comprehension_shift_type: LEMMA
  {x | A_pred(x) AND P(x)} = {a | P(a)}

END weak_ext2

```

that appeared to have similar effects. After a lot of futzing around with types – mostly `finite_set[...]` vs. `set[...]` – before the stars aligned and I could finish the proof I was attempting (Problem 96 from this list).