search

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

Name clash in rule application #66

Closed nano-o closed 4 years ago

nano-o commented 4 years ago

Consider

type t
theorem [thm1] {
    relation p(X1:t,X2:t)
    property forall X1,X2 . p(X1,X2)
}
proof {
    apply introA;
    apply introA
}

This fails with error: symbol x is captured in substitution. Can I make this work somehow? I'm trying to obtain a goal of the form p(x1,x2) for two individuals x1 and x2.

kenmcmil commented 4 years ago

Do it with a substitution, like this:

#lang ivy1.7

include deduction

type t
theorem [thm1] {
    relation p(X1:t,X2:t)
    property forall X1,X2 . p(X1,X2)
}
proof {
    apply introA<x1/x>;
    showgoals;
    apply introA<x2/x>;
    showgoals

}

This gives


giuliano8.ivy: line 12: Proof goals:

theorem [sch25] {
    relation p(V0:t,V1:t)
    individual x1 : t
    property forall X2. p(x1,X2)
}

giuliano8.ivy: line 14: Proof goals:

theorem [sch25] {
    relation p(V0:t,V1:t)
    individual x1 : t
    individual x2 : t
    property p(x1,x2)
}