include "common/Values.ma". definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝ λm,n,x. \snd (vsplit … x). lemma vsplit_O_n : ∀A,n,x. vsplit 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 >vsplit_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. (* add_with_carries was changed to make it whd nicely in some places, but we want to undo that for some lemmas. *) lemma bool_eta : ∀A:Type[0].∀b. ∀P:bool → A. if b then P true else P false = P b. #A * // 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) bool_eta // 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 vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' 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 vsplit_left : ∀A,m,n,h,t. vsplit A (S m) n (h:::t) = (let 〈l,r〉 ≝ vsplit A m n t in 〈h:::l,r〉). #A #m #n #h #t normalize >vsplit_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 >vsplit_eq' cases (vsplit' 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 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) bool_eta // | *: 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 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.