Duplicate Assuming TCC

[marianomoscato]

In some cases, already proved Assuming TCCs are being presented to the user as proof obligations when elements from the imported theory are used in a proof. This issue provokes effort duplication.

See example below.

A[n : nat]: THEORY
BEGIN
  ASSUMING
    na: ASSUMPTION n > 1
  ENDASSUMING

  pa(x: real): bool = x - n > 0
END A

B[n : nat]: THEORY
BEGIN
  ASSUMING
    nb: ASSUMPTION n > 2
  ENDASSUMING

  IMPORTING A[n]

  pb(x: real): bool = x > 2
END B

The importing of A from B generates the following TCC.

% Assuming TCC generated (at line 7, column 12) for  A[n]
    % generated from assumption A.na
  % unfinished
IMP_A_TCC1: OBLIGATION n > 1;

Such TCC can be easily proven by using the assumption B.nb. Let's say there is another theory C which imports B.

C: THEORY
BEGIN

  m: nat = 3

  IMPORTING B

  dummy: CONJECTURE FORALL (x: (pb[m])): x > 1
END C

The expression pb[m] generates the following TCC, from the B.nb assumption.

% Assuming TCC generated (at line 8, column 32) for  pb[m]
    % generated from assumption B.nb
  % unfinished
dummy_TCC1: OBLIGATION m > 2;

If an expression involving, for example, A.na is used in the proof of C.dummy, the TCC shown above is introduced in the proof as a new proof obligation. Nevertheless, this restriction should be considered already satisfied by any parameter of B for which the B.nb assumption has been proved.

In fact, such TCC branch is not generated in PVS 6.0.

Below there is an example proof for C.dummy where a case opens three branches in PVS 7.0.1154 and only two in PVS 6.0.

dummy :  

  |-------
{1}   FORALL (x: (pb[m])): x > 1

Rule? (case "FORALL (a: (pa[m])): a>1")
Case splitting on 
   FORALL (a: (pa[m])): a > 1, 
this yields  3 subgoals: 
dummy.1 :  

{-1}  FORALL (a: (pa[m])): a > 1
  |-------
[1]   FORALL (x: (pb[m])): x > 1

Rule? (postpone)
Postponing dummy.1.

dummy.2 :  

  |-------
{1}   FORALL (a: (pa[m])): a > 1
[2]   FORALL (x: (pb[m])): x > 1

Rule? (postpone)
Postponing dummy.2.

dummy.3T (TCC):   

  |-------
{1}   m > 1
[2]   FORALL (x: (pb[m])): x > 1

Rule? 

The last branch (dummy.3T) shouldn't be present.