It works! Thanks. This will help a lot, I have tons of let-lemmas ;)
Virginia
> Le 26 juin 2020 à 15:26, Raphael Rieu-Helft <raphael.rieu-he...@lri.fr> a
> écrit :
>
> Hi Virginia,
>
> Since your first lemma is already a let-lemma, you can simply call it in the
> body of the second lemma instead of asserting its postcondition.
> let lemma aux1 (f : int -> fset 'a) (a i b : int)
> requires { disjoint_sets f a b }
> requires { a<= i < b }
> ensures { diff (umap f a i) (f i) = umap f a i } =
> disjoint_umap_upperbound f a i b
>
> Best,
> Raphael
>
> On 26/06/2020 15:21, Virginia Aponte wrote:
>> Hi everybody,
>>
>> I am working with disjoint sets and disjoint unions over a container
>> specified via some map. I am having troubles making some of my lemmas to be
>> used by alt-ergo or cvs. I understand that that one must be careful when
>> relying on extensionality, but I wouldn't say this is the case in this
>> particular exemple. When trying to prove the aux1 lemma, the first lemma is
>> necessary to prove the assertion. But it does not seem to be used by
>> Alt-ergo nor CVS. Of course, everything goes ok if I switch to Coq and do
>> some eapply+omega on the first lemma.
>>
>> let rec lemma disjoint_umap_upperbound (f: int -> fset 'a) (a i b: int)
>> requires { disjoint_sets f a b }
>> requires { a<= i < b }
>> ensures { disjoint (umap f a i) (f i) }
>> variant { i - a } =
>> if i-a = 0 then assert { umap f a i = empty }
>> else if i-a = 1 then
>> (assert {umap f a i = f a}; assert {disjoint (f i) (f a)})
>> else if i-a > 1 then disjoint_umap_upperbound f (a+1) i b
>>
>> let lemma aux1 (f : int -> fset 'a) (a i b : int)
>> requires { disjoint_sets f a b }
>> requires { a<= i < b }
>> ensures { diff (umap f a i) (f i) = umap f a i } =
>> assert { disjoint (umap f a i) (f i) }
>>
>> How can I improve the triggering here? Is the problem related with the use
>> of a function parameter in these properties?
>>
>> Virginia
>>
>>
>>
>> _______________________________________________
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr <mailto:Why3-club@lists.gforge.inria.fr>
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>> <https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
