total rewrite of polynomials

leesongun

Mar 11, 2023, 11:20 PM

2QLPCGXFMHV6EF5SVXUQ4UVVVH55XMJAMMNA64IK3J7QD3ZIZO5QC

Dependencies

• [2] QHHC3PPI record old implementation of Polynomial

Change contents

• edit in Data/Polynomial.idr at line 4
  [2.96]

  [2.96]
  +

  + %default total
• replacement in Data/Polynomial.idr at line 18
  [2.361]→[2.361:411](∅→∅)
  − addzero : {x:Poly} -> ([] + x = x)

  − addzero = Refl
  [2.361]

  [2.411]
  + addzero : (x:Poly) -> [] + x = x

  + addzero x = Refl
• replacement in Data/Polynomial.idr at line 21
  [2.412]→[2.412:539](∅→∅)
  − eqList : {x,y:ty} -> {xs, ys:List ty} -> x=y -> xs=ys -> x::xs = y::ys

  − eqList Refl Refl = Refl

  −

  − h1 : (x:Poly) -> (x ++ [] = x)
  [2.412]

  [2.539]
  + h1 : (x:Poly) -> x ++ [] = x
• replacement in Data/Polynomial.idr at line 23
  [2.552]→[2.552:654](∅→∅)
  − h1 (x::xs) = cong (x::) (h1 xs)

  −

  − h2 : (x:Poly) -> (x + [] = x ++ [])

  − h2 [] = Refl

  − h2 (x :: xs) = Refl
  [2.552]

  [2.654]
  + h1 (x::xs) = rewrite (h1 xs) in Refl
• replacement in Data/Polynomial.idr at line 26
  [2.669]→[2.669:736](∅→∅)
  − addzero' : {x:Poly} -> (x + [] = x)

  − addzero' = trans (h2 x) (h1 x)
  [2.669]

  [2.736]
  + addzero' : (x:Poly) -> x + [] = x

  + addzero' [] = Refl

  + addzero' (x :: xs) = h1 (x :: xs)
• replacement in Data/Polynomial.idr at line 31
  [2.751]→[2.751:928](∅→∅)
  − addcomm : {x,y:Poly} -> (x + y = y + x)

  − addcomm {x = []} = sym $ addzero'

  − addcomm {y = []} = addzero'

  − addcomm {x=(x::_), y=(y::_)} =

  − eqList (plusCommutative x y) (addcomm)
  [2.751]

  [2.928]
  + addcomm : (x,y:Poly) -> x + y = y + x

  + addcomm [] y = sym $ addzero' y

  + addcomm x [] = addzero' x

  + addcomm (x::xs) (y::ys) =

  + rewrite plusCommutative x y in

  + rewrite addcomm xs ys in Refl
• replacement in Data/Polynomial.idr at line 39
  [2.943]→[2.943:1233](∅→∅)
  − addassoc : {x,y,z:Poly} -> ((x + y) + z = x + (y + z))

  − addassoc {x = []} = Refl

  − addassoc {y = []} = rewrite addzero' in Refl

  − addassoc {z = []} = trans (addzero') $ cong (x + ) (sym $ addzero')

  − addassoc {x=(x::_), y=(y::_), z=(z::_)} =

  − eqList (sym $ (plusAssociative x y z)) $ addassoc
  [2.943]

  [2.1233]
  + addassoc : (x,y,z:Poly) -> (x + y) + z = x + (y + z)

  + addassoc [] y z = Refl

  + addassoc x [] z = rewrite addzero' x in Refl

  + addassoc x y [] = rewrite addzero' (x+y) in rewrite addzero' y in Refl

  + addassoc (x::xs) (y::ys) (z::zs) =

  + rewrite plusAssociative x y z in

  + rewrite addassoc xs ys zs in

  + Refl
