Changeset 2468 for src/Clight/frontend_misc.ma

Timestamp:

Nov 15, 2012, 6:12:57 PM (8 years ago)

Author:

garnier

Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:

• src/Clight/frontend_misc.ma (modified) (2 diffs)

src/Clight/frontend_misc.ma

@@ -10 +10 @@
 include "basics/lists/listb.ma".
 include "basics/lists/list.ma".
+
+
+(* --------------------------------------------------------------------------- *)
+(* [cthulhu] plays the same role as daemon. It should be droppable. *)
+(* --------------------------------------------------------------------------- *)
+
+axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
 
 (* --------------------------------------------------------------------------- *)
@@ -1647 +1654 @@
 | 3,4: @reflexive_lset_inclusion ]
 qed.
+
+(* --------------------------------------------------------------------------- *)
+(* Stuff on bitvectors, previously in memoryInjections.ma *)
+(* --------------------------------------------------------------------------- *)
+(* --------------------------------------------------------------------------- *)   
+(* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)
+(* --------------------------------------------------------------------------- *) 
+  
+lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.
+#n #bv whd in match (add_with_carries ????); elim bv //
+#n #hd #tl #Hind whd in match (fold_right2_i ????????);
+>Hind normalize
+cases n in tl;
+[ 1: #tl cases hd normalize @refl
+| 2: #n' #tl cases hd normalize @refl ]
+qed.
+
+lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.
+#n #bv whd in match (addition_n ???);
+>add_with_carries_n_O //
+qed.
+
+lemma replicate_Sn : ∀A,sz,elt. 
+  replicate A (S sz) elt = elt ::: (replicate A sz elt).
+// qed.
+
+lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
+
+lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
+#n #xa #a normalize @refl qed.
+
+(* useful facts on carry_of *)
+lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
+lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
+lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
+lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
+lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
+
+
+
+definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
+
+lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n). 
+    add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
+    add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
+#n elim n
+[ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits 
+     elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
+     >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
+     normalize #Heq destruct (Heq) @refl
+| 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
+     destruct #Hind >add_with_carries_Sn >replicate_Sn
+     whd in match (zero ?) in Hind; lapply Hind
+     elim (add_with_carries (S (S n')) 
+            (false:::replicate bool (S n') false)
+            (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
+            normalize >add_with_carries_Sn in Hind;
+     elim (add_with_carries (S n') (replicate bool (S n') false)
+                    (replicate bool (S n') false) true) #flags' #bits'
+     normalize
+     cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
+            [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
+     normalize #Heq destruct @refl
+] qed.     
+
+lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
+#n lapply (one_bv_Sn_aux n)
+whd in match (one_bv ?) in ⊢ (? → (??%%));
+elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
+#H lapply (H bits flags (refl ??)) #H2 >H2 @refl
+qed.
+
+lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n. 
+    add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
+#n    
+elim n
+[ 1: #a >(BitVector_O … a) normalize @refl
+| 2: #n' cases n'
+     [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
+          >(BitVector_O … tl) normalize cases xa @refl
+     | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
+          >one_bv_Sn >zero_Sn
+          lapply (Hind tl)
+          >add_with_carries_Sn >add_with_carries_Sn
+          #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
+          normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
+          normalize nodelta @refl
+] qed.          
+
+(* In order to use associativity on increment, we hide it under addition_n. *)
+lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
+#n
+whd in match (increment ??) in ⊢ (∀_.??%?);
+whd in match (addition_n ???) in ⊢ (∀_.???%);
+#a lapply (increment_to_addition_n_aux n a)
+#Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
+qed.
+
+(* Explicit formulation of addition *)
+
+(* Explicit formulation of the last carry bit *)
+let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
+match n return λx. BitVector x → BitVector x → bool with
+[ O ⇒ λ_,_. init
+| S x ⇒ λa',b'.
+  let hd_a ≝ head' … a' in
+  let hd_b ≝ head' … b' in
+  let tl_a ≝ tail … a' in
+  let tl_b ≝ tail … b' in
+  carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
+] a b.
+
+lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n). 
+  ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
+#n #init #a #b @refl qed.
+
+lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n. 
+  ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
+
+(* correction of [ith_carry] *)
+lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
+  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
+  head' … flags_ab = ith_carry ? a b init.
+#n elim n
+[ 1: #init #a #b #res_ab #flags_ab
+     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
+     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
+     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
+     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
+     destruct
+     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
+     cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
+     @refl
+| 2: #n' #Hind #init #a #b #res_ab #flags_ab
+     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
+     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
+     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
+     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
+     destruct
+     lapply (Hind … init tl_a tl_b tl_res tl_flags)
+     >add_with_carries_Sn >(ith_carry_Sn (S n'))
+     elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
+     elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
+     normalize nodelta cases hd_flags_ab normalize nodelta
+     whd in match (head' ? (S n') ?); #H1 #H2
+     destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
+] qed.
+
+(* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
+definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
+match n return λx. BitVector x → BitVector x → bool with
+[ O ⇒ λ_,_. init
+| S x ⇒ λa',b'.
+  let hd_a ≝ head' … a' in
+  let hd_b ≝ head' … b' in
+  let tl_a ≝ tail … a' in
+  let tl_b ≝ tail … b' in
+  xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
+] a b.
+
+lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n). 
+  ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
+#n #a #b // qed.
+
+lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n. 
+  ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
+
+(* correction of ith_bit *)
+lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
+  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
+  head' … res_ab = ith_bit ? a b init.
+#n
+cases n
+[ 1: #init #a #b #res_ab #flags_ab
+     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
+     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
+     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
+     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
+     destruct
+     >(BitVector_O … tl_a) >(BitVector_O … tl_b) 
+     >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
+     normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
+| 2: #n' #init #a #b #res_ab #flags_ab
+     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
+     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
+     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
+     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
+     destruct
+     lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
+     #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
+     #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
+     >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
+     cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
+     <(H1 (refl ??)) @refl
+] qed.
+
+(* Transform a function from bit-vectors to bits into a vector by folding *)
+let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
+match v with
+[ VEmpty ⇒ VEmpty ?
+| VCons sz elt tl ⇒
+  let bit ≝ f ? v in
+  bit ::: (bitvector_fold ? tl f)
+].
+
+(* Two-arguments version *)
+let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
+match v1  with
+[ VEmpty ⇒ λ_. VEmpty ?
+| VCons sz elt tl ⇒ λv2'.
+  let bit ≝ f ? v1 v2 in
+  bit ::: (bitvector_fold2 ? tl (tail … v2') f)
+] v2.
+
+lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f. 
+  bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
+
+(* These functions pack all the relevant information (including carries) directly. *)
+definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
+
+lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init. 
+  addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
+  
+lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
+
+(* Prove the equivalence of addition_n_direct with add_with_carries *) 
+lemma addition_n_direct_ok : ∀n,carry,v1,v2.
+  (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
+#n elim n
+[ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
+| 2: #n' #Hind #carry #v1 #v2
+     elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
+     elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
+     lapply (Hind carry tl1 tl2)
+     lapply (ith_bit_ok ? carry v1 v2)
+     lapply (ith_carry_ok ? carry v1 v2)
+     destruct
+     #Hind >addition_n_direct_Sn
+     >ith_bit_Sn >add_with_carries_Sn
+     elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
+     cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
+            [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
+     normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
+     whd in match head'; normalize nodelta
+     #H1 #H2 >H1 >H2 @refl
+] qed.
+
+lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.
+  (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.
+#n #carry #v1 #v2 <addition_n_direct_ok
+cases (add_with_carries ????) //
+qed.
+  
+(* trivially lift associativity to our new setting *)     
+lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
+  addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
+  addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
+#n #carry1 #carry2 #v1 #v2 #v3
+<addition_n_direct_ok <addition_n_direct_ok
+<addition_n_direct_ok <addition_n_direct_ok
+lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
+elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
+elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
+#H @(sym_eq … H)
+qed.
+
+lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
+  addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
+#n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
+qed.
+
+definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
+definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
+
+
+(* fold andb on a bitvector. *)
+let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
+match b with
+[ VEmpty ⇒ true
+| VCons sz elt tl ⇒ 
+  andb elt (andb_fold ? tl)
+].
+
+lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
+
+lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
+#n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
+qed.
+
+lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
+  ith_carry … a (one_bv ?) false = andb_fold … a.
+#n elim n
+[ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
+     cases hd normalize @refl
+| 2: #n' #Hind #a
+     elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
+     lapply (Hind … tl) #Hind >one_bv_Sn
+     >ith_carry_Sn whd in match (andb_fold ??);
+     cases hd >Hind @refl
+] qed.
+
+lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
+  ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
+#n #a
+elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
+whd in match (head' ???);
+-a cases n in tl;
+[ 1: #tl >(BitVector_O … tl) cases hd normalize try //
+| 2: #n' #tl >one_bv_Sn >ith_bit_Sn
+     >ith_increment_carry >tail_Sn
+     cases hd try //
+] qed.
+
+(* Lemma used to prove involutivity of two-complement negation *)
+lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
+   (andb_fold (S n) (negation_bv (S n) v) = 
+    andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
+#n elim n
+[ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
+| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
+     lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
+     >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
+     cases hd normalize nodelta
+     [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
+     | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
+     >ith_increment_carry
+     cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
+] qed.
+   
+(* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
+lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
+#n elim n
+[ 1: #v >(BitVector_O v) @refl
+| 2: #n' cases n'
+     [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
+          >(BitVector_O … tl) normalize cases hd @refl
+     | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
+          lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
+          whd in match twocomp_neg_direct; normalize nodelta
+          whd in match increment_direct; normalize nodelta
+          >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
+          >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
+          generalize in match (addition_n_direct (S n'')
+                                                   (negation_bv (S n'')
+                                                   (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
+                                                   (one_bv (S n'')) false); #tail
+          >ith_increment_carry >ith_increment_carry
+          cases hd normalize nodelta 
+          [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
+          | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
+          <twocomp_neg_involutive_aux
+          cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
+      ]
+] qed.
+
+lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
+#n #a #b #va #vb #H destruct (H) @conj @refl qed.
+
+lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
+
+(* Injectivity of increment *)
+lemma increment_inj : ∀n. ∀a,b : BitVector n. 
+  increment_direct ? a = increment_direct ? b →
+  a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
+#n whd in match increment_direct; normalize nodelta elim n
+[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
+| 2: #n' cases n'
+   [ 1: #_ #a #b
+        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
+        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
+        >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
+        normalize #H @conj try //
+   | 2: #n'' #Hind #a #b
+        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
+        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
+        lapply (Hind … tl_a tl_b) -Hind #Hind
+        >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
+        >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
+        #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
+        lapply (Hind Heq2) * #Heq3 #Heq4
+        cut (hd_a = hd_b)
+        [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
+             * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
+             @refl ]
+        #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
+        >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
+] qed.
+
+(* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
+lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
+  a = b → increment_direct ? a = increment_direct ? b. // qed.
+
+(* A more general result. *)
+lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.
+  addition_n_direct ? x delta false = addition_n_direct ? y delta false →
+  x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).
+#n elim n
+[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl
+| 2: #n' #Hind #x #y #delta
+     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
+     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
+     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
+     >addition_n_direct_Sn >ith_bit_Sn
+     >addition_n_direct_Sn >ith_bit_Sn
+     >ith_carry_Sn >ith_carry_Sn
+     lapply (Hind … tlx tly tld) -Hind #Hind #Heq
+     elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl
+     lapply (Hind Heq_tl) -Hind * #HindA #HindB
+     >HindA >HindB >HindB in Heq_hd; #Heq_hd
+     cut (hdx = hdy)
+     [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)
+          cases hdx cases hdy normalize #H try @H try @refl
+          >H try @refl ]
+     #Heq_hd >Heq_hd @conj @refl
+] qed.
+
+(* We also need it the other way around. *)
+lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.
+  x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)
+   addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.
+#n elim n
+[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))
+| 2: #n' #Hind #x #y #delta
+     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
+     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
+     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
+     #Hneq
+     cut (hdx ≠ hdy ∨ tlx ≠ tly)
+     [ @(eq_bv_elim … tlx tly)
+       [ #Heq_tl >Heq_tl >Heq_tl in Hneq;
+         #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *
+                                 #H @H @refl ]
+         #H %1 @H
+       | #H %2 @H ] ]
+     -Hneq #Hneq
+     >addition_n_direct_Sn >addition_n_direct_Sn
+     >ith_bit_Sn >ith_bit_Sn cases Hneq
+     [ 1: #Hneq_hd
+          lapply (addition_n_direct_inj … tlx tly tld)          
+          @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))
+          [ 1: #Heq -Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry
+               % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) -Habsurd
+               lapply Hneq_hd
+               cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)
+               normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_
+               try @(absurd … Heq_hd Hneq_hd)
+               elim Hneq_hd -Hneq_hd #Hneq_hd @Hneq_hd
+               try @refl try assumption try @(sym_eq … Heq_hd)
+          | 2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
+               elim Htl_not_eq -Htl_not_eq #HA #HB @HA @HB ]
+     | 2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) -Hind #Hind
+          % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
+          elim Hind -Hind #HA #HB @HA @HB ]
+] qed.
+
+lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
+
+lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
+   ith_carry (S n) a (one_bv (S n)) false
+   = ith_carry (S n) a (zero (S n)) true.
+#n elim n
+[ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
+| 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
+     lapply (Hind tl_a) #Hind
+     >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
+] qed.
+
+lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
+#n elim n //
+#n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
+>ith_carry_Sn >(Hind tl) cases hd @refl.
+qed.
+
+lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
+  addition_n_direct ? v (zero ?) false = v.
+#n elim n
+[ 1: #v >(BitVector_O … v) normalize @refl
+| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
+     lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
+     >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
+     >xorb_false @refl
+] qed.
+
+lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
+#n elim n
+[ 1: #a >(BitVector_O … a) normalize @refl
+| 2: #n' cases n'
+     [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
+     | 2: #n'' #Hind #a
+          elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
+          lapply (Hind tl_a) -Hind #Hind
+          >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
+          >addition_n_direct_Sn >ith_bit_Sn
+          >xorb_false >Hind @bitvector_cons_eq
+          >increment_to_carry_aux @refl
+     ]
+] qed.
+
+lemma increment_to_carry : ∀n. ∀a,b : BitVector n. 
+  addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
+#n #a #b >increment_to_carry_zero <associative_addition_n_direct
+>neutral_addition_n_direct @refl
+qed.
+
+lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.
+#n #v whd in match (increment ??);
+>addition_n_direct_ok <increment_to_carry_zero @refl
+qed. 
+
+(* Prove -(a + b) = -a + -b *)
+lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n. 
+  twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
+whd in match twocomp_neg_direct; normalize nodelta
+lapply increment_inj_inv
+whd in match increment_direct; normalize nodelta
+#H #n #a #b
+<associative_addition_n_direct @H
+>associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
+>increment_to_carry
+-H lapply b lapply a -b -a 
+cases n
+[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
+| 2: #n' #a #b
+     cut (negation_bv ? (addition_n_direct ? a b false)
+           = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
+          notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
+     [ -n lapply b lapply a elim n'
+     [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
+          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
+          cases hd_a cases hd_b normalize @conj @refl
+     | 2: #n #Hind #a #b
+          elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
+          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
+          lapply (Hind tl_a tl_b) * #H1 #H2
+          @conj
+          [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
+               >carry_notb >H2 @refl
+          | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
+               >negation_bv_Sn >negation_bv_Sn 
+               >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
+               >xorb_lneg >xorb_rneg >notb_notb
+               <xorb_rneg >H2 @refl
+          ] 
+      ] ]
+      * #H1 #H2 @H1
+] qed.
+
+lemma addition_n_direct_neg : ∀n. ∀a.
+ (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
+ ∧ (ith_carry n a (negation_bv n a) false = false).
+#n elim n
+[ 1: #a >(BitVector_O … a) @conj @refl
+| 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
+     lapply (Hind … tl) -Hind * #HA #HB
+     @conj
+     [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
+     | 1: >negation_bv_Sn >addition_n_direct_Sn
+          >ith_bit_Sn >HB >xorb_false >HA
+          @bitvector_cons_eq elim hd @refl
+     ]
+] qed.
+
+(* -a + a = 0 *)
+lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
+whd in match twocomp_neg_direct;
+whd in match increment_direct;
+normalize nodelta
+#n #a <associative_addition_n_direct
+elim (addition_n_direct_neg … a) #H #_ >H
+-H -a
+cases n try //
+#n'
+cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
+       ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
+[ elim n'
+     [ 1: @conj @refl
+     | 2: #n' * #HA #HB @conj
+          [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
+               >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
+          | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
+     ]
+] * #H1 #H2 @H1
+qed.
+
+(* Lift back the previous result to standard operations. *)
+lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
+#n #v whd in match twocomp_neg_direct; normalize nodelta
+whd in match increment_direct; normalize nodelta
+whd in match two_complement_negation; normalize nodelta
+>increment_to_addition_n <addition_n_direct_ok
+whd in match addition_n; normalize nodelta
+elim (add_with_carries ????) #a #b @refl
+qed.
+
+lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
+  two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
+#n #a #b
+lapply (twocomp_neg_plus ? a b)
+>twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
+<addition_n_direct_ok <addition_n_direct_ok
+whd in match addition_n; normalize nodelta
+elim (add_with_carries n a b false) #bits #flags normalize nodelta
+elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
+normalize nodelta #H @H
+qed.
+
+lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
+#n #a lapply (bitvector_opp_direct ? a)
+>twocomp_neg_direct_ok <addition_n_direct_ok
+whd in match (addition_n ???);
+elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
+qed.
+
+lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
+#n #a 
+lapply (neutral_addition_n_direct n a)
+<addition_n_direct_ok
+whd in match (addition_n ???);
+elim (add_with_carries n a (zero n) false) #bits #flags #H @H
+qed.
+
+lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.
+  addition_n ? x delta = addition_n ? y delta → x = y.  
+#n #x #y #delta  
+lapply (addition_n_direct_inj … x y delta)
+<addition_n_direct_ok <addition_n_direct_ok
+whd in match addition_n; normalize nodelta
+elim (add_with_carries n x delta false) #bitsx #flagsx
+elim (add_with_carries n y delta false) #bitsy #flagsy
+normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq
+qed.
+
+lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.
+  x ≠ y → addition_n ? x delta ≠ addition_n ? y delta.  
+#n #x #y #delta  
+lapply (addition_n_direct_inj_inv … x y delta)
+<addition_n_direct_ok <addition_n_direct_ok
+whd in match addition_n; normalize nodelta
+elim (add_with_carries n x delta false) #bitsx #flagsx
+elim (add_with_carries n y delta false) #bitsy #flagsy
+normalize #H1 #H2 @(H1 H2)
+qed.
+