new theorems

abstract_syntax.py

@@ -3039,8 +3039,10 @@ def count_marks(formula):
       return count_marks(rhs) + count_marks(body)
     case Hole(loc2, tyof):
       return 0
+    case ArrayGet(loc, tyof, arr, ind):
+      return count_marks(arr) + count_marks(ind)
     case _:
-      error(loc, 'in count_marks function, unhandled ' + str(formula))
+      error(formula.location, 'in count_marks function, unhandled ' + str(formula))
 
 def find_mark(formula):
   match formula:
@@ -3092,6 +3094,9 @@ def find_mark(formula):
       find_mark(body)
     case Hole(loc2, tyof):
       pass
+    case ArrayGet(loc2, tyof, arr, ind):
+      find_mark(arr)
+      find_mark(ind)
     case _:
       error(loc, 'in find_mark function, unhandled ' + str(formula))
 
@@ -3141,6 +3146,8 @@ def replace_mark(formula, replacement):
                   replace_mark(body, replacement))
     case Hole(loc2, tyof):
       return formula
+    case ArrayGet(loc2, tyof, arr, ind):
+      return ArrayGet(loc2, tyof, replace_mark(arr, replacement), replace_mark(ind, replacement))
     case _:
       error(loc, 'in replace_mark function, unhandled ' + str(formula))
 

lib/Base.pf

@@ -76,6 +76,34 @@ proof
   }
 end
 
+theorem iff_symm: all P:bool, Q:bool.
+  if (P ⇔ Q) then (Q ⇔ P)
+proof
+  arbitrary P:bool, Q:bool
+  assume: P ⇔ Q
+  have fwd: if Q then P by assume: Q apply (recall P ⇔ Q) to (recall Q)
+  have bkwd: if P then Q by assume: P apply (recall P ⇔ Q) to (recall P)
+  fwd, bkwd
+end
+
+theorem iff_trans: all P:bool, Q:bool, R:bool.
+  if (P ⇔ Q) and (Q ⇔ R) then P ⇔ R
+proof
+  arbitrary P:bool, Q:bool, R:bool
+  assume prem: (P ⇔ Q) and (Q ⇔ R)
+  have fwd: if P then R by {
+    assume: P
+    have: Q by apply prem to recall P
+    conclude R by apply prem to recall Q
+  }
+  have bkwd: if R then P by {
+    assume: R
+    have: Q by apply prem to recall R
+    conclude P by apply prem to recall Q
+  }
+  fwd, bkwd
+end
+
 theorem contrapositive : all P : bool, Q : bool.
   if (if P then Q) and not Q then not P
 proof

lib/Nat.pf

@@ -1,4 +1,5 @@
 import Option
+import Base
 
 union Nat {
   zero
@@ -1342,6 +1343,39 @@ proof
   }
 end
 
+theorem sub_pos_iff_less: all x: Nat, y:Nat. y < x ⇔ 0 < x - y
+proof
+  induction Nat
+  case 0 {
+    arbitrary y:Nat
+    have fwd: if y < 0 then 0 < 0 - y by
+        definition {operator<, operator≤}
+    have bkwd: if 0 < 0 - y then y < 0 by
+        definition {operator-, operator<, operator≤}
+    fwd, bkwd
+  }
+  case suc(x') assume IH {
+    arbitrary y:Nat
+    switch y {
+      case 0 {
+        have fwd: if 0 < suc(x') then 0 < suc(x') - 0
+            by assume _ definition {operator-,operator<, operator≤,operator≤}
+        have bkwd: if 0 < suc(x') - 0 then 0 < suc(x')
+            by assume _ definition {operator<, operator≤, operator≤}
+        fwd, bkwd
+      }
+      case suc(y') {
+        have IH': y' < x' ⇔ 0 < x' - y' by IH[y']
+        suffices suc(y') < suc(x') ⇔ 0 < x' - y' by definition operator-
+        have syx_yx: suc(y') < suc(x') ⇔ y' < x'
+            by apply iff_symm[y' < x',suc(y') < suc(x')] to less_suc_iff_suc_less[y',x']
+        apply iff_trans[suc(y') < suc(x'), y' < x', 0 < x' - y']
+        to syx_yx, IH'
+      }
+    }
+  }
+end
+
 // NOTE: This has to be after dichotomy, so it can't be with the other mult theorems
 theorem dist_mult_sub : all x : Nat. all y : Nat, z : Nat.
   x * (y - z) = x * y - x * z
@@ -2020,6 +2054,46 @@ proof
   div2_suc_double[n]
 end
 
+lemma div2_aux_pos_less: all n:Nat. if 0 < n then div2(n) < n and div2_aux(n) ≤ n
+proof
+  induction Nat
+  case 0 {
+    assume: 0 < 0
+    conclude false by apply less_irreflexive to recall 0 < 0
+  }
+  case suc(n') assume IH {
+    assume: 0 < suc(n')
+    switch n' {
+      case 0 {
+        definition {div2, div2_aux, operator<, operator≤, operator≤, div2}
+      }
+      case suc(n'') assume np_eq {
+        have: 0 < n' by {
+            suffices 0 < suc(n'') by rewrite np_eq
+            definition {operator<, operator≤, operator≤}
+        }
+        have IH': div2(n') < n' and div2_aux(n') ≤ n' by apply IH to (recall 0 < n')
+        suffices div2_aux(n') < suc(n') and div2_aux(suc(n')) ≤ suc(n')
+            by definition {div2} and rewrite (symmetric np_eq)
+        have _1: div2_aux(n') < suc(n') by {
+            suffices div2_aux(n') ≤ n' by definition {operator<, operator≤}
+            conjunct 1 of IH'
+        }
+        have _2: div2_aux(suc(n')) ≤ suc(n') by {
+           suffices div2(n') ≤ n' by definition {div2_aux, operator≤}
+           apply less_implies_less_equal to conjunct 0 of IH'
+        }
+        _1, _2
+      }
+    }
+  }
+end
+
+theorem div2_pos_less: all n:Nat. if 0 < n then div2(n) < n
+proof
+  div2_aux_pos_less
+end
+
 /*
  Properties of pos2nat
  */

proof_checker.py

@@ -254,6 +254,10 @@ def rewrite_aux(loc, formula, equation):
 
     case TAnnote(loc2, tyof, subject, typ):
       return TAnnote(loc, tyof, rewrite_aux(loc, subject, equation), typ)
+
+    case ArrayGet(loc2, tyof, arr, ind):
+      return ArrayGet(loc, tyof, rewrite_aux(loc, arr, equation),
+                      rewrite_aux(loc, ind, equation))
 
     case TLet(loc2, tyof, var, rhs, body):
       return TLet(loc2, tyof, var, rewrite_aux(loc, rhs, equation),
@@ -2098,7 +2102,10 @@ def type_check_term(term, typ, env, recfun, subterms):
             except Exception as e:
               pass
       if var_typ == typ:
-        return Var(loc, typ, rs[0], [ rs[0] ])
+        if len(rs) > 0:
+            return Var(loc, typ, rs[0], [ rs[0] ])
+        else:
+            return Var(loc, typ, name, [name])
       else:
         error(loc, 'expected a term of type ' + str(typ) \
               + '\nbut got term ' + str(term) + ' of type ' + str(var_typ))