include "common/Values.ma".

definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
λm,n,x. \snd (split … x).

lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
qed.

lemma truncate_eq : ∀n,x. truncate 0 n x = x.
#n #x normalize >split_O_n @refl
qed.

lemma hdtl : ∀A,n. ∀x:Vector A (S n). x = (head' … x):::(tail … x).
#A #n #x
@(match x return λn.
    match n return λn.Vector A n → Prop with
    [ O ⇒ λ_.True
    | S m ⇒ λx:Vector A (S m). x = (head' A m x):::(tail A m x) ]
  with [ VEmpty ⇒ I | VCons p h t ⇒ ? ])
@refl
qed.

lemma vempty : ∀A. ∀x:Vector A O. x = [[ ]].
#A #x
@(match x return λn.
    match n return λn.Vector A n → Prop with
    [ O ⇒ λx.x = [[ ]]
    | _ ⇒ λ_.True ]
  with [ VEmpty ⇒ ? | VCons _ _ _ ⇒ I ])
@refl
qed.

lemma fold_right2_i_unfold : ∀A,B,C,n,hx,hy,f,a,x,y.
  fold_right2_i A B C f a ? (hx:::x) (hy:::y) =
  f ? hx hy (fold_right2_i A B C f a n x y).
// qed.

lemma add_with_carries_unfold : ∀n,x,y,c.
  add_with_carries n x y c = fold_right2_i ????? n x y.
// qed.

lemma add_with_carries_extend : ∀n,hx,hy,x,y,c.
  (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c
  in 〈tail ?? rs, tail ?? cs〉) = add_with_carries n x y c.
#n #hx #hy #x #y #c
>add_with_carries_unfold
> (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
<add_with_carries_unfold
cases (add_with_carries n x y c)
//
qed.

lemma tail_plus_1 : ∀n,hx,hy,x,y.
  tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y.
#n #hx #hy #x #y
whd in ⊢ (??(???%)%)
<(add_with_carries_extend n hx hy x y false)
cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
//
qed.

lemma split_eq' : ∀A,m,n,v. split A m n v = split' A m n v.
#A #m cases m
[ #n cases n
  [ #v >(vempty … v) @refl
  | #n' #v >(hdtl … v) //
  ]
| #m' #n #v >(hdtl … v) //
] qed.  

lemma split_left : ∀A,m,n,h,t.
  split A (S m) n (h:::t) = let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉.
#A #m #n #h #t normalize >split_eq' @refl
qed.

lemma truncate_head : ∀m,n,h,t.
  truncate (S m) n (h:::t) = truncate m n t.
#m #n #h #t normalize >split_eq' cases (split' bool m n t) //
qed.

lemma truncate_tail : ∀m,n,v.
  truncate (S m) n v = truncate m n (tail … v).
#m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl
  qed.

lemma truncate_add_with_carries : ∀m,n,x,y,c.
  (let 〈rs,cs〉 ≝ add_with_carries … x y c in 〈truncate m n rs, truncate m n cs〉) =
  add_with_carries … (truncate … x) (truncate … y) c.
#m elim m
[ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs
  whd in ⊢ (??%?) >truncate_eq >truncate_eq  @refl
| #m' #IH #n #x #y #c
  >(hdtl … x) >(hdtl … y)
  >truncate_head >truncate_head <IH
  <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y))
  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%)
  <truncate_tail <truncate_tail @refl
] qed.

lemma truncate_plus : ∀m,n,x,y.
  truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y).
#m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries 
cases (add_with_carries ????) //
qed.

lemma truncate_pad : ∀m,n,x.
  truncate m n (pad … x) = x.
#m0 elim m0
[ #n #x >truncate_eq //
| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
] qed.

theorem zero_plus_reduce : ∀m,n,x,y. 
  truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y.
#m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)
@truncate_plus
qed.

definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
 
lemma truncate_sign : ∀m,n,x.
  truncate m n (sign … x) = x.
#m0 elim m0
[ #n #x >truncate_eq //
| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
] qed.

theorem sign_plus_reduce : ∀m,n,x,y. 
  truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
#m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)
@truncate_plus
qed.

lemma sign_zero : ∀n,x.
  sign n O x = x.
#n #x @refl qed.

lemma sign_vcons : ∀m,n,x.
  sign m (S n) x = (sign_bit ? x):::(sign m n x).
#m #n #x @refl
qed.

lemma sign_vcons_hd : ∀m,n,h,t.
  sign (S m) (S n) (h:::t) = h:::(sign (S m) n (h:::t)).
// qed.

lemma zero_vcons : ∀m.
  zero (S m) = false:::(zero m).
// qed.

lemma zero_sign : ∀m,n.
  sign m n (zero ?) = zero ?.
#m #n elim n
[ //
| #n' #IH >sign_vcons >IH elim m //
] qed.

lemma add_with_carries_vcons : ∀n,hx,hy,x,y,c.
  add_with_carries (S n) (hx:::x) (hy:::y) c
  = (let 〈rs,cs〉 ≝ add_with_carries n x y c in 〈?:::rs, ?:::cs〉).
[ #n #hx #hy #x #y #c
  >add_with_carries_unfold
  > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
  <add_with_carries_unfold
  cases (add_with_carries n x y c)
  //
| *: skip
]
qed.

lemma sign_bitflip : ∀m,n,x.
  negation_bv ? (sign (S m) n x) = sign (S m) n (negation_bv ? x).
#m #n #x @(vector_inv_n … x) #h #t elim n
[ @refl
| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
] qed.

lemma truncate_negation_bv : ∀m,n,x.
  truncate m n (negation_bv ? x) = negation_bv ? (truncate m n x).
#m #n elim m
[ #x >truncate_eq >truncate_eq @refl
| #m' #IH #x @(vector_inv_n … x) #h #t >truncate_tail >truncate_tail
  >(IH t) @refl
] qed.

lemma truncate_zero : ∀m,n.
  truncate m n (zero ?) = zero ?.
#m #n elim m
[ >truncate_eq @refl
| #m' #IH >truncate_tail >zero_vcons <IH @refl
] qed.

lemma zero_negate_reduce : ∀m,n,x.
  truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
#m #n #x whd in ⊢ (??(???%)%)
lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
#rs #cs whd in ⊢ (??%? → ??(???%)?)
>truncate_negation_bv
>truncate_pad >truncate_zero cases (add_with_carries ????)
#rs' #cs' #E destruct //
qed.

lemma sign_negate_reduce : ∀m,n,x.
  truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
#m #n #x whd in ⊢ (??(???%)%)
>sign_bitflip <(zero_sign (S n) m)
lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
#rs #cs whd in ⊢ (??%? → ??(???%)?)
>truncate_sign >truncate_sign cases (add_with_carries ????)
#rs' #cs' #E destruct //
qed.

theorem zero_subtract_reduce : ∀m,n,x,y.
  truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
#m #n #x #y
whd in ⊢ (??(???%)%)
lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
#rs #cs whd in ⊢ (??%? → ??(???%)?)
>zero_negate_reduce >truncate_pad
cases (add_with_carries ????)
#rs' #cs' #E destruct @refl
qed.

theorem sign_subtract_reduce : ∀m,n,x,y.
  truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
#m #n #x #y
whd in ⊢ (??(???%)%)
lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
#rs #cs whd in ⊢ (??%? → ??(???%)?)
>sign_negate_reduce >truncate_sign
cases (add_with_carries ????)
#rs' #cs' #E destruct @refl
qed.