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

[PVS-Help] Decompose-equality after assert



Hi, I'm hoping someone can explain the following behaviour to me.

Consider the following proof steps (understanding the formula isn't
necessary, just that it is an equality between tuples):

====================================================================
cinv_ssn.10 :  

[-1,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------

Rule? (decompose-equality)
Applying decompose-equality,
this simplifies to: 
cinv_ssn.10 :  

{-1}  c0`n(ppp) = c0`ss(q)`1
{-2}  1 + c0`ss(ppp)`2 = c0`ss(q)`2
  |-------

====================================================================

This is what I would expect.  However, if I execute 'record' before
decomposing the equality I get the empty sequent, eg.

====================================================================
cinv_ssn.10 :  

[-1,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------

Rule? (record)
Simplifying and recording with decision procedures,
this simplifies to: 
cinv_ssn.10 :  

[-1,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------

Rule? (decompose-equality)
Applying decompose-equality,
this simplifies to: 
cinv_ssn.10 :  

  |-------

====================================================================

I don't understand why the equality decomposes to true after
recording (I noticed this when doing an 'assert') .
Any help appreciated.
(Btw, there are formulas which I have 'hidden', but my understanding
is they should not affect what is going on).

Thanks,
Rob

Below is the output from (decompose-equality$) after 'record'ing.


====================================================================
cinv_ssn.10 :  

[-1,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------

Rule? (decompose-equality$)
Case splitting on 
   (c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
    (c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2, 
this yields  2 subgoals: 
cinv_ssn.10.1 :  

{-1}  (c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
       (c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2
[-2,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------

Simplifying with decision procedures,
this simplifies to: 
cinv_ssn.10.1 :  

{-1}  TRUE AND TRUE
[-2,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------

Deleting some formulas,
this simplifies to: 
cinv_ssn.10.1 :  

[-1]  TRUE AND TRUE
  |-------

Applying disjunctive simplification to flatten sequent,
this simplifies to: 
cinv_ssn.10.1 :  

  |-------

Postponing cinv_ssn.10.1.

cinv_ssn.10.2 :  

[-1,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------
{1}   (c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
       (c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2

No change on: (flatten)
cinv_ssn.10.2 :  

[-1,(main)]
      (c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
  |-------
{1}   (c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
       (c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2

Repeatedly applying the replace rule,

This completes the proof of cinv_ssn.10.2.

cinv_ssn.10.1 :  

  |-------


====================================================================