Changeset 2286 for src/ASM/Vector.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Vector.ma
r2124 r2286 92 92 @(dependent_rewrite_vectors A … E) 93 93 try assumption % 94 qed. 95 96 lemma Vector_singl_elim : ∀A.∀P : Vector A 1 → Prop.∀v. 97 (∀a.v = [[ a ]] → P [[ a ]]) → P v. 98 #A #P #v 99 elim (Vector_Sn … v) #a * #tl >(Vector_O … tl) #EQ >EQ #H @H % qed. 100 101 lemma Vector_pair_elim : ∀A.∀P : Vector A 2 → Prop.∀v. 102 (∀a,b.v = [[ a ; b ]] → P [[ a ; b ]]) → P v. 103 #A #P #v 104 elim (Vector_Sn … v) #a * #tl @(Vector_singl_elim … tl) #b #EQ1 #EQ2 destruct 105 #H @H % 106 qed. 107 108 lemma Vector_triple_elim : ∀A.∀P : Vector A 3 → Prop.∀v. 109 (∀a,b,c.v = [[ a ; b ; c ]] → P [[ a ; b ; c ]]) → P v. 110 #A #P #v 111 elim (Vector_Sn … v) #a * #tl @(Vector_pair_elim … tl) #b #c #EQ1 #EQ2 destruct 112 #H @H % 94 113 qed. 95 114 … … 214 233 [ VEmpty ⇒ I  VCons m hd tl ⇒ tl ]. 215 234 235 lemma tail_head' : ∀A,n,v.v = head' A n v ::: tail … v. 236 #A #n #v elim (Vector_Sn … v) #hd * #tl #EQ >EQ % qed. 237 216 238 let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝ 217 239 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with … … 421 443 qed. 422 444 445 lemma vector_append_empty : ∀A,n.∀v : Vector A n.v @@ [[ ]] ≃ v. 446 #A #n #v elim v n [%] 447 #n #hd #tl change with (?→?:::(?@@?)≃?) 448 lapply (tl@@[[ ]]) 449 <plus_n_O #v #EQ >EQ % 450 qed. 451 423 452 lemma vector_associative_append: 424 453 ∀A: Type[0]. … … 591 620 // 592 621 qed. 593 622 623 lemma v_invert_append : ∀A,n,m.∀v,v' : Vector A n.∀u,u' : Vector A m. 624 v @@ u = v' @@ u' → v = v' ∧ u = u'. 625 #A #n #m #v elim v n 626 [ #v' >(Vector_O ? v') #u #u' normalize #EQ %{EQ} % 627  #n #hd #tl #IH #v' elim (Vector_Sn ?? v') #hd' * #tl' #EQv' >EQv' v' 628 #u #u' normalize #EQ destruct(EQ) elim (IH … e0) #EQ' #EQ'' %{EQ''} 629 >EQ' % 630 ] 631 qed. 632 594 633 (* ===================================== *) 595 634 (* Other manipulations. *) … … 761 800 #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/ 762 801 ] qed. 802 803 lemma eq_v_append : ∀A,n,m,test,v1,v2,u1,u2. 804 eq_v A (n+m) test (v1@@u1) (v2@@u2) = 805 (eq_v A n test v1 v2 ∧ eq_v A m test u1 u2). 806 #A #n #m #test #v1 lapply m m elim v1 n 807 [ #m #v2 >(Vector_O … v2) #u1 #u2 % ] 808 #n #hd #tl #IH #m #v2 809 elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ v2 810 #u1 #u2 whd in ⊢ (??%(?%?)); 811 whd in match (head' ???); 812 whd in match (tail ???); 813 whd in match (tail ???); 814 elim (test ??) normalize nodelta [ @IH  % ] 815 qed. 763 816 764 817 (* ===================================== *) … … 881 934 ] 882 935 qed. 936 937 (* ===================================== *) 938 (* Vector prefix and suffix relations. *) 939 (* ===================================== *) 940 941 (* n.b.: if n = m this is equivalent to equality, without n and m needing to be 942 Leibnizequal *) 943 let rec vprefix A n m (test : A → A → bool) (v1 : Vector A n) (v2 : Vector A m) on v1 : bool ≝ 944 match v1 with 945 [ VEmpty ⇒ true 946  VCons n' hd1 tl1 ⇒ 947 match v2 with 948 [ VEmpty ⇒ false 949  VCons m' hd2 tl2 ⇒ test hd1 hd2 ∧ vprefix … test tl1 tl2 950 ] 951 ]. 952 953 let rec vsuffix A n m test (v1 : Vector A n) (v2 : Vector A m) on v2 : bool ≝ 954 If leb (S n) m then with prf do 955 match v2 return λm.λv2:Vector A m.leb (S n) m → bool with 956 [ VEmpty ⇒ Ⓧ 957  VCons m' hd2 tl2 ⇒ λ_.vsuffix ?? m' test v1 tl2 958 ] prf 959 else (if eqb n m then 960 vprefix A n m test v1 v2 961 else 962 false). 963 964 include alias "arithmetics/nat.ma". 965 966 lemma prefix_to_le : ∀A,n,m,test,v1,v2. 967 vprefix A n m test v1 v2 → n ≤ m. 968 #A #n #m #test #v1 lapply m m elim v1 n [//] 969 #n #hd #tl #IH #m * m [*] 970 #m #hd' #tl' 971 whd in ⊢ (?%→?); 972 elim (test ??) [2: *] 973 whd in ⊢ (?%→?); 974 #H @le_S_S @(IH … H) 975 qed. 976 977 lemma vprefix_ok : ∀A,n,m,test,v1,v2. 978 vprefix A n m test v1 v2 → le n m ∧ 979 ∃pre.∃post : Vector A (m  n).v2 ≃ pre @@ post ∧ 980 bool_to_Prop (eq_v … test v1 pre). 981 #A #n #m #test #v1 #v2 #G %{(prefix_to_le … G)} 982 lapply G lapply v2 lapply m m elim v1 n 983 [ #m #v2 * <minus_n_O %{[[ ]]} %{v2} % % ] 984 #n #hd1 #tl1 #IH #m * m [*] 985 #m #hd2 #tl2 whd in ⊢ (?%→?); 986 elim (true_or_false_Prop (test hd1 hd2)) #H >H normalize nodelta [2: *] 987 #G elim (IH … G) #pre * #post * #EQ #EQ' 988 %{(hd2:::pre)} %{post} % 989 [ change with (?≃hd2 ::: (? @@ ?)) lapply EQ lapply (pre @@ post) 990 <(minus_to_plus m … (prefix_to_le … G) (refl …)) 991 #V #EQ'' >EQ'' % 992  whd in ⊢ (?%); 993 whd in match (head' ???); >H 994 @EQ' 995 ] 996 qed. 997 998 lemma vprefix_to_eq : ∀A,n,test,v1,v2. 999 vprefix A n n test v1 v2 = eq_v … test v1 v2. 1000 #A #n #test #v1 elim v1 n 1001 [ #v2 >(Vector_O … v2) % 1002  #n #hd1 #tl1 #IH 1003 #v2 elim (Vector_Sn … v2) #hd2 * #tl2 #EQ destruct(EQ) 1004 normalize elim (test ??) [2: %] 1005 normalize @IH 1006 ] 1007 qed. 1008 1009 lemma vprefix_true : ∀A,n,m,test.∀v1,pre : Vector A n.∀post : Vector A m. 1010 eq_v … test v1 pre → bool_to_Prop (vprefix … test v1 (pre @@ post)). 1011 #A #n #m #test #v1 lapply m m elim v1 n 1012 [ #m #pre #post #_ % 1013  #n #hd #tl #IH #m #pre elim (Vector_Sn … pre) #hd' * #tl' #EQpre >EQpre 1014 #post 1015 whd in ⊢ (?%→?%); whd in match (head' ???); 1016 elim (test hd hd') [2: *] normalize nodelta whd in match (tail ???); 1017 @IH 1018 ] 1019 qed. 1020 1021 lemma vsuffix_to_le : ∀A,n,m,test,v1,v2. 1022 vsuffix A n m test v1 v2 → n ≤ m. 1023 #A #n #m #test #v1 #v2 lapply v1 lapply n n elim v2 m 1024 [ #n * n 1025 [ * % 1026  #n #hd #tl * 1027 ] 1028  #m #hd2 #tl2 #IH 1029 #n #v1 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?) 1030 @If_elim normalize nodelta @leb_elim #H * 1031 [ #_ @(transitive_le … H) %2 %1 1032  #ABS elim (ABS I) 1033  #_ @eqb_elim #G normalize nodelta [2: *] 1034 destruct #_ % 1035 ] 1036 ] 1037 qed. 1038 1039 lemma vsuffix_ok : ∀A,n,m,test,v1,v2. 1040 vsuffix A n m test v1 v2 → le n m ∧ 1041 ∃pre : Vector A (m  n).∃post.v2 ≃ pre @@ post ∧ 1042 bool_to_Prop (eq_v … test v1 post). 1043 #A #n #m #test #v1 #v2 #G %{(vsuffix_to_le … G)} 1044 lapply G lapply v1 lapply n n 1045 elim v2 m 1046 [ #n #v1 1047 whd in ⊢ (?%→?); 1048 @eqb_elim #EQ1 [2: *] 1049 normalize nodelta lapply v1 v1 >EQ1 #v1 1050 >(Vector_O … v1) * %{[[ ]]} %{[[ ]]} % % 1051  #m #hd2 #tl2 #IH #n #v1 1052 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?) 1053 @If_elim normalize nodelta #H 1054 [ #G elim (IH … G) #pre * #post * #EQ1 #EQ2 1055 >minus_Sn_m 1056 [ %{(hd2:::pre)} %{post} %{EQ2} 1057 change with (?≃?:::(?@@?)) 1058 lapply EQ1 lapply (pre@@post) 1059 <plus_minus_m_m 1060 [ #v #EQ >EQ %] 1061 ] 1062 @(vsuffix_to_le … G) 1063  @eqb_elim #EQn [2: *] normalize nodelta 1064 generalize in match (hd2:::tl2); 1065 <EQn in ⊢ (%→%→??(λ_.??(λ_.?(?%%??)?))); 1066 #v2' >vprefix_to_eq #G 1067 <EQn in ⊢ (?%(λ_:%.??(λ_.?(???%%)?))); 1068 <minus_n_n %{[[ ]]} %{v2'} %{G} 1069 % 1070 ] 1071 ] 1072 qed. 1073 1074 lemma vsuffix_true : ∀A,n,m,test.∀pre : Vector A n.∀v1,post : Vector A m. 1075 eq_v … test v1 post → bool_to_Prop (vsuffix … test v1 (pre @@ post)). 1076 #A #n #m #test #pre lapply m m elim pre n 1077 [ #m #v1 #post lapply v1 v1 cases post m 1078 [ #v1 >(Vector_O … v1) * % 1079  #m #hd #tl #v1 #G 1080 change with (bool_to_Prop (If ? then with prf do ? else ?)) 1081 @If_elim normalize nodelta 1082 [ @leb_elim #H * @⊥ @(absurd ? H ?) normalize // ] 1083 #_ >eqb_n_n normalize nodelta 1084 >vprefix_to_eq assumption 1085 ] 1086  #n #hd2 #tl2 #IH 1087 #m #v1 #post #G 1088 change with (bool_to_Prop (If ? then with prf do ? else ?)) 1089 @If_elim normalize nodelta 1090 [ #H @IH @G 1091  @leb_elim [ #_ * #ABS elim (ABS I) ] 1092 #H #_ @eqb_elim #K 1093 [ @⊥ @(absurd ? K) @lt_to_not_eq // ] 1094 normalize elim H H #H @H normalize 1095 >plus_n_Sm_fast // 1096 ] 1097 ] 1098 qed. 1099 1100 (* ===================================== *) 1101 (* Vector flattening and recursive splitting. *) 1102 (* ===================================== *) 1103 1104 let rec rvsplit A n m on n : Vector A (n * m) → Vector (Vector A m) n ≝ 1105 match n return λn.Vector ? (n * m) → Vector (Vector ? m) n with 1106 [ O ⇒ λ_.VEmpty ? 1107  S k ⇒ 1108 λv.let 〈pre,post〉 ≝ vsplit … m (k*m) v in 1109 pre ::: rvsplit … post 1110 ]. 1111 1112 let rec vflatten A n m (v : Vector (Vector A m) n) on v : Vector A (n * m) ≝ 1113 match v return λn.λ_ : Vector ? n.Vector ? (n * m) with 1114 [ VEmpty ⇒ VEmpty ? 1115  VCons n' hd tl ⇒ hd @@ vflatten ? n' m tl 1116 ]. 1117 1118 lemma vflatten_rvsplit : ∀A,n,m,v.vflatten A n m (rvsplit A n m v) = v. 1119 #A #n elim n n 1120 [ #m #v >(Vector_O ? v) % 1121  #n #IH #m #v 1122 whd in match (rvsplit ????); 1123 @vsplit_elim #pre #post #EQ 1124 normalize nodelta 1125 whd in match (vflatten ????); >IH >EQ % 1126 ] 1127 qed. 1128 1129 lemma rvsplit_vflatten : ∀A,n,m,v.rvsplit A n m (vflatten A n m v) = v. 1130 #A #n #m #v elim v n 1131 [ % 1132  #n #hd #tl #IH 1133 whd in match (vflatten ????); 1134 whd in match (rvsplit ????); 1135 @vsplit_elim #pre #post #EQ 1136 elim (v_invert_append … EQ) #EQ1 #EQ2 <EQ1 <EQ2 1137 normalize nodelta >IH % 1138 ] 1139 qed. 1140 1141 (* Paolo: should'nt it be in the standard library? *) 1142 lemma sym_jmeq : ∀A,B.∀a : A.∀b : B.a≃b → b≃a. 1143 #A #B #a #b * % qed. 1144 1145 lemma vflatten_append : ∀A,n,m,p,v1,v2. 1146 vflatten A (n+m) p (v1 @@ v2) ≃ vflatten A n p v1 @@ vflatten A m p v2. 1147 #A #n #m #p #v1 lapply m m elim v1 1148 [ #m #v2 % 1149  #n #hd1 #tl1 #IH #m #v2 1150 whd in ⊢ (??%?(????%?)); 1151 lapply (IH … v2) 1152 lapply (vflatten … (tl1@@v2)) 1153 cut ((n+m)*p = n*p + m*p) 1154 [ // ] #EQ whd in match (S n + m); whd in match (S ? * ?); 1155 whd in match (S n * ?); >EQ in ⊢ (%→?%%??→?%%??); EQ 1156 #V #EQ >EQ V @sym_jmeq @vector_associative_append 1157 ] 1158 qed. 1159 1160 lemma eq_v_vflatten : ∀A,n,m,test,v1,v2. 1161 eq_v A ? test (vflatten A n m v1) (vflatten A n m v2) = 1162 eq_v ?? (eq_v … test) v1 v2. 1163 #A #n #m #test #v1 elim v1 n 1164 [ #v2 >(Vector_O … v2) % ] 1165 #n #hd #tl #IH #v2 1166 elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ v2 1167 whd in ⊢ (??(????%%)%); 1168 whd in match (head' ???); 1169 whd in match (tail ???); 1170 >eq_v_append >IH % 1171 qed. 1172 1173 lemma vprefix_vflatten : ∀A,n,m,p,test.∀v1,v2. 1174 vprefix ? n m (eq_v ? p test) v1 v2 → 1175 bool_to_Prop (vprefix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)). 1176 #A #n #m #p #test #v1 #v2 #G 1177 elim (vprefix_ok … G) #le_nm 1178 * #pre * #post * 1179 lapply (vflatten_append … pre post) 1180 lapply (pre @@ post) 1181 <(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?); 1182 #v2' #EQ1 #EQ2 >EQ2 v2 lapply EQ1 EQ1 1183 lapply (vflatten A m p v2') 1184 cut (m*p = n*p + (mn)*p) 1185 [ <(commutative_times p) <(commutative_times p) <(commutative_times p) 1186 <distributive_times_plus <(minus_to_plus … le_nm (refl …)) % ] 1187 #EQ >EQ #v2' #EQ' >EQ' v2' v2' 1188 #G @vprefix_true 1189 >eq_v_vflatten @G 1190 qed. 1191 1192 lemma vsuffix_vflatten : ∀A,n,m,p,test.∀v1,v2. 1193 vsuffix ? n m (eq_v ? p test) v1 v2 → 1194 bool_to_Prop (vsuffix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)). 1195 #A #n #m #p #test #v1 #v2 #G 1196 elim (vsuffix_ok … G) #le_nm * #pre * #post * 1197 lapply (vflatten_append … pre post) 1198 lapply (pre @@ post) 1199 >commutative_plus in ⊢ (%→?%%??→???%%→?); 1200 <(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?); 1201 #v2' #EQ1 #EQ2 >EQ2 v2 lapply EQ1 EQ1 1202 lapply (vflatten A m p v2') 1203 cut (m*p = (mn)*p + n*p) 1204 [ <(commutative_times p) <(commutative_times p) <(commutative_times p) 1205 <distributive_times_plus <commutative_plus <(minus_to_plus … le_nm (refl …)) % ] 1206 #EQ >EQ #v2' #EQ' >EQ' 1207 #G @vsuffix_true 1208 >eq_v_vflatten @G 1209 qed.
Note: See TracChangeset
for help on using the changeset viewer.