Handle `conseq` when the combined statement has a non-empty ambient logic context.

[fdupress]

I was trying out this PR and I still get some issues with combining lossless with hoare to get phoare.
I don't know why, but this is the pattern that fails with invalid goal:

require import AllCore FMap.


module Foo = {
   proc foo(i :int, a : (int,int) fmap) = {
           a.[i] <- oget a.[i] + 1;
           return a;
   }
}.

lemma foo_ll : islossless Foo.foo by islossless.

lemma foo_h _i _a :
   hoare [ Foo.foo : i = _i /\ a = _a ==>
     forall j, j<>_i =>  _a.[j] = res.[j]] by proc;auto;smt(FMap.get_setE).

lemma foo_p _i _a : phoare [ Foo.foo : i = _i /\ a = _a ==>
     forall j, j<>_i =>  _a.[j] = res.[j]] = 1%r
   by conseq foo_ll (foo_h _i _a).

_Originally posted by @mbbarbosa in https://github.com/EasyCrypt/easycrypt/pull/837#issuecomment-3619981606_

[oskgo]

@mbbarbosa You can use seq as an ugly workaround until I figure out how to fix this:

require import AllCore FMap.

module Foo = {
   proc foo(i :int, a : (int,int) fmap) = {
           a.[i] <- oget a.[i] + 1;
           return a;
   }
}.

lemma foo_ll : islossless Foo.foo by islossless.

lemma foo_h _i _a :
   hoare [ Foo.foo : i = _i /\ a = _a ==>
     forall j, j<>_i =>  _a.[j] = res.[j]] by proc;auto;smt(FMap.get_setE).

lemma foo_p _i _a : phoare [ Foo.foo : i = _i /\ a = _a ==>
     forall j, j<>_i =>  _a.[j] = res.[j]] = 1%r.
proc*.
seq 2: true 1%r 1%r _ 0%r #post => //.
- call (foo_h _i _a); auto.
call foo_ll; auto.

EDIT: Another workaround is to define an operator abstracting away the quantifier in the post of the hoare statement.

require import AllCore FMap.

module Foo = {
   proc foo(i :int, a : (int,int) fmap) = {
           a.[i] <- oget a.[i] + 1;
           return a;
   }
}.

lemma foo_ll : islossless Foo.foo by islossless.

op po (_i:int) (_a: (int, int) fmap) r = forall j, j<>_i =>  _a.[j] = r.[j].

lemma foo_h _i _a :
   hoare [ Foo.foo : i = _i /\ a = _a ==>
     po _i _a res] by proc;auto;smt(FMap.get_setE).

lemma foo_p _i _a : phoare [ Foo.foo : i = _i /\ a = _a ==>
     forall j, j<>_i =>  _a.[j] = res.[j]] = 1%r.
conseq foo_ll (foo_h _i _a).

[oskgo]

Minimization:

require import Real.

module Foo = {proc foo() = {}}.

lemma foo_ll : islossless Foo.foo by islossless.

op [opaque] p = predT<:int>.

lemma foo_h: hoare [ Foo.foo : true ==> forall j, p j]. 
proof. by proc; auto => /> j; rewrite /p. qed.

lemma foo_p: phoare[ Foo.foo : true ==> forall j, p j] = 1%r.
conseq foo_ll foo_h.

Yes, the [opaque] is necessary.