• replacement in Data/Polynomial.idr at line 49
  [2.1248]→[2.1248:1299](∅→∅)
  − mulzero : {x:Poly} -> ([] * x = [])

  − mulzero = Refl
  [2.1248]

  [2.1299]
  + mulzero : (x:Poly) -> [] * x = []

  + mulzero x = Refl
• replacement in Data/Polynomial.idr at line 53
  [2.1314]→[2.1314:1407](∅→∅)
  − mulzero' : {x:Poly} -> (x * [] = [])

  − mulzero' {x = []} = Refl

  − mulzero' {x = (_ :: _)} = Refl
  [2.1314]

  [2.1407]
  + mulzero' : (x:Poly) -> x * [] = []

  + mulzero' [] = Refl

  + mulzero' (x :: xs) = Refl
• replacement in Data/Polynomial.idr at line 58
  [2.1422]→[2.1422:1580](∅→∅)
  − mulone : {x:Poly} -> ([1] * x = x)

  − mulone {x = []} = Refl

  − mulone {x = (x :: xs)} = eqList (plusZeroRightNeutral x) $

  − trans (cong (+ []) mulone) addzero'

  −
  [2.1422]

  [2.1580]
  + mulone : (x:Poly) -> [1] * x = x

  + mulone [] = Refl

  + mulone (x :: xs) =

  + rewrite plusZeroRightNeutral x in

  + rewrite mulone xs in

  + rewrite addzero' xs in Refl

  +
• replacement in Data/Polynomial.idr at line 66
  [2.1594]→[2.1594:1719](∅→∅)
  − mulone' : {x:Poly} -> (x * [1] = x)

  − mulone' {x = []} = Refl

  − mulone' {x = (x :: xs)} = eqList (multOneRightNeutral x) mulone'
  [2.1594]

  [2.1719]
  + mulone' : (x:Poly) -> x * [1] = x

  + mulone' [] = Refl

  + mulone' (x :: xs) =

  + rewrite multOneRightNeutral x in

  + rewrite mulone' xs in Refl
• replacement in Data/Polynomial.idr at line 72
  [2.1720]→[2.1720:1801](∅→∅)
  − eqadd : (Num ty) => {a,b,c,d:ty} -> a=c -> b=d -> a+b=c+d

  − eqadd Refl Refl = Refl
  [2.1720]

  [2.1801]
  + eqadd : (a,b,c,d:Poly) -> (a + b) + (c + d) = (a + c) + (b + d)

  + eqadd a b c d =

  + rewrite addassoc a b (c + d) in

  + rewrite addassoc a c (b + d) in

  + rewrite sym $ addassoc b c d in

  + rewrite sym $ addassoc c b d in

  + rewrite addcomm b c in Refl
• replacement in Data/Polynomial.idr at line 80
  [2.1802]→[2.1802:1993](∅→∅)
  − eqadd2 : {a,b,c,d:Poly} -> ((a+b)+(c+d) = (a+c)+(b+d))

  − eqadd2 = trans addassoc

  − $ trans (cong (a+)

  − $ trans (sym addassoc)

  − $ trans (cong (+d) addcomm) addassoc)

  − $ sym addassoc
  [2.1802]

  [2.1993]
  + public export

  + dist : (x,y,z:Poly) -> x * (y + z) = x * y + x * z

  + dist [] _ _ = Refl

  + dist x [] z = rewrite mulzero' x in Refl

  + dist x y [] =

  + rewrite mulzero' x in

  + rewrite addzero' y in

  + rewrite addzero' (x * y) in Refl

  + dist (x::xs) (y::ys) (z::zs) =

  + rewrite multDistributesOverPlusRight x y z in

  + rewrite dist xs (y::ys) (z::zs) in

  + rewrite dist [x] ys zs in

  + rewrite eqadd ([x] * ys) ([x] * zs) (xs * (y::ys)) (xs * (z::zs)) in

  + Refl
