Changeset 2286 for src/ASM/Vector.ma

Timestamp:

Aug 2, 2012, 3:18:11 PM (7 years ago)

Author:

tranquil

Message:

Big update!

• merge of all _paolo variants
• reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
• split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:

• src/ASM/Vector.ma (modified) (6 diffs)

src/ASM/Vector.ma

@@ -92 +92 @@
   @(dependent_rewrite_vectors A … E)
   try assumption %
+qed.
+
+lemma Vector_singl_elim : ∀A.∀P : Vector A 1 → Prop.∀v.
+  (∀a.v = [[ a ]] → P [[ a ]]) → P v.
+#A #P #v
+elim (Vector_Sn … v) #a * #tl >(Vector_O … tl) #EQ >EQ #H @H % qed.
+
+lemma Vector_pair_elim : ∀A.∀P : Vector A 2 → Prop.∀v.
+  (∀a,b.v = [[ a ; b ]] → P [[ a ; b ]]) → P v.
+#A #P #v
+elim (Vector_Sn … v) #a * #tl @(Vector_singl_elim … tl) #b #EQ1 #EQ2 destruct
+#H @H %
+qed.
+
+lemma Vector_triple_elim : ∀A.∀P : Vector A 3 → Prop.∀v.
+  (∀a,b,c.v = [[ a ; b ; c ]] → P [[ a ; b ; c ]]) → P v.
+#A #P #v
+elim (Vector_Sn … v) #a * #tl @(Vector_pair_elim … tl) #b #c #EQ1 #EQ2 destruct
+#H @H %
 qed.
 
@@ -214 +233 @@
 [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
 
+lemma tail_head' : ∀A,n,v.v = head' A n v ::: tail … v.
+#A #n #v elim (Vector_Sn … v) #hd * #tl #EQ >EQ % qed.
+
 let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
  match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
@@ -421 +443 @@
 qed.
 
+lemma vector_append_empty : ∀A,n.∀v : Vector A n.v @@ [[ ]] ≃ v.
+#A #n #v elim v -n [%]
+#n #hd #tl change with (?→?:::(?@@?)≃?)
+lapply (tl@@[[ ]])
+<plus_n_O #v #EQ >EQ %
+qed.
+
 lemma vector_associative_append:
   ∀A: Type[0].
@@ -591 +620 @@
     //
 qed.
-    
+
+lemma v_invert_append : ∀A,n,m.∀v,v' : Vector A n.∀u,u' : Vector A m.
+  v @@ u = v' @@ u' → v = v' ∧ u = u'.
+#A #n #m #v elim v -n
+[ #v' >(Vector_O ? v') #u #u' normalize #EQ %{EQ} %
+| #n #hd #tl #IH #v' elim (Vector_Sn ?? v') #hd' * #tl' #EQv' >EQv' -v'
+  #u #u' normalize #EQ destruct(EQ) elim (IH … e0) #EQ' #EQ'' %{EQ''}
+  >EQ' %
+]
+qed.
+
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 (* Other manipulations.                                                       *)
@@ -761 +800 @@
   #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
 ] qed.
