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

*To*: pvs-help@csl.sri.com*Subject*: What's up here?*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Sun, 16 Apr 2000 13:27:07 -0400 (EDT)*Delivery-Date*: Sun Apr 16 10:29:18 2000

I'm trying to discharge a TCC that ought to be pretty simple: the full TCC is: Are_Conn_in_BASE_TCC1: OBLIGATION FORALL (K, L: Location_BASE, p: finseq[Location_BASE]): Is_Prefix[Location_BASE](<>K, p) AND Is_Suffix[Location_BASE](<>L,p) IMPLIES (FORALL (M, N: Location_BASE): Is_Substring[Location_BASE](<>M o <>N, p) AND M /= N IMPLIES TRUE AND Card[Location_BASE](Pair[Location_BASE](M, N)) = 2); There's a lot of extra garbage here. It really boils down to a proof obligation to discharge the following sequent: |------- {1} Card[Location_BASE](Pair[Location_BASE](M!1, N!1)) = 2 [2] M!1 = N!1 The type Location_BASE is an interpreted type = {n: nat| 1 <= n <= Max} where Max is a posint parameter to the theory; the operator, "Pair", is defined in an imported theory as follows: pairs[T: TYPE] : THEORY BEGIN IMPORTING finite_sets@finite_sets_eq[T, below[2]] x,y: VAR T Pair(x,y): finite_set[T] = {z: T| z = x or z = y} PairCard: claim x /= y implies Card[T](Pair[T](x,y)) = 2 END pairs So Pair(x,y) is just {x,y}. I've proved the claim PairCard, which says that if x and y are distinct, then the cardinality of {x,y} is 2. Now I'm trying to use PairCard to discharge the sequent cited above. I would have thought it could be done straightaway by using PairCard. But when I do a (lemma "PairCard[Location_BASE]" ("x" "M!1" "y" "N!1")) I get the following sequent: {-1} M!1 /= N!1 IMPLIES Card[Location_BASE](Pair[Location_BASE](M!1,N!1)) = 2 |------- [1] Card[Location_BASE](Pair[Location_BASE](M!1, N!1)) = 2 [2] M!1 = N!1 and again, as far as I can see, this should be trivially true. But it doesn't get discharged with (grind). I've tried expanding "Card" and "Pair". "Card" expands, in both antecedent and consequent occurrences, all the way down to min(inj_set(Pair[Location_BASE](M!1, N!1))) and further. Oddly, (expand "Pair") only effects the antecedent occurrence of "Pair". At any rate, with these expansions we get identical seeming antecedent and consequent, yet the sequent can't be discharged. I must be missing something obvious. Sorry in advance if that's the case... Can anybody help? Mark Aronszajn

- Prev by Date:
**help, !** - Next by Date:
**inductive predicates in adt** - Prev by thread:
**Re: inductive predicates in adt** - Next by thread:
**help, !** - Index(es):