• edit in Data/Polynomial.idr at line 95
  [2.1994]

  [2.1994]
  + lemma : (x : Nat) -> (xs : List Nat) -> (y : Nat) -> (ys : List Nat) -> [x] * ys + (y :: ys) * xs = [y] * xs + (x :: xs) * ys
• replacement in Data/Polynomial.idr at line 97
  [2.2008]→[2.2008:2543](∅→∅)
  − dist : {x,y,z:Poly} -> (x*(y+z) = x*y+ x*z)

  − dist {x = []} = Refl

  − dist {y = []} = cong (+ (x * z)) $ sym $ mulzero'

  − dist {z = []} =

  − trans (cong (x * ) addzero')

  − $ trans (sym addzero')

  − $ cong (x * y + ) $ sym mulzero'

  − dist {x = [x], y = (y :: ys), z = (z :: zs)} =

  − eqList (multDistributesOverPlusRight x y z)

  − $ trans addzero' $ trans dist

  − $ sym $ eqadd addzero' addzero'

  − dist {x = (x::xs), y = (y::ys), z = (z::zs)} =

  − eqList (multDistributesOverPlusRight x y z)

  − $ trans (eqadd dist dist)

  − $ eqadd2
  [2.2008]

  [2.2543]
  + mulcomm : (x,y:Poly) -> x * y = y * x
• replacement in Data/Polynomial.idr at line 99
  [2.2544]→[2.2544:3357](∅→∅)
  − mulcomm' : (x,y:Poly) -> (x * y = y * x)

  − mulcomm' [] _ = sym mulzero'

  − mulcomm' _ [] = mulzero'

  − mulcomm' [x] (y::ys) =

  − eqList (multCommutative x y)

  − $ trans addzero' (mulcomm' [x] ys)

  − mulcomm' (x :: xx :: xs) [y] = sym $ mulcomm' [y] (x :: xx :: xs)

  − mulcomm' (x :: xx :: xs) (y :: yy :: ys) =

  − eqList (multCommutative x y)

  − $ trans (eqadd (mulcomm' [x] (yy::ys)) (mulcomm' (xx::xs) (y :: yy :: ys)))

  − $ trans (

  − eqList (trans (plusCommutative (yy * x) (y * xx))

  − $ eqadd (multCommutative y xx)

  − $ multCommutative yy x)

  − $ trans (sym addassoc)

  − $ trans (eqadd (trans addcomm $ eqadd (mulcomm' [y] xs) (mulcomm' ys [x]))

  − $ mulcomm' (yy::ys) (xx::xs))

  − $ addassoc

  − )

  − $ sym $ eqadd (mulcomm' [y] (xx::xs)) (mulcomm' (yy::ys) (x :: xx :: xs))
  [2.2544]

  [2.3357]
  + lemma x [] y ys = addzero' ([x] * ys)

  + lemma x xs y [] = sym $ addzero' ([y] * xs)

  + lemma x (xx :: xs) y (yy :: ys) =

  + rewrite mulcomm (xx::xs) (yy::ys) in

  + rewrite plusCommutative (x * yy) (y * xx) in

  + rewrite addzero' ([x] * ys) in

  + rewrite addzero' ([y] * xs) in

  + rewrite eqadd [] ([x] * ys) ([y] * xs) ((yy::ys) * (xx::xs)) in

  + Refl
• replacement in Data/Polynomial.idr at line 109
  [2.3358]→[2.3358:3442](∅→∅)
  − public export

  − mulcomm : {x,y:Poly} -> (x * y = y * x)

  − mulcomm {x, y} = mulcomm' x y
  [2.3358]
  + mulcomm [] y = sym $ mulzero' y

  + mulcomm x [] = mulzero' x

  + mulcomm (x::xs) (y::ys) =

  + rewrite mulcomm xs (y::ys) in

  + rewrite mulcomm ys (x::xs) in

  + rewrite multCommutative x y in

  + rewrite lemma x xs y ys in Refl