%implied goals cannot be proved in presence of hiding

[sternk]

Reported by till and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1103

---

With the following specification

spec test =
  sort s
  op a,b,c:s
  . a = b %(axiom)%
hide c
then . a=b %(goal)% %implied
end

I have found no way to prove the goal, although it obviously follows. However, with

spec test =
  sort s
  op a,b,c:s
  . a = b %(axiom)%
hide c
then %implies
 . a=b %(goal)% 
end

I can prove the goal by first computing the normal form, and then calling the auto DG prover. Here is a variant where the proof cannot be done by entirely by the DG prover, but still some actual theorem prover needs to be called:

spec test =
  sort s
  op a,b,c,d:s
  . a = b %(axiom1)%
  . b = c %(axiom2)%
hide d
then %implies
  . a=c %(goal)% 
end

[sternk]

Comment by mcodescu Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1103#comment:2

---

I guess it would make sense that once you do a hiding, in the resulting theory you keep the sentences that do not have hidden symbols. Currently a hiding removes all sentences from the theory.

[sternk]

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1103#comment:3

---

Replying to mcodescu:

I guess it would make sense that once you do a hiding, in the resulting

theory you keep the sentences that do not have hidden symbols. Currently

a hiding removes all sentences from the theory.

This would help in some cases, but not all. Consider:

spec test =
  sort s
  pred P:s
  op a:s
  . P(a) %(axiom1)%
hide a
then
  . exists x:s . P(x) %(goal)% %implied
end

Here, the goal cannot be proved. But it can be proved in

spec test =
  sort s
  pred P:s
  op a:s
  . P(a) %(axiom1)%
hide a
then %implies
  . exists x:s . P(x) %(goal)% 
end

I think a solution would be to shift open proof goals from each node with incoming hiding links to its normal form when doing the normal form computation. A separate issue is the interaction between auto DG prover and normal form computation. The user should be guided not to move in a dead end. But maybe the shiftig of proof goals avoids dead ends.

[sternk]

Comment by clange Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1103#comment:4

---

In the setting in which I am experiencing this problem, the hiding link and the proof goals are further away from each other:

from Path/To/Lib get SpecWithHiding

spec Foo = SpecWithHiding with ... end

spec Bar = Foo then Baz then ... end

spec WhatIAmActuallyInterestedIn = Bar then
  sorts S; T
  preds p: S * T;
        q: S;
  ops   o: S -> T;
  forall x: S; y: T
  . p(x, y) %(axiom1)%
  . q(s) %(theorem1)% %implied
  . p(x, o(x)) %(theorem2)% %implied
end

What is the right way to apply your workaround in this setting? Is it

spec WhatIAmActuallyInterestedIn = Bar then
  sorts S; T
  preds p: S * T;
        q: S;
  ops   o: S -> T;
  forall x: S; y: T
  . p(x, y) %(axiom1)%
  then %implies
  . q(s) %(theorem1)%
  then %implies
  . p(x, o(x)) %(theorem2)%
end

and then "compute normal form", and then? If I didn't need the Auto DG prover before (I didn't), do I need it now, as an extra preparation step? And then, finally, I invoke the same prover as before?

[sternk]

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1103#comment:5

---

I have made your example self-contained. Then, it suffices to all "Compute normal form" and then "Auto DG prover". The proof goal at the red node should be provable with SPASS, darwin etc. (Unfortunately, the last step does not work for me due to some new problem. I will file a ticket.)

spec SpecWithHiding =
   sorts S; T
   preds p: S * T;
         q: S;
   ops   a,b: S -> T;
         s:S
   . q(s) %(axiom0)%
   hide a
end

spec Foo = SpecWithHiding with b|-> o end

spec Baz =
  sort U
end

spec Bar = Foo then Baz then sort V end

spec WhatIAmActuallyInterestedIn = Bar then
   sorts S; T
   preds p: S * T;
         q: S;
   ops   o: S -> T;
   forall x: S; y: T
   . p(x, y) %(axiom1)%
   then %implies
   . q(s) %(theorem1)%
   then %implies
   forall x:S
   . p(x, o(x)) %(theorem2)%
 end

[sternk]

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1103#comment:6

---

the new ticket is #1111