Ignore:
Timestamp:
Jun 29, 2011, 10:47:39 AM (8 years ago)
Author:
mulligan
Message:

resolved conflict in rtlabs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1043 r1045  
    10681068     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    10691069
    1070 axiom split_elim:
     1070lemma split_zero:
     1071  ∀A,m.
     1072  ∀v: Vector A m.
     1073    〈[[]], v〉 = split A 0 m v.
     1074  #A #m #v
     1075  elim v
     1076  [ %
     1077  | #n #hd #tl #ih
     1078    normalize in ⊢ (???%) %
     1079  ]
     1080qed.
     1081
     1082lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
     1083 #A #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     1084 #n #hd #tl #abs @⊥ destruct (abs)
     1085qed.
     1086
     1087lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
     1088 ∃hd.∃tl.v ≃ VCons A n hd tl.
     1089 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     1090 [ #abs @⊥ destruct (abs)
     1091 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     1092qed.
     1093
     1094lemma vector_append_zero:
     1095  ∀A,m.
     1096  ∀v: Vector A m.
     1097  ∀q: Vector A 0.
     1098    v = q@@v.
     1099  #A #m #v #q
     1100  >(Vector_O A q) %
     1101qed.
     1102
     1103lemma prod_eq_left:
     1104  ∀A: Type[0].
     1105  ∀p, q, r: A.
     1106    p = q → 〈p, r〉 = 〈q, r〉.
     1107  #A #p #q #r #hyp
     1108  >hyp %
     1109qed.
     1110
     1111lemma prod_eq_right:
     1112  ∀A: Type[0].
     1113  ∀p, q, r: A.
     1114    p = q → 〈r, p〉 = 〈r, q〉.
     1115  #A #p #q #r #hyp
     1116  >hyp %
     1117qed.
     1118
     1119corollary prod_vector_zero_eq_left:
     1120  ∀A, n.
     1121  ∀q: Vector A O.
     1122  ∀r: Vector A n.
     1123    〈q, r〉 = 〈[[ ]], r〉.
     1124  #A #n #q #r
     1125  generalize in match (Vector_O A q …)
     1126  #hyp
     1127  >hyp in ⊢ (??%?)
     1128  %
     1129qed.
     1130
     1131axiom split_succ:
     1132  ∀A, m, n.
     1133  ∀l: Vector A m.
     1134  ∀r: Vector A n.
     1135  ∀v: Vector A (m + n).
     1136  ∀hd: A.
     1137    v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
     1138(*
     1139  #A #m
     1140  elim m
     1141  [ #n #l #r #v #hd #equal #hyp
     1142    normalize >(Vector_O A l) >equal
     1143    >(Vector_O A l) %
     1144  | #n' #ih #n #l #r #v #hd
     1145    #equal #hyp
     1146    cases(Vector_Sn A n' l)
     1147    #hd' #exists
     1148    cases exists #tl #jmeq
     1149    >jmeq *)
     1150
     1151lemma split_prod:
     1152  ∀A,m,n.
     1153  ∀p: Vector A (m + n).
     1154  ∀v: Vector A m.
     1155  ∀q: Vector A n.
     1156    p = v@@q → 〈v, q〉 = split A m n p.
     1157  #A #m
     1158  elim m
     1159  [ #n #p #v #q #hyp
     1160    >hyp <(vector_append_zero A n q v)
     1161    >(prod_vector_zero_eq_left A …)
     1162    @split_zero
     1163  | #r #ih #n #p #v #q #hyp
     1164    >hyp
     1165    cases (Vector_Sn A r v)
     1166    #hd #exists
     1167    cases exists
     1168    #tl #jmeq >jmeq
     1169    @split_succ [1: % |2: @ih % ]
     1170  ]
     1171qed.
     1172
     1173lemma split_prod_exists:
     1174  ∀A, m, n.
     1175  ∀p: Vector A (m + n).
     1176  ∃v: Vector A m.
     1177  ∃q: Vector A n.
     1178    〈v, q〉 = split A m n p.
     1179  #A #m #n #p
     1180  elim m
     1181  @ex_intro
     1182  [1:
     1183  |2: @ex_intro
     1184      [1:
     1185      |2:
     1186      ]
     1187  ]
     1188
     1189lemma split_elim:
    10711190 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
    10721191  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
     1192  #A #l #m #v #P #hyp
     1193  normalize
     1194  <(split_prod A l m v ? ? ?)
    10731195
    10741196example half_add_SO:
     
    11101232  | cons hd tl ⇒
    11111233    let 〈new_pc, byte〉 ≝ next code_memory pc in
    1112       hd = byte ∧ encoding_check code_memory new_pc final_pc tl
     1234      hd = byte ∧ encoding_check code_memory new_c final_pc tl
    11131235  ].
    11141236
Note: See TracChangeset for help on using the changeset viewer.