search

SRI-CSL / PVS

The People's Verification System
http://pvs.csl.sri.com
GNU General Public License v2.0
135 stars 32 forks source link

`powerset_finite` could be tighter #90

Open kai-e opened 1 year ago

kai-e commented 1 year ago

The prelude has

  powerset_finite: JUDGEMENT
    powerset(A: finite_set[T]) HAS_TYPE finite_set[set[T]]

when it could be stronger.

powerset_finite2: JUDGEMENT
    powerset(A: finite_set[T]) HAS_TYPE finite_set[finite_set[T]]

with the proof

(""
 (skolem-typepred)
 (ground)
 (("1"
   (skolem-typepred)
   (expand "powerset")
   (lemma "finite_subset" ("s" "x!1" "A" "A!1"))
   (propax))
  ("2"
   (expand "is_finite")
   (skolem-typepred)
   (inst 1 "exp2(card(A!1))" "powerset_natfun(A!1)")
   (expand "injective?")
   (lemma "powerset_natfun_inj[T]")
   (grind))))

Maybe keep both.

kai-e commented 1 year ago

I'm not entirely sure this is super-useful, but anyway, we can do a tiny bit better

powerset_finite3: JUDGEMENT
    powerset(B) HAS_TYPE non_empty_finite_set[finite_set[T]]

The proof (after having the previous one) is just the default ("" (judgement-tcc)).