Re: [PVS-Help] singleton lists

[Bruno Dutertre <bruno@sdl.sri.com>]

   list_cons_eta: AXIOM
     FORALL (cons?_var: (cons?)):
       cons(car(cons?_var), cdr(cons?_var)) = cons?_var;
R. Colvin wrote:
> 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
> in.
> 
> I have a theory:
> 
> ----------------------------------
> map_properties[T1, T2: TYPE]: Theory
> begin
> 	
> 	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))
> [snip]
> ++++++++++++++++
> 
> 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"))
> ++++++++++++++++
> 

Hi,

This fails because theory map_properties has two parameters T1 and T2.
Even though T2 does not occur in list_cons2, both parameters
must be instantiated when the lemma is used.

Variable l of list_cons and list_cons2 is of type list[T1], so PVS
can infer the actual type T1 from the term "c0`list", but that's not
enough. The prover cannot determine T2. When you use lemma "list_cons"
and give a substitution for "f" then the prover has enough information
to determine both T1 and T2.

The simplest solution to avoid this f is to specify explicitly the types
you want. For example, if T1 and T2 are nat, you can write
(lemma "list_cons2[nat, nat]" ...).

> 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?
> 

Yes, the following axiom is generated from the definition of list:

   list_cons_eta: AXIOM
     FORALL (cons?_var: (cons?)):
       cons(car(cons?_var), cdr(cons?_var)) = cons?_var;

It's in theory "list_adt" that axiomatizes the list datatype. The theory
can be viewed using M-x view-prelude-theory.

In a proof, you rarely need to invoke these lemmas explictly. The
commands (eta ..) or (apply-eta ..) will do it for you. Also,
(apply-extensionality ...) is often more useful than the eta
axioms.

Bruno