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

Re: resubmit question : string

Kong Woei Susanto wrote:
> 
> Hi,
> I am sorry for this multiple question.
> 
> I have tried the example from Dave and Sam.
> Unfortunetly, the proof sequence in dave mail (4 Nov 97)
> or sam mail (4 Mar 96) stop when the string is
> transform to list.
> Seems that 'cons_lem' and 'char_lem' not recognized.
> 
> Am I missing something ?

The problem is likely to come from the distinction between
the types 'finseq[(char?)]' and 'string' (i.e. finseq[character]).

The rule 'fseq_lem' in theory 'string_lemmas' matches
equalities between terms of type 'string' but not between
terms of type 'finseq[(char?)]'.

The string literals (i.e. "abcd") are of type 'finseq[(char?)]' not 
of type 'string'. This means that you cannot show

   test1: LEMMA NOT "abcd" = "abce" 

by (AUTO-REWRITE-THEORY "string_lemmas")(ASSERT) because 'fseq_lem'
does not math.


However, if you try

   a: string = "abcd"
   b: string = "abce"

   test2: LEMMA NOT a=b

then (AUTO-REWRITE-THEORY "string_lemmas")(EXPAND* "a" "b")
(ASSERT) works because 'fseq_lem' matches.


It gets even more hairy if you use /=. You can prove

   test3: LEMMA a /= b 

by 

(GROUND)(EXPAND* "a" "b")
(AUTO-REWRITE-THEORY"string_lemmas")(ASSERT) 

but not by 

(EXPAND* "a" "b")(GROUND)
(AUTO-REWRITE-THEORY"string_lemmas")(ASSERT). 


A solution is to extend "string_lemmas" so that there
is a rule for both cases:

  string_lemmas: THEORY
 
    BEGIN

    l1, l2: VAR list[(char?)]

    c1, c2: VAR (char?)

    fseq_lem1: LEMMA
         list2finseq(l1): string = list2finseq(l2) IFF l1 = l2

    fseq_lem2: LEMMA
         list2finseq(l1) = list2finseq(l2) IFF l1 = l2
	
    cons_lem: LEMMA cons(c1,l1) = cons(c2,l2) IFF c1 = c2 & l1 = l2

    char_lem: LEMMA c1 = c2 IFF code(c1) = code(c2)

    END string_lemmas



Bruno

-- 
Bruno Dutertre                             | bruno@csl.sri.com
CSL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717