[Why3-club] lemma visibility

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Tue Jan 8 13:40:52 CET 2019


Dear Julia,

There is at least one way to do this, which is the following declaration:

  meta remove_prop axiom your_lemma

You can insert it either in the module containing the lemma, once you do
not need it anymore, or in a separate module which includes (uses) the
original module.

Another possibility is to use several modules and the "clone"
instruction, as follows:

  module Intf
    axiom FinalThm: forall x....
  end
  module Proof
    lemma LocalLemma1: ...
    lemma LocalLemma2: ...
    clone export Intf
  end
  module Client
    use Intf
    ...
  end

Here the client module does not see the local lemmas used to prove the
theorem. The "clone export" instruction will (by default) turn the
cloned axiom into a lemma.

Best regards,
--
Jean-Christophe (and Andrei)


On 1/4/19 4:48 PM, Julia Lawall wrote:
> Is it possible to make a lemma only visible within a module, but not
> visible to other modules that may import the module?  It seems that the
> presence or absence of some irrelevant lemmas can have a big impact on
> whether at least Alt-Ergo can succeed in doing some proofs in a reasonable
> amount of time.
> 
> thanks,
> julia
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> 


More information about the Why3-club mailing list