Another Variable Ordering Effect

[DavePearce]

(this is likely to be related to #91)

The following fails for reasons unknown:

assert "index out of bounds (not less than length)":
    forall(int[] arr2, int[] arr1, int i, int[] arr2$3, int[] arr2$2):
        if:
            arr1 == [1, 2, 64]
            arr2 == arr1
            arr2$2 == arr1[2:=i]
            arr2$3 == arr2$2
        then:
            2 < |arr2$3|

Removing arr2 == arr1 (which is not required) and this will pass.

[DavePearce]

This is definitely a variable ordering effect. Here is a modified version to emphasise this:

assert "index out of bounds (not less than length)":
    forall(int[] as, int[] bs, int[] cs, int[] ds, int i):
        if:
            as == [1, 2, 64]
            bs == as
            cs == as[2:=i]
            ds == cs
        then:
            2 < |ds|

The failing proof for this is:

81. exists(int[] as, int[] bs, int[] cs, int[] ds, int i).((((as == [1, 2,  () 
 86. exists(int[] as, int[] bs, int[] cs, int[] ds, int i).((as == [1 (Simp 81) 
 85. (as == [1, 2, 64]) && (as == bs) && (cs == as[2:=i]) && (cs  (Exists-E 86) 
 63. as == [1, 2, 64]                                                (And-E 85) 
 82. as == bs                                                        (And-E 85) 
 69. cs == as[2:=i]                                                  (And-E 85) 
 83. cs == ds                                                        (And-E 85) 
 84. 2 >= |ds|                                                       (And-E 85) 
 87. [1, 2, 64] == bs                                              (Eq-S 82,63) 
 89. cs == bs[2:=i]                                                (Eq-S 69,82) 
 90. as[2:=i] == ds                                                (Eq-S 83,69) 
 93. |ds| >= 0                                                    (ArrLen-I 84) 
 94. bs == [1, 2, 64]                                                 (Simp 87) 
 96. ds == [1, 2, 64][2:=i]                                     (Eq-S 89,83,87) 
 97. ds == as[2:=i]                                                   (Simp 90) 
 99. |as[2:=i]| >= 0                                               (Eq-S 93,90) 
 100. cs == [1, 2, 64][2:=i]                                       (Eq-S 89,94) 
 102. ds == [1, 2, i]                                                 (Simp 96) 
 103. [1, 2, 64][2:=i] == [1, 2, 64][2:=i]                      (Eq-S 97,96,63) 
 105. |as| >= 0                                                       (Simp 99) 
 106. cs == [1, 2, i]                                                (Simp 100) 
 107. as[2:=i] == [1, 2, i]                                       (Eq-S 102,97) 
 109. true                                                           (Simp 103) 
 111. |[1, 2, 64]| >= 0                                           (Eq-S 105,63) 
 112. [1, 2, 64][2:=i] == [1, 2, i]                               (Eq-S 107,63) 

This should fail by 84. 2 >= |ds| and 102. ds == [1, 2, i]. Now, if we rename say ds to as2 then it passes with this proof:

 81. exists(int[] as, int[] bs, int[] cs, int[] as2, int i).((((as == [1, 2, () 
 85. exists(int[] as, int[] bs, int[] cs, int[] as2, int i).((as == [ (Simp 81) 
 84. (as == [1, 2, 64]) && (as == bs) && (cs == as[2:=i]) && (as2 (Exists-E 85) 
 63. as == [1, 2, 64]                                                (And-E 84) 
 82. as == bs                                                        (And-E 84) 
 69. cs == as[2:=i]                                                  (And-E 84) 
 71. as2 == cs                                                       (And-E 84) 
 83. 2 >= |as2|                                                      (And-E 84) 
 86. [1, 2, 64] == bs                                              (Eq-S 82,63) 
 88. cs == bs[2:=i]                                                (Eq-S 69,82) 
 95. as2 == [1, 2, 64][2:=i]                                    (Eq-S 88,71,86) 
 100. as2 == [1, 2, i]                                                (Simp 95) 
 105. 2 >= |[1, 2, i]|                                            (Eq-S 83,100) 
 55. false                                                           (Simp 105)

Then, we can see that end up applying the substitution to give as2 == [1, 2, i] which leads to the contradiction.

[DavePearce]

Right, the issue seems to be that it makes the following substitution:

(ds == as[2:=i]) ==> ([1, 2, 64][2:=i] == [1, 2, 64][2:=i])

This effectively kills the substitution operation I suppose.

[DavePearce]

Right, this is really a relatively simple bug in CongruenceClosure. Fixed now modulo wierd knock-on effects ... :)