# [Agda] Re: Classical Mathematics for a Constructive World

Jan Burse janburse at fastmail.fm
Sun Dec 2 11:10:01 CET 2012

```wren ng thornton schrieb:
> You run into similar issues in separation logic. When using Hoare
> separation logic we get this nice frame rule:
>
>      {P}   C {Q}
>      -------------
>      {P*R} C {Q*R}
>
> (subject to some mild side conditions about R). People often focus on
> the fact that the addition of R is preserved from precondition to
> postcondition

Correctness wise I guess the above inference
rule is in most cases invalid. Take the following
example:

{ x = 0 v x = 1 }
x = x + 1
{ x = 1 v x = 2 }

Now add the condition x = 0:

{ x = 0 }
x = x + 1
{ false }

What it needs is x = a & x = b -> false
for a <> b. Should be possible in minimal
logic without any choice principle. Its
would be for example part of CET (Clark
Equational Theory). So I guess it is not
related. But I might be wrong.

Or what would be the mild condition on R
to make the inference rule meaningful?

Bye

```