From a49f76859e9a1f08f2432f654350fd2327347705 Mon Sep 17 00:00:00 2001
From: Pieter Bos <p.h.bos@student.utwente.nl>
Date: Thu, 15 Sep 2022 16:17:27 +0200
Subject: [PATCH] Bring sequence axiomatization more in line with carbon to fix
 #629 - Weakened triggers for singleton - Placed append empty left/right in
 one quantifier - Split index_over_append into left/right version, and used
 separate arithmetic functions - Phrase disequality with skolem function for
 differing index

---
 src/main/resources/dafny_axioms/sequences.vpr | 59 ++++++++++++++-----
 1 file changed, 45 insertions(+), 14 deletions(-)

diff --git a/src/main/resources/dafny_axioms/sequences.vpr b/src/main/resources/dafny_axioms/sequences.vpr
index 300ba4c3e..f7005299a 100644
--- a/src/main/resources/dafny_axioms/sequences.vpr
+++ b/src/main/resources/dafny_axioms/sequences.vpr
@@ -14,6 +14,9 @@ domain $Seq[E] {
   function Seq_drop(s: $Seq[E], n: Int): $Seq[E]
   function Seq_equal(s1: $Seq[E], s2: $Seq[E]): Bool
   function Seq_sameuntil(s1: $Seq[E], s2: $Seq[E], i: Int): Bool
+  function Seq_skolemdiff(s1: $Seq[E], s2: $Seq[E]): Int
+  function Seq_arith_add(i: Int, j: Int): Int
+  function Seq_arith_sub(i: Int, j: Int): Int
 
   axiom seq_length_non_negative {
     forall s: $Seq[E] :: {Seq_length(s)}
@@ -30,7 +33,7 @@ domain $Seq[E] {
   }
 
   axiom length_singleton_seq {
-    forall e: E :: {Seq_length(Seq_singleton(e))}
+    forall e: E :: {Seq_singleton(e)}
       Seq_length(Seq_singleton(e)) == 1
   }
 
@@ -66,24 +69,41 @@ domain $Seq[E] {
       e1 == e2
   }
 
-  axiom seq_append_empty_left { // The axiom was not in the Dafny version
-    forall s: $Seq[E] :: {Seq_append(Seq_empty(), s)}
-      Seq_append(Seq_empty(), s) == s
+  axiom seq_append_empty {
+    forall s1: $Seq[E], s2: $Seq[E] :: {Seq_append(s1, s2)}
+      (s1 == Seq_empty() ==> Seq_append(s1, s2) == s2) &&
+      (s2 == Seq_empty() ==> Seq_append(s1, s2) == s1)
   }
 
-  axiom seq_append_empty_right { // The axiom was not in the Dafny version
-    forall s: $Seq[E] :: {Seq_append(s, Seq_empty())}
-      Seq_append(s, Seq_empty()) == s
+  axiom seq_index_over_append_left {
+    forall s1: $Seq[E], s2: $Seq[E], i: Int ::
+        {Seq_index(Seq_append(s1, s2), i)}
+        {Seq_index(s1, i), Seq_append(s1, s2)}
+      s1 != Seq_empty() && s2 != Seq_empty() && 0 <= i && i < Seq_length(s1) ==> Seq_index(Seq_append(s1, s2), i) == Seq_index(s1, i)
   }
 
-  axiom seq_index_over_append {
+  axiom seq_index_over_append_right {
     forall s1: $Seq[E], s2: $Seq[E], i: Int ::
         {Seq_index(Seq_append(s1, s2), i)}
-        {Seq_index(s1, i), Seq_append(s1, s2)}
-      s1 != Seq_empty() && s2 != Seq_empty() /*&& 0 <= i && i < Seq_length(Seq_append(s1, s2))*/ ==> ( // Implication not in the Dafny version
-        i < Seq_length(s1)
-          ? Seq_index(Seq_append(s1, s2), i) == Seq_index(s1, i)
-          : Seq_index(Seq_append(s1, s2), i) == Seq_index(s2, i - Seq_length(s1)))
+      s1 != Seq_empty() && s2 != Seq_empty() && Seq_length(s1) <= i && i < Seq_length(Seq_append(s1, s2)) ==>
+        Seq_arith_add(Seq_arith_sub(i, Seq_length(s1)), Seq_length(s1)) == i &&
+        Seq_index(Seq_append(s1, s2), i) == Seq_index(s2, Seq_arith_sub(i, Seq_length(s1)))
+  }
+
+  axiom seq_index_over_append_right_inv {
+    forall s1: $Seq[E], s2: $Seq[E], i: Int ::
+        {Seq_index(s2, i), Seq_append(s1, s2)}
+      s1 != Seq_empty() && s2 != Seq_empty() && 0 <= i && i < Seq_length(s2) ==>
+        Seq_arith_sub(Seq_arith_add(i, Seq_length(s1)), Seq_length(s1)) == i &&
+        Seq_index(Seq_append(s1, s2), Seq_arith_add(i, Seq_length(s1))) == Seq_index(s2, i)
+  }
+
+  axiom seq_add_def {
+    forall i: Int, j: Int :: {Seq_arith_add(i, j)} Seq_arith_add(i, j) == i + j
+  }
+
+  axiom seq_sub_def {
+    forall i: Int, j: Int :: {Seq_arith_sub(i, j)} Seq_arith_sub(i, j) == i - j
   }
 
   axiom seq_length_invariant_over_update {
@@ -156,7 +176,7 @@ domain $Seq[E] {
   axiom extensional_seq_equality {
     forall s1: $Seq[E], s2: $Seq[E] :: {Seq_equal(s1, s2)}
       Seq_equal(s1, s2)
-        <==> // Two implications in the Dafny version
+        ==>
       (Seq_length(s1) == Seq_length(s2) &&
        forall i: Int :: {Seq_index(s1, i)} {Seq_index(s2, i)}
           0 <= i && i < Seq_length(s1) ==>
@@ -168,6 +188,17 @@ domain $Seq[E] {
       Seq_equal(s1, s2) ==> s1 == s2
   }
 
+  axiom seq_disequality_skolem {
+    forall s1: $Seq[E], s2: $Seq[E] :: {Seq_equal(s1, s2)}
+      (s1 == s2 && Seq_equal(s1, s2)) ||
+      (s1 != s2 && !Seq_equal(s1, s2) && Seq_length(s1) != Seq_length(s2)) ||
+      (s1 != s2 && !Seq_equal(s1, s2) && Seq_length(s1) == Seq_length(s2) &&
+        Seq_skolemdiff(s1, s2) == Seq_skolemdiff(s2, s1) &&
+        0 <= Seq_skolemdiff(s1, s2) && Seq_skolemdiff(s1, s2) < Seq_length(s1) &&
+        Seq_index(s1, Seq_skolemdiff(s1, s2)) != Seq_index(s2, Seq_skolemdiff(s1, s2))
+      )
+  }
+
   axiom extensional_seq_equality_prefix {
     forall s1: $Seq[E], s2: $Seq[E], n: Int :: {Seq_sameuntil(s1, s2, n)}
       Seq_sameuntil(s1, s2, n)