Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2448 r2468  
    1010include "basics/lists/listb.ma".
    1111include "basics/lists/list.ma".
     12
     13
     14(* --------------------------------------------------------------------------- *)
     15(* [cthulhu] plays the same role as daemon. It should be droppable. *)
     16(* --------------------------------------------------------------------------- *)
     17
     18axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
    1219
    1320(* --------------------------------------------------------------------------- *)
     
    16471654| 3,4: @reflexive_lset_inclusion ]
    16481655qed.
     1656
     1657(* --------------------------------------------------------------------------- *)
     1658(* Stuff on bitvectors, previously in memoryInjections.ma *)
     1659(* --------------------------------------------------------------------------- *)
     1660(* --------------------------------------------------------------------------- *)   
     1661(* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)
     1662(* --------------------------------------------------------------------------- *)
     1663 
     1664lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.
     1665#n #bv whd in match (add_with_carries ????); elim bv //
     1666#n #hd #tl #Hind whd in match (fold_right2_i ????????);
     1667>Hind normalize
     1668cases n in tl;
     1669[ 1: #tl cases hd normalize @refl
     1670| 2: #n' #tl cases hd normalize @refl ]
     1671qed.
     1672
     1673lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.
     1674#n #bv whd in match (addition_n ???);
     1675>add_with_carries_n_O //
     1676qed.
     1677
     1678lemma replicate_Sn : ∀A,sz,elt.
     1679  replicate A (S sz) elt = elt ::: (replicate A sz elt).
     1680// qed.
     1681
     1682lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
     1683
     1684lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
     1685#n #xa #a normalize @refl qed.
     1686
     1687(* useful facts on carry_of *)
     1688lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
     1689lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
     1690lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
     1691lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
     1692lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
     1693
     1694
     1695
     1696definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
     1697
     1698lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).
     1699    add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
     1700    add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
     1701#n elim n
     1702[ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
     1703     elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
     1704     >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
     1705     normalize #Heq destruct (Heq) @refl
     1706| 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
     1707     destruct #Hind >add_with_carries_Sn >replicate_Sn
     1708     whd in match (zero ?) in Hind; lapply Hind
     1709     elim (add_with_carries (S (S n'))
     1710            (false:::replicate bool (S n') false)
     1711            (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
     1712            normalize >add_with_carries_Sn in Hind;
     1713     elim (add_with_carries (S n') (replicate bool (S n') false)
     1714                    (replicate bool (S n') false) true) #flags' #bits'
     1715     normalize
     1716     cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
     1717            [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
     1718     normalize #Heq destruct @refl
     1719] qed.     
     1720
     1721lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
     1722#n lapply (one_bv_Sn_aux n)
     1723whd in match (one_bv ?) in ⊢ (? → (??%%));
     1724elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
     1725#H lapply (H bits flags (refl ??)) #H2 >H2 @refl
     1726qed.
     1727
     1728lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.
     1729    add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
     1730#n   
     1731elim n
     1732[ 1: #a >(BitVector_O … a) normalize @refl
     1733| 2: #n' cases n'
     1734     [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
     1735          >(BitVector_O … tl) normalize cases xa @refl
     1736     | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
     1737          >one_bv_Sn >zero_Sn
     1738          lapply (Hind tl)
     1739          >add_with_carries_Sn >add_with_carries_Sn
     1740          #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
     1741          normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
     1742          normalize nodelta @refl
     1743] qed.         
     1744
     1745(* In order to use associativity on increment, we hide it under addition_n. *)
     1746lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
     1747#n
     1748whd in match (increment ??) in ⊢ (∀_.??%?);
     1749whd in match (addition_n ???) in ⊢ (∀_.???%);
     1750#a lapply (increment_to_addition_n_aux n a)
     1751#Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
     1752qed.
     1753
     1754(* Explicit formulation of addition *)
     1755
     1756(* Explicit formulation of the last carry bit *)
     1757let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
     1758match n return λx. BitVector x → BitVector x → bool with
     1759[ O ⇒ λ_,_. init
     1760| S x ⇒ λa',b'.
     1761  let hd_a ≝ head' … a' in
     1762  let hd_b ≝ head' … b' in
     1763  let tl_a ≝ tail … a' in
     1764  let tl_b ≝ tail … b' in
     1765  carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
     1766] a b.
     1767
     1768lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
     1769  ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
     1770#n #init #a #b @refl qed.
     1771
     1772lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
     1773  ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
     1774
     1775(* correction of [ith_carry] *)
     1776lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
     1777  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
     1778  head' … flags_ab = ith_carry ? a b init.
     1779#n elim n
     1780[ 1: #init #a #b #res_ab #flags_ab
     1781     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     1782     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     1783     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     1784     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     1785     destruct
     1786     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
     1787     cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
     1788     @refl
     1789| 2: #n' #Hind #init #a #b #res_ab #flags_ab
     1790     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     1791     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     1792     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     1793     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     1794     destruct
     1795     lapply (Hind … init tl_a tl_b tl_res tl_flags)
     1796     >add_with_carries_Sn >(ith_carry_Sn (S n'))
     1797     elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
     1798     elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
     1799     normalize nodelta cases hd_flags_ab normalize nodelta
     1800     whd in match (head' ? (S n') ?); #H1 #H2
     1801     destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
     1802] qed.
     1803
     1804(* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
     1805definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
     1806match n return λx. BitVector x → BitVector x → bool with
     1807[ O ⇒ λ_,_. init
     1808| S x ⇒ λa',b'.
     1809  let hd_a ≝ head' … a' in
     1810  let hd_b ≝ head' … b' in
     1811  let tl_a ≝ tail … a' in
     1812  let tl_b ≝ tail … b' in
     1813  xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
     1814] a b.
     1815
     1816lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
     1817  ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
     1818#n #a #b // qed.
     1819
     1820lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
     1821  ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
     1822
     1823(* correction of ith_bit *)
     1824lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
     1825  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
     1826  head' … res_ab = ith_bit ? a b init.
     1827#n
     1828cases n
     1829[ 1: #init #a #b #res_ab #flags_ab
     1830     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     1831     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     1832     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     1833     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     1834     destruct
     1835     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
     1836     >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
     1837     normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
     1838| 2: #n' #init #a #b #res_ab #flags_ab
     1839     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     1840     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     1841     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     1842     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     1843     destruct
     1844     lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
     1845     #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
     1846     #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
     1847     >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
     1848     cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
     1849     <(H1 (refl ??)) @refl
     1850] qed.
     1851
     1852(* Transform a function from bit-vectors to bits into a vector by folding *)
     1853let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
     1854match v with
     1855[ VEmpty ⇒ VEmpty ?
     1856| VCons sz elt tl ⇒
     1857  let bit ≝ f ? v in
     1858  bit ::: (bitvector_fold ? tl f)
     1859].
     1860
     1861(* Two-arguments version *)
     1862let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
     1863match v1  with
     1864[ VEmpty ⇒ λ_. VEmpty ?
     1865| VCons sz elt tl ⇒ λv2'.
     1866  let bit ≝ f ? v1 v2 in
     1867  bit ::: (bitvector_fold2 ? tl (tail … v2') f)
     1868] v2.
     1869
     1870lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.
     1871  bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
     1872
     1873(* These functions pack all the relevant information (including carries) directly. *)
     1874definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
     1875
     1876lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.
     1877  addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
     1878 
     1879lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
     1880
     1881(* Prove the equivalence of addition_n_direct with add_with_carries *)
     1882lemma addition_n_direct_ok : ∀n,carry,v1,v2.
     1883  (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
     1884#n elim n
     1885[ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
     1886| 2: #n' #Hind #carry #v1 #v2
     1887     elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
     1888     elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
     1889     lapply (Hind carry tl1 tl2)
     1890     lapply (ith_bit_ok ? carry v1 v2)
     1891     lapply (ith_carry_ok ? carry v1 v2)
     1892     destruct
     1893     #Hind >addition_n_direct_Sn
     1894     >ith_bit_Sn >add_with_carries_Sn
     1895     elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
     1896     cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
     1897            [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
     1898     normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
     1899     whd in match head'; normalize nodelta
     1900     #H1 #H2 >H1 >H2 @refl
     1901] qed.
     1902
     1903lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.
     1904  (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.
     1905#n #carry #v1 #v2 <addition_n_direct_ok
     1906cases (add_with_carries ????) //
     1907qed.
     1908 
     1909(* trivially lift associativity to our new setting *)     
     1910lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
     1911  addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
     1912  addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
     1913#n #carry1 #carry2 #v1 #v2 #v3
     1914<addition_n_direct_ok <addition_n_direct_ok
     1915<addition_n_direct_ok <addition_n_direct_ok
     1916lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
     1917elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
     1918elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
     1919#H @(sym_eq … H)
     1920qed.
     1921
     1922lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
     1923  addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
     1924#n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
     1925qed.
     1926
     1927definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
     1928definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
     1929
     1930
     1931(* fold andb on a bitvector. *)
     1932let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
     1933match b with
     1934[ VEmpty ⇒ true
     1935| VCons sz elt tl ⇒
     1936  andb elt (andb_fold ? tl)
     1937].
     1938
     1939lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
     1940
     1941lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
     1942#n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
     1943qed.
     1944
     1945lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
     1946  ith_carry … a (one_bv ?) false = andb_fold … a.
     1947#n elim n
     1948[ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
     1949     cases hd normalize @refl
     1950| 2: #n' #Hind #a
     1951     elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
     1952     lapply (Hind … tl) #Hind >one_bv_Sn
     1953     >ith_carry_Sn whd in match (andb_fold ??);
     1954     cases hd >Hind @refl
     1955] qed.
     1956
     1957lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
     1958  ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
     1959#n #a
     1960elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
     1961whd in match (head' ???);
     1962-a cases n in tl;
     1963[ 1: #tl >(BitVector_O … tl) cases hd normalize try //
     1964| 2: #n' #tl >one_bv_Sn >ith_bit_Sn
     1965     >ith_increment_carry >tail_Sn
     1966     cases hd try //
     1967] qed.
     1968
     1969(* Lemma used to prove involutivity of two-complement negation *)
     1970lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
     1971   (andb_fold (S n) (negation_bv (S n) v) =
     1972    andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
     1973#n elim n
     1974[ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
     1975| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     1976     lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
     1977     >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
     1978     cases hd normalize nodelta
     1979     [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
     1980     | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
     1981     >ith_increment_carry
     1982     cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
     1983] qed.
     1984   
     1985(* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
     1986lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
     1987#n elim n
     1988[ 1: #v >(BitVector_O v) @refl
     1989| 2: #n' cases n'
     1990     [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     1991          >(BitVector_O … tl) normalize cases hd @refl
     1992     | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     1993          lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
     1994          whd in match twocomp_neg_direct; normalize nodelta
     1995          whd in match increment_direct; normalize nodelta
     1996          >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
     1997          >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
     1998          generalize in match (addition_n_direct (S n'')
     1999                                                   (negation_bv (S n'')
     2000                                                   (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
     2001                                                   (one_bv (S n'')) false); #tail
     2002          >ith_increment_carry >ith_increment_carry
     2003          cases hd normalize nodelta
     2004          [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
     2005          | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
     2006          <twocomp_neg_involutive_aux
     2007          cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
     2008      ]
     2009] qed.
     2010
     2011lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
     2012#n #a #b #va #vb #H destruct (H) @conj @refl qed.
     2013
     2014lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
     2015
     2016(* Injectivity of increment *)
     2017lemma increment_inj : ∀n. ∀a,b : BitVector n.
     2018  increment_direct ? a = increment_direct ? b →
     2019  a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
     2020#n whd in match increment_direct; normalize nodelta elim n
     2021[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
     2022| 2: #n' cases n'
     2023   [ 1: #_ #a #b
     2024        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
     2025        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
     2026        >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
     2027        normalize #H @conj try //
     2028   | 2: #n'' #Hind #a #b
     2029        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
     2030        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
     2031        lapply (Hind … tl_a tl_b) -Hind #Hind
     2032        >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
     2033        >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
     2034        #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
     2035        lapply (Hind Heq2) * #Heq3 #Heq4
     2036        cut (hd_a = hd_b)
     2037        [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
     2038             * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
     2039             @refl ]
     2040        #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
     2041        >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
     2042] qed.
     2043
     2044(* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
     2045lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
     2046  a = b → increment_direct ? a = increment_direct ? b. // qed.
     2047
     2048(* A more general result. *)
     2049lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.
     2050  addition_n_direct ? x delta false = addition_n_direct ? y delta false →
     2051  x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).
     2052#n elim n
     2053[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl
     2054| 2: #n' #Hind #x #y #delta
     2055     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
     2056     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
     2057     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
     2058     >addition_n_direct_Sn >ith_bit_Sn
     2059     >addition_n_direct_Sn >ith_bit_Sn
     2060     >ith_carry_Sn >ith_carry_Sn
     2061     lapply (Hind … tlx tly tld) -Hind #Hind #Heq
     2062     elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl
     2063     lapply (Hind Heq_tl) -Hind * #HindA #HindB
     2064     >HindA >HindB >HindB in Heq_hd; #Heq_hd
     2065     cut (hdx = hdy)
     2066     [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)
     2067          cases hdx cases hdy normalize #H try @H try @refl
     2068          >H try @refl ]
     2069     #Heq_hd >Heq_hd @conj @refl
     2070] qed.
     2071
     2072(* We also need it the other way around. *)
     2073lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.
     2074  x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)
     2075   addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.
     2076#n elim n
     2077[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))
     2078| 2: #n' #Hind #x #y #delta
     2079     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
     2080     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
     2081     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
     2082     #Hneq
     2083     cut (hdx ≠ hdy ∨ tlx ≠ tly)
     2084     [ @(eq_bv_elim … tlx tly)
     2085       [ #Heq_tl >Heq_tl >Heq_tl in Hneq;
     2086         #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *
     2087                                 #H @H @refl ]
     2088         #H %1 @H
     2089       | #H %2 @H ] ]
     2090     -Hneq #Hneq
     2091     >addition_n_direct_Sn >addition_n_direct_Sn
     2092     >ith_bit_Sn >ith_bit_Sn cases Hneq
     2093     [ 1: #Hneq_hd
     2094          lapply (addition_n_direct_inj … tlx tly tld)         
     2095          @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))
     2096          [ 1: #Heq -Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry
     2097               % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) -Habsurd
     2098               lapply Hneq_hd
     2099               cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)
     2100               normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_
     2101               try @(absurd … Heq_hd Hneq_hd)
     2102               elim Hneq_hd -Hneq_hd #Hneq_hd @Hneq_hd
     2103               try @refl try assumption try @(sym_eq … Heq_hd)
     2104          | 2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
     2105               elim Htl_not_eq -Htl_not_eq #HA #HB @HA @HB ]
     2106     | 2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) -Hind #Hind
     2107          % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
     2108          elim Hind -Hind #HA #HB @HA @HB ]
     2109] qed.
     2110
     2111lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
     2112
     2113lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
     2114   ith_carry (S n) a (one_bv (S n)) false
     2115   = ith_carry (S n) a (zero (S n)) true.
     2116#n elim n
     2117[ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
     2118| 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
     2119     lapply (Hind tl_a) #Hind
     2120     >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
     2121] qed.
     2122
     2123lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
     2124#n elim n //
     2125#n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
     2126>ith_carry_Sn >(Hind tl) cases hd @refl.
     2127qed.
     2128
     2129lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
     2130  addition_n_direct ? v (zero ?) false = v.
     2131#n elim n
     2132[ 1: #v >(BitVector_O … v) normalize @refl
     2133| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     2134     lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
     2135     >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
     2136     >xorb_false @refl
     2137] qed.
     2138
     2139lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
     2140#n elim n
     2141[ 1: #a >(BitVector_O … a) normalize @refl
     2142| 2: #n' cases n'
     2143     [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
     2144     | 2: #n'' #Hind #a
     2145          elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
     2146          lapply (Hind tl_a) -Hind #Hind
     2147          >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
     2148          >addition_n_direct_Sn >ith_bit_Sn
     2149          >xorb_false >Hind @bitvector_cons_eq
     2150          >increment_to_carry_aux @refl
     2151     ]
     2152] qed.
     2153
     2154lemma increment_to_carry : ∀n. ∀a,b : BitVector n.
     2155  addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
     2156#n #a #b >increment_to_carry_zero <associative_addition_n_direct
     2157>neutral_addition_n_direct @refl
     2158qed.
     2159
     2160lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.
     2161#n #v whd in match (increment ??);
     2162>addition_n_direct_ok <increment_to_carry_zero @refl
     2163qed.
     2164
     2165(* Prove -(a + b) = -a + -b *)
     2166lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.
     2167  twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
     2168whd in match twocomp_neg_direct; normalize nodelta
     2169lapply increment_inj_inv
     2170whd in match increment_direct; normalize nodelta
     2171#H #n #a #b
     2172<associative_addition_n_direct @H
     2173>associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
     2174>increment_to_carry
     2175-H lapply b lapply a -b -a
     2176cases n
     2177[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
     2178| 2: #n' #a #b
     2179     cut (negation_bv ? (addition_n_direct ? a b false)
     2180           = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
     2181          notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
     2182     [ -n lapply b lapply a elim n'
     2183     [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
     2184          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
     2185          cases hd_a cases hd_b normalize @conj @refl
     2186     | 2: #n #Hind #a #b
     2187          elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
     2188          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
     2189          lapply (Hind tl_a tl_b) * #H1 #H2
     2190          @conj
     2191          [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
     2192               >carry_notb >H2 @refl
     2193          | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
     2194               >negation_bv_Sn >negation_bv_Sn
     2195               >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
     2196               >xorb_lneg >xorb_rneg >notb_notb
     2197               <xorb_rneg >H2 @refl
     2198          ]
     2199      ] ]
     2200      * #H1 #H2 @H1
     2201] qed.
     2202
     2203lemma addition_n_direct_neg : ∀n. ∀a.
     2204 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
     2205 ∧ (ith_carry n a (negation_bv n a) false = false).
     2206#n elim n
     2207[ 1: #a >(BitVector_O … a) @conj @refl
     2208| 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
     2209     lapply (Hind … tl) -Hind * #HA #HB
     2210     @conj
     2211     [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
     2212     | 1: >negation_bv_Sn >addition_n_direct_Sn
     2213          >ith_bit_Sn >HB >xorb_false >HA
     2214          @bitvector_cons_eq elim hd @refl
     2215     ]
     2216] qed.
     2217
     2218(* -a + a = 0 *)
     2219lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
     2220whd in match twocomp_neg_direct;
     2221whd in match increment_direct;
     2222normalize nodelta
     2223#n #a <associative_addition_n_direct
     2224elim (addition_n_direct_neg … a) #H #_ >H
     2225-H -a
     2226cases n try //
     2227#n'
     2228cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
     2229       ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
     2230[ elim n'
     2231     [ 1: @conj @refl
     2232     | 2: #n' * #HA #HB @conj
     2233          [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
     2234               >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
     2235          | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
     2236     ]
     2237] * #H1 #H2 @H1
     2238qed.
     2239
     2240(* Lift back the previous result to standard operations. *)
     2241lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
     2242#n #v whd in match twocomp_neg_direct; normalize nodelta
     2243whd in match increment_direct; normalize nodelta
     2244whd in match two_complement_negation; normalize nodelta
     2245>increment_to_addition_n <addition_n_direct_ok
     2246whd in match addition_n; normalize nodelta
     2247elim (add_with_carries ????) #a #b @refl
     2248qed.
     2249
     2250lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
     2251  two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
     2252#n #a #b
     2253lapply (twocomp_neg_plus ? a b)
     2254>twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
     2255<addition_n_direct_ok <addition_n_direct_ok
     2256whd in match addition_n; normalize nodelta
     2257elim (add_with_carries n a b false) #bits #flags normalize nodelta
     2258elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
     2259normalize nodelta #H @H
     2260qed.
     2261
     2262lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
     2263#n #a lapply (bitvector_opp_direct ? a)
     2264>twocomp_neg_direct_ok <addition_n_direct_ok
     2265whd in match (addition_n ???);
     2266elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
     2267qed.
     2268
     2269lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
     2270#n #a
     2271lapply (neutral_addition_n_direct n a)
     2272<addition_n_direct_ok
     2273whd in match (addition_n ???);
     2274elim (add_with_carries n a (zero n) false) #bits #flags #H @H
     2275qed.
     2276
     2277lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.
     2278  addition_n ? x delta = addition_n ? y delta → x = y. 
     2279#n #x #y #delta 
     2280lapply (addition_n_direct_inj … x y delta)
     2281<addition_n_direct_ok <addition_n_direct_ok
     2282whd in match addition_n; normalize nodelta
     2283elim (add_with_carries n x delta false) #bitsx #flagsx
     2284elim (add_with_carries n y delta false) #bitsy #flagsy
     2285normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq
     2286qed.
     2287
     2288lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.
     2289  x ≠ y → addition_n ? x delta ≠ addition_n ? y delta. 
     2290#n #x #y #delta 
     2291lapply (addition_n_direct_inj_inv … x y delta)
     2292<addition_n_direct_ok <addition_n_direct_ok
     2293whd in match addition_n; normalize nodelta
     2294elim (add_with_carries n x delta false) #bitsx #flagsx
     2295elim (add_with_carries n y delta false) #bitsy #flagsy
     2296normalize #H1 #H2 @(H1 H2)
     2297qed.
     2298
Note: See TracChangeset for help on using the changeset viewer.