using a theorem to prove an invariant: `with p=q` fails

microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.

Other

223 stars 80 forks source link

using a theorem to prove an invariant: `with p=q` fails #70

Closed nano-o closed 4 years ago

nano-o commented 4 years ago

This fails with error: unknown symbol: q

#lang ivy1.7

axiom [my_axiom] {
    individual p:bool
    property true
}

individual q:bool

invariant true
proof {
    apply my_axiom with p = q
}

kenmcmil commented 4 years ago

Fixed in commit d52be27. Thanks.