+
+lemma eq_v_append : ∀A,n,m,test,v1,v2,u1,u2.
+  eq_v A (n+m) test (v1@@u1) (v2@@u2) =
+  (eq_v A n test v1 v2 ∧ eq_v A m test u1 u2).
+#A #n #m #test #v1 lapply m -m elim v1 -n
+[ #m #v2 >(Vector_O … v2) #u1 #u2 % ]
+#n #hd #tl #IH #m #v2
+elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
+#u1 #u2 whd in ⊢ (??%(?%?));
+whd in match (head' ???);
+whd in match (tail ???);
+whd in match (tail ???);
+elim (test ??) normalize nodelta [ @IH | % ]
+qed.
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -881 +934 @@
   ]
 qed.
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Vector prefix and suffix relations.                                        *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)    
+
+(* n.b.: if n = m this is equivalent to equality, without n and m needing to be
+   Leibniz-equal *)
+let rec vprefix A n m (test : A → A → bool) (v1 : Vector A n) (v2 : Vector A m) on v1 : bool ≝
+match v1 with
+[ VEmpty ⇒ true
+| VCons n' hd1 tl1 ⇒
+  match v2 with
+  [ VEmpty ⇒ false
+  | VCons m' hd2 tl2 ⇒ test hd1 hd2 ∧ vprefix … test tl1 tl2
+  ]
+].
+
+let rec vsuffix A n m test (v1 : Vector A n) (v2 : Vector A m) on v2 : bool ≝
+If leb (S n) m then with prf do
+  match v2 return λm.λv2:Vector A m.leb (S n) m → bool with
+  [ VEmpty ⇒ Ⓧ
+  | VCons m' hd2 tl2 ⇒ λ_.vsuffix ?? m' test v1 tl2
+  ] prf
+else (if eqb n m then
+  vprefix A n m test v1 v2
+else
+  false).
+
+include alias "arithmetics/nat.ma".
+
+lemma prefix_to_le : ∀A,n,m,test,v1,v2.
+  vprefix A n m test v1 v2 → n ≤ m.
+#A #n #m #test #v1 lapply m -m elim v1 -n [//]
+#n #hd #tl #IH #m * -m [*]
+#m #hd' #tl'
+whd in ⊢ (?%→?);
+elim (test ??) [2: *]
+whd in ⊢ (?%→?);
+#H @le_S_S @(IH … H)
+qed.
+
+lemma vprefix_ok : ∀A,n,m,test,v1,v2.
+  vprefix A n m test v1 v2 → le n m ∧
+  ∃pre.∃post : Vector A (m - n).v2 ≃ pre @@ post ∧
+            bool_to_Prop (eq_v … test v1 pre).
+#A #n #m #test #v1 #v2 #G %{(prefix_to_le … G)}
+lapply G lapply v2 lapply m -m elim v1 -n
+[ #m #v2 * <minus_n_O %{[[ ]]} %{v2} % % ]
+#n #hd1 #tl1 #IH #m * -m [*]
+#m #hd2 #tl2 whd in ⊢ (?%→?);
+elim (true_or_false_Prop (test hd1 hd2)) #H >H normalize nodelta [2: *]
+#G elim (IH … G) #pre * #post * #EQ #EQ'
+%{(hd2:::pre)} %{post} %
+[ change with (?≃hd2 ::: (? @@ ?)) lapply EQ lapply (pre @@ post)
+  <(minus_to_plus m … (prefix_to_le … G) (refl …))
+  #V #EQ'' >EQ'' %
+| whd in ⊢ (?%);
+  whd in match (head' ???); >H
+  @EQ'
+]
+qed.
+
+lemma vprefix_to_eq : ∀A,n,test,v1,v2.
+  vprefix A n n test v1 v2 = eq_v … test v1 v2.
+#A #n #test #v1 elim v1 -n
+[ #v2 >(Vector_O … v2) %
+| #n #hd1 #tl1 #IH
+  #v2 elim (Vector_Sn … v2) #hd2 * #tl2 #EQ destruct(EQ)
+  normalize elim (test ??) [2: %]
+  normalize @IH
+]
+qed.
+
+lemma vprefix_true : ∀A,n,m,test.∀v1,pre : Vector A n.∀post : Vector A m.
+  eq_v … test v1 pre → bool_to_Prop (vprefix … test v1 (pre @@ post)).
+#A #n #m #test #v1 lapply m -m elim v1 -n
+[ #m #pre #post #_ %
+| #n #hd #tl #IH #m #pre elim (Vector_Sn … pre) #hd' * #tl' #EQpre >EQpre
+  #post
+  whd in ⊢ (?%→?%); whd in match (head' ???);
+  elim (test hd hd') [2: *] normalize nodelta whd in match (tail ???);
+  @IH
+]
+qed.
+
+lemma vsuffix_to_le : ∀A,n,m,test,v1,v2.
+  vsuffix A n m test v1 v2 → n ≤ m.
+#A #n #m #test #v1 #v2 lapply v1 lapply n -n elim v2 -m
+[ #n * -n
+  [ * %
+  | #n #hd #tl *
+  ]
+| #m #hd2 #tl2 #IH
+  #n #v1 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
+  @If_elim normalize nodelta @leb_elim #H *
+  [ #_ @(transitive_le … H) %2 %1
+  | #ABS elim (ABS I)
+  | #_ @eqb_elim #G normalize nodelta [2: *]
+    destruct #_ %
+  ]
+]
+qed.
+  
+lemma vsuffix_ok : ∀A,n,m,test,v1,v2.
+  vsuffix A n m test v1 v2 → le n m ∧
+  ∃pre : Vector A (m - n).∃post.v2 ≃ pre @@ post ∧
+            bool_to_Prop (eq_v … test v1 post).
+#A #n #m #test #v1 #v2 #G %{(vsuffix_to_le … G)}
+lapply G lapply v1 lapply n -n
+elim v2 -m
+[ #n #v1
+  whd in ⊢ (?%→?);
+  @eqb_elim #EQ1 [2: *]
+  normalize nodelta lapply v1 -v1 >EQ1 #v1
+  >(Vector_O … v1) * %{[[ ]]} %{[[ ]]} % %
+| #m #hd2 #tl2 #IH #n #v1
+  change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
+  @If_elim normalize nodelta #H
+  [ #G elim (IH … G) #pre * #post * #EQ1 #EQ2
+    >minus_Sn_m
+    [ %{(hd2:::pre)} %{post} %{EQ2}
+      change with (?≃?:::(?@@?))
+      lapply EQ1 lapply (pre@@post)
+      <plus_minus_m_m
+      [ #v #EQ >EQ %]
+    ]
+    @(vsuffix_to_le … G)
+  | @eqb_elim #EQn [2: *] normalize nodelta
+    generalize in match (hd2:::tl2);
+    <EQn in ⊢ (%→%→??(λ_.??(λ_.?(?%%??)?)));
+    #v2' >vprefix_to_eq #G
+    <EQn in ⊢ (?%(λ_:%.??(λ_.?(???%%)?)));
+    <minus_n_n %{[[ ]]} %{v2'} %{G}
+    %
+  ]
+]
+qed.
+
+lemma vsuffix_true : ∀A,n,m,test.∀pre : Vector A n.∀v1,post : Vector A m.
+  eq_v … test v1 post → bool_to_Prop (vsuffix … test v1 (pre @@ post)).
+#A #n #m #test #pre lapply m -m elim pre -n
+[ #m #v1 #post lapply v1 -v1 cases post -m
+  [ #v1 >(Vector_O … v1) * %
+  | #m #hd #tl #v1 #G
+    change with (bool_to_Prop (If ? then with prf do ? else ?))
+    @If_elim normalize nodelta 
+    [ @leb_elim #H * @⊥ @(absurd ? H ?) normalize // ]
+    #_ >eqb_n_n normalize nodelta
+    >vprefix_to_eq assumption
+  ]
+| #n #hd2 #tl2 #IH
+  #m #v1 #post #G
+  change with (bool_to_Prop (If ? then with prf do ? else ?))
+  @If_elim normalize nodelta
+  [ #H @IH @G
+  | @leb_elim [ #_ * #ABS elim (ABS I) ]
+    #H #_ @eqb_elim #K
+    [ @⊥ @(absurd ? K) @lt_to_not_eq // ]
+    normalize elim H -H #H @H normalize
+    >plus_n_Sm_fast //
+  ]
+]
+qed.
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Vector flattening and recursive splitting.                                 *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)    
+
+let rec rvsplit A n m on n : Vector A (n * m) → Vector (Vector A m) n ≝
+match n return λn.Vector ? (n * m) → Vector (Vector ? m) n with
+[ O ⇒ λ_.VEmpty ?
+| S k ⇒
+  λv.let 〈pre,post〉 ≝ vsplit … m (k*m) v in
+  pre ::: rvsplit … post
+].
+
+let rec vflatten A n m (v : Vector (Vector A m) n) on v : Vector A (n * m) ≝
+match v return λn.λ_ : Vector ? n.Vector ? (n * m) with
+[ VEmpty ⇒ VEmpty ?
+| VCons n' hd tl ⇒ hd @@ vflatten ? n' m tl
+].
+
+lemma vflatten_rvsplit : ∀A,n,m,v.vflatten A n m (rvsplit A n m v) = v.
+#A #n elim n -n
+[ #m #v >(Vector_O ? v) %
+| #n #IH #m #v
+  whd in match (rvsplit ????);
+  @vsplit_elim #pre #post #EQ
+  normalize nodelta
+  whd in match (vflatten ????); >IH >EQ %
+]
+qed.
+
+lemma rvsplit_vflatten : ∀A,n,m,v.rvsplit A n m (vflatten A n m v) = v.
+#A #n #m #v elim v -n
+[ %
+| #n #hd #tl #IH
+  whd in match (vflatten ????);
+  whd in match (rvsplit ????);
+  @vsplit_elim #pre #post #EQ
+  elim (v_invert_append … EQ) #EQ1 #EQ2 <EQ1 <EQ2
+  normalize nodelta >IH %
+]
+qed.
+
+(* Paolo: should'nt it be in the standard library? *)
+lemma sym_jmeq : ∀A,B.∀a : A.∀b : B.a≃b → b≃a.
+#A #B #a #b * % qed.
+
+lemma vflatten_append : ∀A,n,m,p,v1,v2.
+  vflatten A (n+m) p (v1 @@ v2) ≃ vflatten A n p v1 @@ vflatten A m p v2.
+#A #n #m #p #v1 lapply m -m elim v1
+[ #m #v2 %
+| #n #hd1 #tl1 #IH #m #v2
+  whd in ⊢ (??%?(????%?));
+  lapply (IH … v2)
+  lapply (vflatten … (tl1@@v2))
+  cut ((n+m)*p = n*p + m*p)
+  [ // ] #EQ whd in match (S n + m); whd in match (S ? * ?);
+  whd in match (S n * ?); >EQ in ⊢ (%→?%%??→?%%??); -EQ
+  #V #EQ >EQ -V @sym_jmeq @vector_associative_append
+]
+qed.
+
+lemma eq_v_vflatten : ∀A,n,m,test,v1,v2.
+  eq_v A ? test (vflatten A n m v1) (vflatten A n m v2) =
+  eq_v ?? (eq_v … test) v1 v2.
+#A #n #m #test #v1 elim v1 -n
+[ #v2 >(Vector_O … v2) % ]
+#n #hd #tl #IH #v2
+elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
+whd in ⊢ (??(????%%)%);
+whd in match (head' ???);
+whd in match (tail ???);
+>eq_v_append >IH %
+qed.
+
+lemma vprefix_vflatten : ∀A,n,m,p,test.∀v1,v2.
+  vprefix ? n m (eq_v ? p test) v1 v2 →
+  bool_to_Prop (vprefix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
+#A #n #m #p #test #v1 #v2 #G
+elim (vprefix_ok … G) #le_nm
+* #pre * #post *
+lapply (vflatten_append … pre post)
+lapply (pre @@ post)
+<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
+#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
+lapply (vflatten A m p v2')
+cut (m*p = n*p + (m-n)*p)
+[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
+  <distributive_times_plus <(minus_to_plus … le_nm (refl …)) % ]
+#EQ >EQ #v2' #EQ' >EQ' -v2' -v2'
+#G @vprefix_true
+>eq_v_vflatten @G
+qed.
+
+lemma vsuffix_vflatten : ∀A,n,m,p,test.∀v1,v2.
+  vsuffix ? n m (eq_v ? p test) v1 v2 →
+  bool_to_Prop (vsuffix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
+#A #n #m #p #test #v1 #v2 #G
+elim (vsuffix_ok … G) #le_nm * #pre * #post * 
+lapply (vflatten_append … pre post)
+lapply (pre @@ post)
+>commutative_plus in ⊢ (%→?%%??→???%%→?);
+<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
+#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
+lapply (vflatten A m p v2')
+cut (m*p = (m-n)*p + n*p)
+[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
+  <distributive_times_plus <commutative_plus <(minus_to_plus … le_nm (refl …)) % ]
+#EQ >EQ #v2' #EQ' >EQ'
+#G @vsuffix_true
+>eq_v_vflatten @G
+qed.