Dafny proof by contradiction with quantifiers

Question

I'm trying to write a proof by contradiction in Dafny for the union of transitive relations being also transitive and I'm not quite sure how to form the arguments with dafny syntax. Can I just show one counter example or do I need to write out all possible cases? Secondly, do I need to relax/restate the conclusion to that there exists some unions of transitive relations which are not also transitive?

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

Your lemma says that for every transitive relations R_1, R_2 it is not case that R_1 + R_2 is transitive relation. But there do exists such relation R_1 = {(a, b)} and R_2 = {(a, b), (b, c), (a, c)}.

Here is an attempt to express original lemma in 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>();
}

Using few assumes to pull three different element out of type out of thin air.