# [Easycrypt-club] conseq

Alley Stoughton alley.stoughton at icloud.com
Tue Jan 30 19:57:24 CET 2018

Hi Bas,

An explanation is below.

Best,

Alley

- - - -

require import AllCore.

module M = {
proc f(x : int, y : int) : int * int = {
return (x - 1, y + 1);
}
}.

module N = {
proc f(x : int, y : int) : int * int = {
return (x + 1, y + 1);
}
}.

lemma M_N : equiv[M.f ~ N.f : ={y} ==> res{1}.`2 = res{2}.`2].
proof. proc; auto. qed.

lemma M : hoare[M.f : 1 < x ==> 0 < res.`1].
proof. proc; auto; smt(). qed.

lemma N : hoare[N.f : x < 1 ==> res.`1 < 2].
proof. proc; auto; smt(). qed.

lemma M_N_combined :
equiv[M.f ~ N.f :
={y} /\ 1 < x{1} /\ x{2} < 1  ==>
res{1}.`2 = res{2}.`2 /\ 0 < res{1} .`1 /\ res{2}.`1 < 2].
proof.
proc.
(* you can't do

conseq M_N M N.

"do not how to combine equivF and hoareF and hoareF into equivS"

equivS refers to the statement form of an equiv, after the proc
has oppened it up

*)
conseq (_ : ={y} ==> ={y})
(_ : 1 < x ==> 0 < x)
(_ : x < 1 ==> x < 2).
smt.
auto; smt.
auto; smt.
auto.
qed.

(* or: *)

lemma M_N_combined' :
equiv[M.f ~ N.f :
={y} /\ 1 < x{1} /\ x{2} < 1  ==>
res{1}.`2 = res{2}.`2 /\ 0 < res{1} .`1 /\ res{2}.`1 < 2].
proof.
conseq M_N M N.
qed.

> On Jan 30, 2018, at 12:49 PM, Bas Spitters <b.a.w.spitters at gmail.com> wrote:
>
> I am trying to use conseq in the form
>
> conseq M_N M N.
>
> p146 of the refman.
>
> I get an error message:
> do not how to combine equivF and hoareS and hoareS into equivS
>
> What does that mean?
>
> Thanks,
>
> Bas
> _______________________________________________
> Easycrypt-club mailing list
> Easycrypt-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/easycrypt-club