[guru-lang] r526 committed - Added some lemmas which will be used to prove _heap_parent_lem1.

[guru...@googlecode.com]

Revision: 526
Author: kevinclancy0
Date: Wed Jul 27 10:47:09 2011
Log: Added some lemmas which will be used to prove _heap_parent_lem1.
http://code.google.com/p/guru-lang/source/detail?r=526

Modified:
/branches/1.0/lib/bv.g
/branches/1.0/lib/pow.g
/branches/1.0/lib/vec.g
/branches/1.0/lib/word.g

=======================================
--- /branches/1.0/lib/bv.g Mon Jun 27 11:27:55 2011
+++ /branches/1.0/lib/bv.g Wed Jul 27 10:47:09 2011
@@ -1102,3 +1102,200 @@
| S l' => hypjoin (bv_dec (mkvec ff l)) (mk_bv_dec_t ff (mkvec ff l)) by
l_eq [l_IH l'] end
end.

+Define bv_tail_le :
+ Forall(n: nat)(l: <bv (S n)>).
+ { (le (to_nat (bv_tail l)) (to_nat l)) = tt }
+ :=
+ induction(n: nat)(l: <bv (S n)>)
+ return { (le (to_nat (bv_tail l)) (to_nat l)) = tt }
+ with
+ | vecn _ =>
+ contra
+ trans
+ inj <bv *> l_Eq
+ clash (S n) Z
+
+ { (le (to_nat (bv_tail l)) (to_nat l)) = tt }
+ | vecc _ n' a l' =>
+ abbrev nat_l = (to_nat (S n) l) in
+ abbrev nat_tail_l = (to_nat n (bv_tail n l)) in
+ % { (le nat_tail_l (mult2 nat_tail_l)) = tt }
+ abbrev p0 =
+ % { (le nat_tail_l (mult nat_tail_l two)) = tt }
+ abbrev p00 =
+ [mult_le
+ nat_tail_l
+ two
+ clash two Z
+ ]
+ in
+ % { (le (mult two nat_tail_l) (mult nat_tail_l two)) = tt }
+ abbrev p01 =
+ [eq_le
+ (mult nat_tail_l two)
+ (mult two nat_tail_l)
+ [mult_comm
+ nat_tail_l
+ two
+ ]
+ ]
+ in
+ [le_trans
+ nat_tail_l
+ (mult nat_tail_l two)
+ (mult two nat_tail_l)
+ p00
+ p01
+ ]
+ in
+ % { (le (mult2 nat_tail_l) (condS a (mult2 nat_tail_l))) = tt }
+ abbrev p1 = [condS_le a (mult2 nat_tail_l)] in
+ % { (le nat_tail_l (condS a (mult2 nat_tail_l))) = tt }
+ abbrev p2 =
+ [le_trans
+ nat_tail_l
+ (mult2 nat_tail_l)
+ (condS a (mult2 nat_tail_l))
+ p0
+ p1
+ ]
+ in
+ % { (le (condS a (mult2 nat_tail_l)) (to_nat l)) = tt }
+ abbrev p3 =
+ abbrev p30 =
+ hypjoin (condS a (mult2 nat_tail_l)) nat_l by
+ l_eq
+ end
+ in
+ [eq_le
+ (condS a (mult2 nat_tail_l))
+ nat_l
+ p30
+ ]
+ in
+ [le_trans
+ nat_tail_l
+ (condS a (mult2 nat_tail_l))
+ nat_l
+ p2
+ p3
+ ]
+ end.
+
+Define bv_shift_le :
+ Forall(x n : nat)(l: <bv (S n)>).
+ { (le (to_nat (bv_shift x l)) (to_nat l)) = tt }
+ :=
+ induction(x : nat)
+ return
+ Forall(n: nat)(l: <bv (S n)>).
+ { (le (to_nat (bv_shift x l)) (to_nat l)) = tt }
+ with
+ | Z =>
+ foralli(n: nat)(l: <bv (S n)>).
+ [eq_le
+ (to_nat (S n) (bv_shift x n l))
+ (to_nat (S n) l)
+ hypjoin (to_nat (bv_shift x l)) (to_nat l) by x_eq end
+ ]
+ | S x' =>
+ foralli(n: nat)(l: <bv (S n)>).
+ case l with
+ | vecn _ =>
+ contra
+ trans
+ l_Eq
+ clash Z (S n)
+
+ { (le (to_nat (bv_shift x l)) (to_nat l)) = tt }
+ | vecc _ n' a l' =>
+ abbrev shifted_once =
+ cast
+ (bv_append
+ n
+ (S Z)
+ (bv_tail n l)
+ (bvc Z ff bvn)
+ )
+ by
+ cong <bv *>
+ trans [plusS n Z]
+ cong (S *) [plusZ n]
+ in
+ % { (to_nat (bv_shift x l)) = (to_nat (bv_shift x'
shifted_once)) }
+ abbrev p0 =
+ abbrev so_erased =
+ (vec_append (vec_tail l) (vecc ff vecn))
+ in
+ hypjoin
+ (to_nat (bv_shift x l))
+ (to_nat (bv_shift x' so_erased))
+ by
+ x_eq
+ end
+ in
+ % { (le (to_nat (bv_shift x l)) (to_nat (bv_shift x'
shifted_once)) = tt }
+ abbrev p1 =
+ [eq_le
+ (to_nat (S n) (bv_shift x n l))
+ (to_nat (S n) (bv_shift x' n shifted_once))
+ p0
+ ]
+ in
+ % { (le (to_nat (bv_shift x l)) (to_nat shifted_once)) = tt }
+ abbrev p2 =
+ [le_trans
+ (to_nat (S n) (bv_shift x n l))
+ (to_nat (S n) (bv_shift x' n shifted_once))
+ (to_nat (S n) shifted_once)
+ p1
+ [x_IH x' n shifted_once]
+ ]
+ in
+ % { (to_nat shifted_once) = (plus (to_nat (bv_tail n l) (mult
(pow2 n (to_nat (bvc Z ff bvn))) }
+ abbrev p3 =
+ [to_nat_append
+ n
+ one
+ (bv_tail n l)
+ (bvc Z ff bvn)
+ ]
+ in
+ % { (to_nat shifted_once) = (to_nat (bv_tail l)) }
+ abbrev p4 =
+ abbrev z =
+ hypjoin (mult (pow2 n) (to_nat (vecc ff vecn))) Z by
+ [multZ (pow2 n)]
+ end
+ in
+ transs
+ p3
+ cong (plus (to_nat (bv_tail l)) *) z
+ [plusZ (to_nat n (bv_tail n l))]
+ end
+ in
+ % { (le (to_nat shifted_once) (to_nat l)) = tt }
+ abbrev one_shift_decreases =
+ [le_trans
+ (to_nat (S n) shifted_once)
+ (to_nat n (bv_tail n l))
+ (to_nat (S n) l)
+ [eq_le
+ (to_nat (S n) shifted_once)
+ (to_nat n (bv_tail n l))
+ p4
+ ]
+ [bv_tail_le n l]
+ ]
+ in
+ [le_trans
+ (to_nat (S n) (bv_shift x n l))
+ (to_nat (S n) shifted_once)
+ (to_nat (S n) l)
+ p2
+ one_shift_decreases
+ ]
+ end
+ end.
+
+
=======================================
--- /branches/1.0/lib/pow.g Mon Apr 18 10:44:45 2011
+++ /branches/1.0/lib/pow.g Wed Jul 27 10:47:09 2011
@@ -369,6 +369,31 @@

Total condS condS_tot.

+Define condS_le :
+ Forall(b: bool)(n: nat). { (le n (condS b n)) = tt }
+ :=
+ foralli(b: bool)(n: nat).
+ case b with
+ | ff =>
+ [eq_le
+ n
+ (condS b n)
+ hypjoin n (condS b n) by b_eq end
+ ]
+ | tt =>
+ [le_trans
+ n
+ (S n)
+ (condS b n)
+ [le_S n]
+ [eq_le
+ (S n)
+ (condS b n)
+ hypjoin (S n) (condS b n) by b_eq end
+ ]
+ ]
+ end.
+
Define condS_Z1 : Forall(b:bool)(n:nat)(u:{(condS b n) = Z}).{b = ff} :=
induction(b:bool) by ub ign ign
return Forall(n:nat)(u:{(condS b n) = Z}).{b = ff} with
=======================================
--- /branches/1.0/lib/vec.g Thu Jul 21 10:41:57 2011
+++ /branches/1.0/lib/vec.g Wed Jul 27 10:47:09 2011
@@ -329,6 +329,40 @@
| vecc _ _ _ l' => cast l' by refl <vec A n>
end.

+Define vec_tail_tot :
+ Forall(A:type)(n:nat)(l:<vec A (S n)>).
+ Exists(l':<vec A n>). { (vec_tail l) = l' }
+ :=
+ foralli(A:type)(n: nat)(l: <vec A (S n)>).
+ case l with
+ | vecn _ =>
+ contra
+ trans l_Eq
+ clash Z (S n)
+
+ Exists(l': <vec A n>). { (vec_tail l) = l' }
+ | vecc B m _ rest =>
+ % { <vec B (S m)> = <vec A (S n)> }
+ abbrev casted_rest =
+ abbrev n_eq_m =
+ inj <vec ** (S *)> l_Eq
+ in
+ abbrev A_eq_B =
+ inj <vec * **> l_Eq
+ in
+
+ cast rest by
+ trans
+ cong <vec A *> symm n_eq_m
+ cong <vec * n> symm A_eq_B
+ in
+ existsi casted_rest
+ { (vec_tail l) = * }
+ hypjoin (vec_tail l) rest by l_eq end
+ end.
+
+Total vec_tail vec_tail_tot.
+
Define vec_append_assoc : Forall(A:type)(n1 : nat)(l1 : <vec A n1>)
(n2 n3 : nat)(l2 : <vec A n2>)(l3 : <vec A n3>).
{ (vec_append (vec_append l1 l2) l3) =
=======================================
--- /branches/1.0/lib/word.g Thu Jul 21 10:41:57 2011
+++ /branches/1.0/lib/word.g Wed Jul 27 10:47:09 2011
@@ -4,7 +4,8 @@

% Set "trust_hypjoins".

-Define wordlen := (mult2 (mult2 (S (S (S (S (S (S (S (S Z)))))))))).
+Define wordlen_pred := (S (mult five six))
+Define wordlen := (S wordlen_pred).

Define primitive word := <bv wordlen> <<END
#define gdelete_word(x)
@@ -82,24 +83,7 @@
Define wordlen_neq_Z :
{ wordlen != Z }
:=
- abbrev sixteen = (mult two eight) in
- abbrev sixteen_not_Z =
- [mult_not_zero
- two
- eight
- clash two Z
- clash eight Z
- ]
- in
- transs
- join wordlen (mult two sixteen)
- [mult_not_zero
- two
- sixteen
- clash two Z
- sixteen_not_Z
- ]
- end.
+ clash (S wordlen_pred) Z.

%=============================================================================
% word and nat