Coq realizations should require to prove `goal`s (at least if they come from cloning)
Consider the following source code (say f.mlw
)
module M1
use int.Int
constant c : int
axiom c_spec : c >= 17
constant d : int
axiom d_spec : d >= c
goal d_prop : d >= 10
end
module M2
use int.Int
constant c : int = 42
clone M1 with
constant c = c,
goal c_spec,
axiom .
goal d_moreprop : d >= 40
end
When trying to prove the goal in the IDE, I got exactly the tasks I expect: for the module M1
I need to prove the goal d_prop
, for M2
I need to prove c_spec
and d_moreprop
.
If I ask to realize these modules in Coq, using commands
why3 realize -D coq-realize -L . -T f.M1 -o tmp
why3 realize -D coq-realize -L . -T f.M2 -o tmp
then for M1.v
I have to define c
, prove c_spec
, define d
and prove d_spec
, but not to prove d_prop
. That surprises me, although one could argue that when using the module M1, the goal d_prop
would not be visible so not need to prove it.
for M2.v
I need to define d
and prove d_spec
that's all. Not only I don't have to prove d_moreprop
, similarly as before, but I don't need to prove c_spec
. This seems to me a mistake, indeed a possible source of unsoundness of realizations.
Am I right? maybe @melquion some thoughts?