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

What's up here?

I'm trying to discharge a TCC that ought to be pretty simple:  the full
TCC is:

FORALL (K, L: Location_BASE, p: finseq[Location_BASE]):
  Is_Prefix[Location_BASE](<>K, p) AND Is_Suffix[Location_BASE](<>L,p)
      (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


    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