Module ...lib.coq.WhyArrays

``` Require Export WhyInt. Implicit Arguments On. Parameter raw_array : Set -> Set. Definition array [T:Set] := Z * (raw_array T). Definition array_length : (T:Set)(array T) -> Z :=   [T:Set; t:(array T)]let (n, _) = t in n. Parameter raw_new : (T:Set) T -> (raw_array T). Definition new : (T:Set) Z -> T -> (array T) :=   [T:Set; n:Z; a:T](n, (raw_new a)). Parameter raw_access : (T:Set) (raw_array T) -> Z -> T. Definition access : (T:Set) (array T) -> Z -> T :=   [T:Set; t:(array T); i:Z]let (_, r) = t in (raw_access r i). Parameter raw_store : (T:Set) (raw_array T) -> Z -> T -> (raw_array T). Definition store : (T:Set) (array T) -> Z -> T -> (array T) :=   [T:Set; t:(array T); i:Z; v:T]   ((array_length t), let (_, r) = t in (raw_store r i v)). Lemma array_length_store :   (T:Set)(t:(array T))(i:Z)(v:T)   (array_length (store t i v)) = (array_length t). Proof. Trivial. Save. Axiom new_def : (T:Set)(n:Z)(v0:T)                 (i:Z) `0 <= i < n` -> (access (new n v0) i) = v0. Axiom store_def_1 : (T:Set)(t:(array T))(v:T)                     (i:Z) `0 <=i < (array_length t)` ->                     (access (store t i v) i) = v. Axiom store_def_2 : (T:Set)(t:(array T))(v:T)                     (i:Z)(j:Z)                     `0 <= i < (array_length t)` ->                     `0 <= j < (array_length t)` ->                     `i <> j` ->                     (access (store t i v) j) = (access t j). Hints Resolve new_def store_def_1 store_def_2 : datatypes v62. Tactic Definition WhyArrays :=   Repeat Rewrite store_def_1;   Repeat Rewrite array_length_store. Tactic Definition AccessStore i j H :=   Elim (Z_eq_dec i j); [     Intro H; Rewrite H; Rewrite store_def_1; WhyArrays   | Intro H; Rewrite store_def_2;              [ Idtac | Idtac | Idtac | Exact H ] ]. Tactic Definition AccessSame :=   Rewrite store_def_1; WhyArrays; Try Omega. Tactic Definition AccessOther :=   Rewrite store_def_2; WhyArrays; Try Omega. Tactic Definition ArraySubst t :=   Subst t; Simpl; WhyArrays; Try Omega. Grammar constr constr0 :=   array_access     [ "#" ident(\$t) "[" constr(\$c) "]" ] -> [ (access \$t \$c) ]. ```

``` ```

Index