Changeset 2468 for src/Clight/frontend_misc.ma
- Timestamp:
- Nov 15, 2012, 6:12:57 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/frontend_misc.ma
r2448 r2468 10 10 include "basics/lists/listb.ma". 11 11 include "basics/lists/list.ma". 12 13 14 (* --------------------------------------------------------------------------- *) 15 (* [cthulhu] plays the same role as daemon. It should be droppable. *) 16 (* --------------------------------------------------------------------------- *) 17 18 axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *) 12 19 13 20 (* --------------------------------------------------------------------------- *) … … 1647 1654 | 3,4: @reflexive_lset_inclusion ] 1648 1655 qed. 1656 1657 (* --------------------------------------------------------------------------- *) 1658 (* Stuff on bitvectors, previously in memoryInjections.ma *) 1659 (* --------------------------------------------------------------------------- *) 1660 (* --------------------------------------------------------------------------- *) 1661 (* Some general lemmas on bitvectors (offsets /are/ bitvectors) *) 1662 (* --------------------------------------------------------------------------- *) 1663 1664 lemma 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 1668 cases n in tl; 1669 [ 1: #tl cases hd normalize @refl 1670 | 2: #n' #tl cases hd normalize @refl ] 1671 qed. 1672 1673 lemma 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 // 1676 qed. 1677 1678 lemma replicate_Sn : ∀A,sz,elt. 1679 replicate A (S sz) elt = elt ::: (replicate A sz elt). 1680 // qed. 1681 1682 lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed. 1683 1684 lemma 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 *) 1688 lemma carry_of_TT : ∀x. carry_of true true x = true. // qed. 1689 lemma carry_of_TF : ∀x. carry_of true false x = x. // qed. 1690 lemma carry_of_FF : ∀x. carry_of false false x = false. // qed. 1691 lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed. 1692 lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed. 1693 1694 1695 1696 definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)). 1697 1698 lemma 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 1721 lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)). 1722 #n lapply (one_bv_Sn_aux n) 1723 whd in match (one_bv ?) in ⊢ (? → (??%%)); 1724 elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags 1725 #H lapply (H bits flags (refl ??)) #H2 >H2 @refl 1726 qed. 1727 1728 lemma 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 1731 elim 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. *) 1746 lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n). 1747 #n 1748 whd in match (increment ??) in ⊢ (∀_.??%?); 1749 whd 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 1752 qed. 1753 1754 (* Explicit formulation of addition *) 1755 1756 (* Explicit formulation of the last carry bit *) 1757 let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝ 1758 match 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 1768 lemma 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 1772 lemma 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] *) 1776 lemma 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. *) 1805 definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit. 1806 match 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 1816 lemma 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 1820 lemma 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 *) 1824 lemma 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 1828 cases 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 *) 1853 let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝ 1854 match 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 *) 1862 let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝ 1863 match 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 1870 lemma 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. *) 1874 definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init). 1875 1876 lemma 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 1879 lemma 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 *) 1882 lemma 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 1903 lemma 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 1906 cases (add_with_carries ????) // 1907 qed. 1908 1909 (* trivially lift associativity to our new setting *) 1910 lemma 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 1916 lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3) 1917 elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta 1918 elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta 1919 #H @(sym_eq … H) 1920 qed. 1921 1922 lemma 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/ 1925 qed. 1926 1927 definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false. 1928 definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v). 1929 1930 1931 (* fold andb on a bitvector. *) 1932 let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝ 1933 match b with 1934 [ VEmpty ⇒ true 1935 | VCons sz elt tl ⇒ 1936 andb elt (andb_fold ? tl) 1937 ]. 1938 1939 lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed. 1940 1941 lemma 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 1943 qed. 1944 1945 lemma 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 1957 lemma 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 1960 elim (BitVector_Sn … a) #hd * #tl #Heq >Heq 1961 whd 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 *) 1970 lemma 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. *) 1986 lemma 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 2011 lemma 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 2014 lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed. 2015 2016 (* Injectivity of increment *) 2017 lemma 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) *) 2045 lemma increment_inj_inv : ∀n. ∀a,b : BitVector n. 2046 a = b → increment_direct ? a = increment_direct ? b. // qed. 2047 2048 (* A more general result. *) 2049 lemma 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. *) 2073 lemma 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 2111 lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed. 2112 2113 lemma 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 2123 lemma 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. 2127 qed. 2128 2129 lemma 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 2139 lemma 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 2154 lemma 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 2158 qed. 2159 2160 lemma 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 2163 qed. 2164 2165 (* Prove -(a + b) = -a + -b *) 2166 lemma 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. 2168 whd in match twocomp_neg_direct; normalize nodelta 2169 lapply increment_inj_inv 2170 whd 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 2176 cases 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 2203 lemma 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 *) 2219 lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?). 2220 whd in match twocomp_neg_direct; 2221 whd in match increment_direct; 2222 normalize nodelta 2223 #n #a <associative_addition_n_direct 2224 elim (addition_n_direct_neg … a) #H #_ >H 2225 -H -a 2226 cases n try // 2227 #n' 2228 cut ((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 2238 qed. 2239 2240 (* Lift back the previous result to standard operations. *) 2241 lemma 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 2243 whd in match increment_direct; normalize nodelta 2244 whd in match two_complement_negation; normalize nodelta 2245 >increment_to_addition_n <addition_n_direct_ok 2246 whd in match addition_n; normalize nodelta 2247 elim (add_with_carries ????) #a #b @refl 2248 qed. 2249 2250 lemma 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 2253 lapply (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 2256 whd in match addition_n; normalize nodelta 2257 elim (add_with_carries n a b false) #bits #flags normalize nodelta 2258 elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags' 2259 normalize nodelta #H @H 2260 qed. 2261 2262 lemma 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 2265 whd in match (addition_n ???); 2266 elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H 2267 qed. 2268 2269 lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a. 2270 #n #a 2271 lapply (neutral_addition_n_direct n a) 2272 <addition_n_direct_ok 2273 whd in match (addition_n ???); 2274 elim (add_with_carries n a (zero n) false) #bits #flags #H @H 2275 qed. 2276 2277 lemma 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 2280 lapply (addition_n_direct_inj … x y delta) 2281 <addition_n_direct_ok <addition_n_direct_ok 2282 whd in match addition_n; normalize nodelta 2283 elim (add_with_carries n x delta false) #bitsx #flagsx 2284 elim (add_with_carries n y delta false) #bitsy #flagsy 2285 normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq 2286 qed. 2287 2288 lemma 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 2291 lapply (addition_n_direct_inj_inv … x y delta) 2292 <addition_n_direct_ok <addition_n_direct_ok 2293 whd in match addition_n; normalize nodelta 2294 elim (add_with_carries n x delta false) #bitsx #flagsx 2295 elim (add_with_carries n y delta false) #bitsy #flagsy 2296 normalize #H1 #H2 @(H1 H2) 2297 qed. 2298
Note: See TracChangeset
for help on using the changeset viewer.