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

Re: [PVS-Help] singleton lists

Hi Bruno,

On Fri, 7 May, Bruno Dutertre wrote:
: R. Colvin wrote:
: > Hi, I'm having I'm having trouble working with an antecedent:
: > [snip]
: There's a proof command that does just what you want:
: (decompose-equality -10)

Thanks, that fixed it

: To make proofs more automatic, a good trick is to have
: the following lemma as an auto-rewrite:
:     equal_cons: LEMMA cons(a, x) = cons(b, y) IFF a=b AND x=y

Will do, thanks

: > You'll note the inclusion of the unused
: > variable 'f' in the definition of 'cons_null'.  Theorems apparently
: > need two variables for the 'lemma' command to work.  Is this
: > correct, and if so is there a neater work around?
: > 
: The lemma command works for any lemma. When it fails, it should give
: you an error message with some indication of the reason. That's usually
: for a lemma that comes from a parameterized theory and the prover
: cannot determine how to instantiate the parameters. The presence or
: absence of f should not matter.

Ok.  I tried using a single-parameter lemma in a different context
and the 'lemma' rule worked fine.  But I still can't seem to make it
work using the single-parameter version in the proofs I'm interested

I have a theory:

map_properties[T1, T2: TYPE]: Theory
	l: VAR list[T1]
	f: VAR [T1 -> T2]

	list_cons: THEOREM
		(forall f, l: cons?(l) implies l = cons(car(l), cdr(l)))

	list_cons2: THEOREM
		(forall l: cons?(l) implies l = cons(car(l), cdr(l)))

	[snip some other theorems]

end map_properties

In my proof I can execute:

Rule? (lemma list_cons ("l" "c0`list" "f" "next(c0)"))

Applying list_cons where 
  l gets c0`list,
  f gets next(c0),
this simplifies to: 

inv_np_not_ssq.1 :  

{-1}  cons?(c0`list) IMPLIES c0`list = cons(car(c0`list), cdr(c0`list))

At the very next 'Rule?' prompt:

Rule? (lemma list_cons2 ("l" "c0`list"))

Found 0 resolutions for list_cons2 relative to the substitution.
Please check substitution, provide actual parameters for lemma name,
or supply more substitutions.
No change on: (lemma list_cons2 ("l" "c0`list"))

The object c0`list is the same in each case.  As I said, I could get
'list_cons2' to work in a different context.  

The theorem list_cons is a fairly obvious property I need in my
proofs - is there something in the prelude (or elsewhere) that I
could use in place of list_cons?