half a proof

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
  mutual
    *-distribʳ :  {n} (x y z : BitVector n)  (y + z) * x  (y * x) + (z * x)
    *-distribʳ [] [] [] = refl
    *-distribʳ {Nsuc n} xs ys zs = *-distribʳ1 xs ys zs

    *-distribʳ1 :  {n} (x y z : BitVector (Nsuc n))  (y + z) * x  (y * x) + (z * x)
    *-distribʳ1 xs (0#  ys) (0#  zs) rewrite *-distribʳ (droplast xs) ys zs = refl
    *-distribʳ1 (0#  xs) (0#  ys) (1#  zs)
             rewrite *-distribʳ (droplast (0#  xs)) ys zs
                   | sym (assoc xs (ys * droplast (0#  xs)) (zs * droplast (0#  xs)))
                   | comm xs (ys * droplast (0#  xs))
                   | assoc (ys * droplast (0#  xs)) xs (zs * droplast (0#  xs)) = refl
    *-distribʳ1 (1#  xs) (0#  ys) (1#  zs)
             rewrite *-distribʳ (droplast (1#  xs)) ys zs
                   | sym (assoc xs (ys * droplast (1#  xs)) (zs * droplast (1#  xs)))
                   | comm xs (ys * droplast (1#  xs))
                   | assoc (ys * droplast (1#  xs)) xs (zs * droplast (1#  xs)) = refl
    *-distribʳ1 (0#  xs) (1#  ys) (0#  zs)
             rewrite *-distribʳ (droplast (0#  xs)) ys zs
                   | assoc xs (ys * droplast (0#  xs)) (zs * droplast (0#  xs)) = refl
    *-distribʳ1 (1#  xs) (1#  ys) (0#  zs)
             rewrite *-distribʳ (droplast (1#  xs)) ys zs
                   | assoc xs (ys * droplast (1#  xs)) (zs * droplast (1#  xs)) = refl
    *-distribʳ1 (0#  xs) (1#  ys) (1#  zs) rewrite extract-carry ys zs 
                                                    | *-distribʳ (droplast (0#  xs)) (one _) (add 0# ys zs) 
                                                    | *-distribʳ (droplast (0#  xs)) ys zs 
                                                    | assoc xs (ys * droplast (0#  xs)) (xs + (zs * droplast (0#  xs)))
                                                    | sym (assoc (ys * droplast (0#  xs)) xs (zs * droplast (0#  xs)))
                                                    | comm (ys * droplast (0#  xs)) xs 
                                                    | assoc xs (ys * droplast (0#  xs)) (zs * droplast (0#  xs))
                                                    | sym (assoc xs xs ((ys * droplast (0#  xs)) + (zs * droplast (0#  xs))))
                                                    | *-identityˡ (droplast (0#  xs))
                                                    | shift-to-add 0# xs
                                                    = refl
    *-distribʳ1 (1#  xs) (1#  ys) (1#  zs) = cong (__ 0#) {!!}