Changeset 905 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 8, 2011, 6:07:20 PM (10 years ago)

Author:

mulligan

Message:

work from today

File:

• src/ASM/AssemblyProof.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -48 +48 @@
 
 (* END RUSSELL **)
+
+
+definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
+  λP.
+    P true ∧ P false.
+ 
+let rec bitvector_elim_prop_internal
+  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
+  match m return λm. m ≤ n → BitVector (n - m) → Prop with
+  [ O    ⇒ λprf1. λprefix. P ?
+  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
+  ].
+  [ applyS prefix
+  | letin res ≝ (bit ::: prefix)
+    < (minus_S_S ? ?)
+    > (minus_Sn_m ? ?)
+  [ @ res
+  | @ prf2
+  ]
+  | /2/
+  ].
+qed.
+
+definition bitvector_elim_prop ≝
+  λn: nat.
+  λP: BitVector n → Prop.
+    bitvector_elim_prop_internal n P n ? ?.
+  [ @ (le_n ?)
+  | < (minus_n_n ?)
+    @ [[ ]]
+  ]
+qed.
+
+lemma eq_b_eq:
+  ∀b, c.
+    eq_b b c = true → b = c.
+  #b #c
+  cases b
+  cases c
+  normalize //
+qed.
+
+lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
+ #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
+ #n #hd #tl #abs @⊥ //
+qed.
+
+lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
+ ∃hd.∃tl.v ≃ VCons bool n hd tl.
+ #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
+ [ #abs @⊥ //
+ | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
+qed.
+
+lemma eq_bv_eq:
+  ∀n, v, q.
+    eq_bv n v q = true → v = q.
+  #n #v #q generalize in match v
+  elim q
+  [ #v #h @BitVector_O
+  | #n #hd #tl #ih #v' #h
+    cases (BitVector_Sn ? v')
+    #hd' * #tl' #jmeq >jmeq in h;
+    #new_h
+    change in new_h with ((andb ? ?) = ?);
+    cases(conjunction_true … new_h)
+    #eq_heads #eq_tails
+    whd in eq_heads:(??(??(%))?);
+    cases(eq_b_eq … eq_heads)
+    whd in eq_tails:(??(?????(%))?);
+    change in eq_tails with (eq_bv ??? = ?);
+    <(ih tl') //
+  ]
+qed.
+
+lemma bool_eq_internal_eq:
+  ∀b, c.
+    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
+  #b #c
+  cases b
+  [ normalize //
+  | normalize
+    cases c
+    [ normalize //
+    | normalize //
+    ]
+  ]
+qed.
+
+lemma eq_bv_refl:
+  ∀n,v. eq_bv n v v = true.
+  #n #v
+  elim v
+  [ //
+  | #n #hd #tl #ih
+    normalize
+    cases hd
+    [ normalize
+      @ ih
+    | normalize
+      @ ih
+    ]
+  ]
+qed.
+
+lemma eq_eq_bv:
+  ∀n, v, q.
+    v = q → eq_bv n v q = true.
+  #n #v
+  elim v
+  [ #q #h <h normalize %
+  | #n #hd #tl #ih #q #h >h //
+  ]
+qed.
 
 let rec foldl_strong_internal
@@ -625 +739 @@
 qed.
 
-lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
- #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
- #n #hd #tl #abs @⊥ //
-qed.
-
-lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
- ∃hd.∃tl.v ≃ VCons bool n hd tl.
- #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
- [ #abs @⊥ //
- | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
-qed.
-
 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].