[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
More information about the Agda
mailing list