[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

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