substitution looking good

base/Nat/max/big.kind

@@ -0,0 +1,25 @@
+Nat.max.big(
+  a: Nat
+  b: Nat
+): And<Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true), Equal<Bool>(Nat.lte(b, Nat.max(a,b)), true)>
+  def cmp_ab = Nat.lte(a, b)
+  let lemma_ab = Equal.refl!(cmp_ab)
+  (case cmp_ab {
+    true:
+      (lemma_ab)
+        Pair.new!!(lemma_ab, Nat.Order.refl(b))
+    false:
+      (lemma_ab)
+        let lemma_ba = Nat.lte.comm.false!!(lemma_ab)
+        Pair.new!!(Nat.Order.refl(a), lemma_ba)
+  }: (lemma_ab: Equal<Bool>(Nat.lte(a, b), cmp_ab)) -> And<
+    Equal<Bool>(Nat.lte(a, case cmp_ab { true: b, false: a }), true),
+    Equal<Bool>(Nat.lte(b, case cmp_ab { true: b, false: a }), true)>)(
+    lemma_ab
+  )
+
+Nat.max.big.left(a: Nat, b: Nat): Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true)
+  Pair.fst!!(Nat.max.big(a, b))
+
+Nat.max.big.right(a: Nat, b: Nat): Equal<Bool>(Nat.lte(b, Nat.max(a,b)), true)
+  Pair.snd!!(Nat.max.big(a, b))

base/Test.kind

@@ -38,42 +38,104 @@ Nat.AddExp.dimension.zero(
         unit
     var:
       (Hyp)
-        ?var
+        let contra = Nat.succ_neq_zero!(Hyp)
+        Empty.absurd!(contra)
     add:
       (Hyp)
-        def left_dim = Nat.AddExp.dimension(exp.left)
-        let left_lemma =
-          (case left_dim {
-            zero:
-              (left_dim, Hyp)
-                ?zero
-            succ:
-              (left_dim, Hyp)
-                ?succ
-          }: (left_dim: Nat
-              Hyp: Equal<Nat>(Nat.max(left_dim, Nat.AddExp.dimension(exp.right)), 0)) ->
-              Equal<Nat>(left_dim, 0))(
-            left_dim,
-            Hyp
-          )
-//        let left = Nat.AddExp.dimension.zero(exp.left)
-//        let right = Nat.AddExp.dimension.zero(exp.right)
-        ?add
-        //Pair.new!!(left, right)
+        let {left_small, right_small} = Nat.max.big(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
+        def max = Nat.max(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
+        let left_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
+          max, 0, Hyp,
+          (x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.left), x), true),
+          left_small
+        ))
+        let right_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
+          max, 0, Hyp
+          (x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.right), x), true),
+          right_small
+        ))
+        let left = Nat.AddExp.dimension.zero(exp.left, left_zero)
+        let right = Nat.AddExp.dimension.zero(exp.right, right_zero)
+        Pair.new!!(left, right)
   }: (Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))(
     Hyp
   )
 
+Nat.AddExp.compute(
+  exp: Nat.AddExp
+  Hyp: Nat.AddExp.constant(exp)
+): Nat
+  case exp with Hyp {
+    const:
+      exp.value
+    var:
+      Empty.absurd!(Hyp)
+    add:
+      open Hyp
+      Nat.add(Nat.AddExp.compute(exp.left, Hyp.fst), Nat.AddExp.compute(exp.right, Hyp.snd))
+  }!
+
 Nat.AddExp.substitution(
   exp: Nat.AddExp
 ): Variadic(Nat.AddExp.dimension(exp), Nat, Nat)
-  ?substitution
+  def dim = Nat.AddExp.dimension(exp)
+  def Hyp = Nat.Order.refl(dim)
+  Nat.AddExp.substitution.aux0(dim, exp, Hyp)
 
-Nat.AddExp.substitution.aux(
+Nat.AddExp.substitution.aux0(
   n: Nat
   exp: Nat.AddExp
+  Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), n), true)
 ): Variadic(n, Nat, Nat)
-  ?substitution
+  case n with Hyp {
+    zero:
+      def Hyp = Nat.Order.chain.aux!(Hyp)
+      def Hyp = Nat.AddExp.dimension.zero!(Hyp)
+      Nat.AddExp.compute(exp, Hyp)
+    succ:
+      (value)
+        def new_exp = Nat.AddExp.substitution.aux1(exp, value, Nat.succ(n.pred))
+        let Hyp = Nat.AddExp.substitution.aux2(exp, value, Nat.succ(n.pred), Hyp)
+        Nat.AddExp.substitution.aux0(n.pred, new_exp, Hyp)
+  }!
+
+Nat.AddExp.substitution.aux1(
+  exp: Nat.AddExp
+  value: Nat
+  idx: Nat
+): Nat.AddExp
+  case exp {
+    const:
+      exp
+    var:
+      case Nat.lte(idx, exp.idx) {
+        true:
+          Nat.AddExp.const(value)
+        false:
+          exp
+      }
+    add:
+      Nat.AddExp.add(
+        Nat.AddExp.substitution.aux1(exp.left, value, idx)
+        Nat.AddExp.substitution.aux1(exp.right, value, idx)
+      )
+  }
+
+Nat.AddExp.substitution.aux2(
+  exp: Nat.AddExp
+  value: Nat
+  idx: Nat
+  Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), idx), true)
+): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx)
+   Equal<Bool>(Nat.lte(Nat.AddExp.dimension(new_exp), Nat.pred(idx)), true)
+  case exp with Hyp {
+    const:
+      Equal.refl<Bool>(true)
+    var:
+      ?var
+    add:
+      ?add
+  }!
 
 Test: _
   "hi"