Reappearing TCC from Instantiation Argument

[marianomoscato]

The typechecker is requesting to prove TCCs already proved in the originating theory. See example below.

The type checker produces two TCCs when applied on the following theory.

D: THEORY BEGIN

  p(n: nat): MACRO bool =  (n>0 IMPLIES 1/n > 0.23)

  dummy: LEMMA FORALL(l: list[(p)]): FALSE

END D

Those TCCs are shown below. The second one is correctly subsumed by the first one.

% Subtype TCC generated (at line 3, column 42) for  n
    % expected type  nznum
  % unfinished
p_TCC1: OBLIGATION FORALL (n: nat): n > 0 IMPLIES n /= 0;

% The subtype TCC (at line 3, column 4) in decl dummy for  n
    % expected type  nznum
  % is subsumed by p_TCC1

Nevertheless, when the same kind of quantification appears in a different theory importing D, the same subtype TCC is not longer subsumed. See the example below.

E: THEORY BEGIN

  IMPORTING D

  dummy: LEMMA FORALL(l: list[(p)]): FALSE

END E

The TCC generated by typechecking E is shown below.

% Subtype TCC generated (at line 3, column 4) for  n
    % expected type  nznum
  % unfinished
dummy_TCC1: OBLIGATION FORALL (n: nat): n > 0 IMPLIES n /= 0;

This TCC should be subsumed as well or even not be generated at all.

As expected, this issue also occurs if a formula such as the one in the dummy lemma is used in a proof command, as for example in (case "FORALL(l: list[(p)]): FALSE").