prove spec of Nat.div and Nat.mod

except recursive call assumptions

base/Nat/add/swap.kind

@@ -0,0 +1,6 @@
+Nat.add.swap(
+  a: Nat
+  b: Nat
+  c: Nat
+): Equal(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)))
+  ?Nat.add.swap

base/Nat/div_mod/go/succ_quotient.kind

@@ -0,0 +1,11 @@
+Nat.div_mod.go.succ_quotient(
+  d: Nat, q: Nat, r: Nat
+): Equal(
+    Pair(Nat, Nat)
+    Nat.div_mod.go(d, q, r)(
+      () Pair(Nat, Nat)
+      (fst, snd) Pair.new(Nat, Nat, Nat.succ(fst), snd)
+    )
+    Nat.div_mod.go(d, Nat.succ(q), r)
+  )
+  ?Nat.div_mod.go.succ_quotient

base/Nat/div_mod/spec.kind

@@ -1,3 +1,8 @@
+// n = r + q*d
+// r < n
+// --------------
+// r = Nat.mod(n, d)
+// q = Nat.div(n, d)
 Nat.div_mod.spec(
   n: Nat
   q: Nat
@@ -6,4 +11,41 @@ Nat.div_mod.spec(
   H0: Equal(Nat, n, Nat.add(r, Nat.mul(q, d)))
   H1: Equal(Bool, Nat.lte(Nat.succ(r), d), true)
 ): Equal(Pair<Nat, Nat>, Pair.new(Nat, Nat, q, r), Nat.div_mod(n, d))
-  ?test
+  case q with H0 {
+    zero:
+      let H0 = case Nat.add.zero_right(r) {
+        refl:
+          mirror(H0)
+      }: Equal(Nat, self.b, n)
+      case H0 {
+        refl:
+          let H1 = mirror(Nat.lte.comm.true(r, d, H1))
+          case H1 {
+            refl:
+              refl
+          }: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,0,r), H1.b((self) Pair(Nat,Nat),Nat.div_mod.go(d,1,Nat.sub(r,d)),Pair.new(Nat,Nat,0,r)))
+      }: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,0,r), Nat.div_mod(H0.b,d))
+    succ:
+      let H1 = mirror(Nat.lte.comm.true(r, d, H1))
+      let H0 = mirror(H0)
+      case H0 {
+        refl:
+          let pre_cond = mirror(Nat.lte.slack_right(d, d, Nat.add(r,Nat.mul(q.pred,d)), Nat.Order.refl(d)))
+          let cond = case Nat.add.swap(d, r, Nat.mul(q.pred,d)) {
+            refl:
+              pre_cond
+          }: Equal(Bool, Bool.true, Nat.lte(d, self.b))
+          case cond {
+            refl:
+              let succ_out = Nat.div_mod.go.succ_quotient(d, 0, Nat.sub(n,d))
+              case succ_out {
+                refl:
+                  let ind = Nat.div_mod.spec(Nat.sub(n, d), q.pred, d, r, ?H0, ?H1)
+                  case ind {
+                    refl:
+                      refl
+                  }: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), ind.b(() Pair(Nat,Nat),(fst) (snd) Pair.new(Nat,Nat,Nat.succ(fst),snd)))
+              }: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), succ_out.b)
+          }: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), cond.b((self) Pair(Nat,Nat),Nat.div_mod.go(d,1,Nat.sub(n,d)),Pair.new(Nat,Nat,0,n)))
+      }: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), Nat.lte(d, H0.b,(self) Pair(Nat,Nat),Nat.div_mod.go(d,1,Nat.sub(n,d)),Pair.new(Nat,Nat,0,n)))
+  }!

base/Nat/lte/slack_right.kind

@@ -0,0 +1,6 @@
+Nat.lte.slack_right(
+  a: Nat, b: Nat, c: Nat
+  H: Equal(Bool, Nat.lte(a, b), true)
+): Equal(Bool, Nat.lte(a, Nat.add(b, c)), true)
+  ?Nat.lte.slack_right
+

base/Nat/ltn/mul.kind

@@ -1,3 +1,8 @@
 // TODO
 Nat.ltn.mul(
-)
+  a: Nat
+  b: Nat
+  c: Nat
+  H: Equal(Bool, Nat.ltn(a, b), true)
+): Equal(Bool, Nat.ltn(Nat.mul(c, a), Nat.mul(c, b)), true)
+  ?Nat.ltn.mul

base/Nat/mod/mul_both.kind

@@ -1,10 +1,28 @@
+// a*(b%c) == (a*b)%(a*c)
 Nat.mod.mul_both(
   a: Nat
   b: Nat
   c: Nat
   H0: Equal(Bool, Nat.lte(1, a), true)
   H1: Equal(Bool, Nat.lte(1, c), true)
-// a*(b%c) == (a*b)%(a*c)
 ): Equal(Nat, Nat.mul(a, Nat.mod(b, c)), Nat.mod(Nat.mul(a, b), Nat.mul(a, c)))
   let bound_lemma = Nat.lte.comm.false(c, Nat.mod(b, c), Nat.mod.small(b, c, H1))
-  ?mul_both
+  let bound = Nat.ltn.mul( Nat.mod(b,c), c, a, bound_lemma)
+  let id_lemma = Nat.div_mod.recover(b, c, H1)
+  let id_lemma = apply(Nat.mul(a), id_lemma)
+  let distrib = Nat.mul.distrib_left(a,Nat.mod(b,c),Nat.mul(Nat.div(b,c),c))
+  let id_lemma = case distrib {
+    refl:
+      id_lemma
+  }: Equal(Nat, distrib.b, Nat.mul(a,b))
+  let id_lemma = case Nat.mul.swap(a, Nat.div(b,c), c) {
+    refl:
+      id_lemma
+  }: Nat.add(Nat.mul(a,Nat.mod(b,c)), self.b) == Nat.mul(a,b)
+  // Nat.add(Nat.mul(a,Nat.mod(b,c)),Nat.mul(Nat.div(b,c),Nat.mul(a,c))) == Nat.mul(a,b)
+  let almost_qed = Nat.div_mod.spec(Nat.mul(a, b), Nat.div(b,c), Nat.mul(a,c), Nat.mul(a,Nat.mod(b,c)), mirror(id_lemma), bound)
+  let qed = apply(Pair.snd(Nat, Nat), almost_qed)
+  case qed {
+    refl:
+      refl
+  }: Equal(Nat, Nat.mul(a,Nat.mod(b,c)), qed.b)

base/Nat/mul/swap.kind

@@ -0,0 +1,6 @@
+Nat.mul.swap(
+  a: Nat
+  b: Nat
+  c: Nat
+): Equal(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)))
+  ?Nat.mul.swap