Dafny 用量词反证法证明

Question

我正在尝试在 Dafny 中通过反证法证明传递关系的并集也是传递的，但我不太确定如何使用 Dafny 语法形成论点。我可以只展示一个反例还是我需要写出所有可能的情况？其次，我是否需要 relax/restate 得出结论，即存在一些不具有传递性的传递关系的并集？

predicate relationOnASet<T>(R: set<(T,T)>, S: set<T>) {
    forall ts :: ts in R ==> ts.0 in S && ts.1 in S
}
predicate transitive<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    forall a,b,c :: a in S && b in S && c in S && (a,b) in R && (b,c) in R ==> (a,c) in R
}

lemma transitiveUnionContra<T>(R_1: set<(T,T)>, S_1: set<T>, R_2: set<(T,T)>, S_2: set<T>)
    requires |R_1| > 0
    requires |R_2| > 0
    requires |S_1| > 0
    requires |S_2| > 0
    requires relationOnASet(R_1, S_1)
    requires relationOnASet(R_2, S_2)
    requires transitive(R_1, S_1)
    requires transitive(R_2, S_2)
    ensures !transitive(R_1+R_2, S_1+S_2) 
{
    if transitive(R_1 + R_2, S_1+S_2) {
        forall a,b,c | a in S_1+S_2 && b in S_1+S_2 && c in S_1+S_2 && (a,b) in R_1+R_2 && (b,c) in R_1+R_2 
            ensures (a,c) in R_1+R_2 
        {
            if a in S_1 && a !in S_2 && b in S_1 && b in S_2 && c in S_2 && c !in S_1 {
                assert (a,c) !in R_1;
                assert (a,c) !in R_2;
                assert (a,c) !in R_1+R_2;
                assert false;
            }
        } 
    }
}

Answer 1

你的引理说，对于每个传递关系 R_1，R_2，R_1 + R_2 不是传递关系。但是确实存在这样的关系 R_1 = {(a, b)} 和 R_2 = {(a, b), (b, c), (a, c)}.

这是在 dafny 中表达原始引理的尝试。

predicate relationOnASet<T> (R : set<(T,T)>, S : set<T>) {
    forall ts :: ts in R ==> ts.0 in S && ts.1 in S
}
predicate transitive<T>(R: set<(T,T)>, S: set<T>)
    requires relationOnASet(R, S)
{
  forall a, b, c ::
    a in S &&
    b in S &&
    c in S &&
    (a, b) in R &&
    (b, c) in R ==> (a, c) in R
}

lemma transitiveUnionContra<T>()
  returns (
  R1: set<(T, T)>, S1: set<T>,
  R2: set<(T, T)>, S2: set<T>)
  ensures relationOnASet(R1, S1)
  ensures relationOnASet(R2, S2)
  ensures transitive(R1, S1)
  ensures transitive(R2, S2)
  ensures ! transitive(R1 + R2, S1 + S2)
{
  var a : T :| assume true;
  var b : T :| assume a != b;
  var c : T :| assume a != c && b != c;
  S1 := {a, b};
  S2 := {b, c};
  R1 := {(a, b)};
  R2 := {(b, c)};
}

lemma notTrueAlways<T>()
  ensures !
  (forall S1 : set<T>, S2 : set<T>, R1 : set<(T,T)>, R2 : set<(T, T)> ::
  relationOnASet(R1, S1) &&
  relationOnASet(R2, S2) &&
  transitive(R1, S1) &&
  transitive(R2, S2)  ==> transitive(R1 + R2, S1 + S2)
  )
{
  var a, b, c, d := transitiveUnionContra<T>();
}

用很少的假设凭空拉出三个不同的元素。

Dafny 用量词反证法证明

Dafny proof by contradiction with quantifiers

proof

dafny

set-theory