Coq: precise generic vectors

(probably still some pattern matching to do, but I don't think the models
use that)

2 files changed, 188 insertions, 5 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index db0339d8..ee193865 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -124,9 +124,29 @@ Fixpoint repeat' {a} (xs : list a) n :=
   | O => []
   | S n => xs ++ repeat' xs n
   end.
+Lemma repeat'_length {a} {xs : list a} {n : nat} : List.length (repeat' xs n) = (n * List.length xs)%nat.
+induction n.
+* reflexivity.
+* simpl.
+  rewrite app_length.
+  auto with arith.
+Qed.
 Definition repeat {a} (xs : list a) (n : Z) :=
   if n <=? 0 then []
   else repeat' xs (Z.to_nat n).
+Lemma repeat_length {a} {xs : list a} {n : Z} (H : n >= 0) : length_list (repeat xs n) = n * length_list xs.
+unfold length_list, repeat.
+destruct n.
++ reflexivity. 
++ simpl (List.length _).
+  rewrite repeat'_length.
+  rewrite Nat2Z.inj_mul.
+  rewrite positive_nat_Z.
+  reflexivity.  
++ exfalso.
+  auto with zarith.
+Qed.
+
 (*declare {isabelle} termination_argument repeat = automatic
 
 Definition duplicate_to_list bit length := repeat [bit] length
@@ -187,6 +207,32 @@ lemma just_list_spec:
   ((forall xs. (just_list xs = None) <-> List.elem None xs) &&
    (forall xs es. (just_list xs = Some es) <-> (xs = List.map Some es)))*)
 
+Lemma just_list_length {A} : forall (l : list (option A)) (l' : list A),
+  Some l' = just_list l -> List.length l = List.length l'.
+induction l.
+* intros.
+  simpl in H.
+  inversion H.
+  reflexivity.
+* intros.
+  destruct a; simplify_eq H.
+  simpl in *.
+  destruct (just_list l); simplify_eq H.
+  intros.
+  subst.
+  simpl.
+  f_equal.
+  apply IHl.
+  reflexivity.
+Qed.
+
+Lemma just_list_length_Z {A} : forall (l : list (option A)) l', Some l' = just_list l -> length_list l = length_list l'.
+unfold length_list.
+intros.
+f_equal.
+auto using just_list_length.
+Qed.
+
 (*** Bits *)
 Inductive bitU := B0 | B1 | BU.
 
@@ -641,10 +687,10 @@ Definition update_list {A} (is_inc : bool) (xs : list A) n x :=
   | [] => failwith "extract_only_element called for empty list"
   | [e] => e
   | _ => failwith "extract_only_element called for list with more elements"
-end
+end*)
 
 (*** Machine words *)
-*)
+
 Definition mword (n : Z) :=
   match n with
   | Zneg _ => False
@@ -1272,6 +1318,38 @@ Definition index_list from to step :=
     index_list' from to step (S (Z.abs_nat (from - to)))
   else [].
 
+Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Vars) : Vars :=
+  if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then
+    match n with
+    | O => vars
+    | S n => let vars := body from vars in foreach_Z' (from + step) to step n vars body
+    end
+  else vars.
+
+Definition foreach_Z {Vars} from to step vars body :=
+  foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body.
+
+Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (from <= to)} `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> Vars) {struct n} : Vars :=
+  if sumbool_of_bool (from + off <=? to) then
+    match n with
+    | O => vars
+    | S n => let vars := body (from + off) _ vars in foreach_Z_up' from to step (off + step) n vars body
+    end
+  else vars.
+
+Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (to <= from)} `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> Vars) {struct n} : Vars :=
+  if sumbool_of_bool (to <=? from + off) then
+    match n with
+    | O => vars
+    | S n => let vars := body (from + off) _ vars in foreach_Z_down' from to step (off - step) n vars body
+    end
+  else vars.
+
+Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (from <= to)} `{ArithFact (0 < step)} :=
+    foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (to <= from)} `{ArithFact (0 < step)} :=
+    foreach_Z_down' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+
 (*val while : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars
 Fixpoint while vars cond body :=
   if cond vars then while (body vars) cond body else vars
@@ -1385,3 +1463,108 @@ Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c <=
 Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c >= a /\ c >= b)} :=
   build_ex (Z.max a b).
 
+
+(*** Generic vectors *)
+
+Definition vec (T:Type) (n:Z) := { l : list T & length_list l = n }.
+Definition vec_length {T n} (v : vec T n) := n.
+Definition vec_access_dec {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+  access_list_dec (projT1 v) m.
+Definition vec_access_inc {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+  access_list_inc (projT1 v) m.
+
+Program Definition vec_init {T} (t : T) (n : Z) `{ArithFact (n >= 0)} : vec T n :=
+  existT _ (repeat [t] n) _.
+Next Obligation.
+rewrite repeat_length; auto using fact.
+unfold length_list.
+simpl.
+auto with zarith.
+Qed.
+
+Lemma skipn_length {A n} {l: list A} : (n <= List.length l -> List.length (skipn n l) = List.length l - n)%nat.
+revert l.
+induction n.
+* simpl. auto with arith.
+* intros l H.
+  destruct l.
+  + inversion H.
+  + simpl in H.
+    simpl.
+    rewrite IHn; auto with arith.
+Qed.
+Lemma update_list_inc_length {T} {l:list T} {m x} : 0 <= m < length_list l -> length_list (update_list_inc l m x) = length_list l.
+unfold update_list_inc, list_update, length_list.
+intro H.
+f_equal.
+assert ((0 <= Z.to_nat m < Datatypes.length l)%nat).
+{ destruct H as [H1 H2].
+  split.
+  + change 0%nat with (Z.to_nat 0).
+    apply Z2Nat.inj_le; auto with zarith.
+  + rewrite <- Nat2Z.id.
+    apply Z2Nat.inj_lt; auto with zarith.
+}
+rewrite app_length.
+rewrite firstn_length_le; only 2:omega.
+cbn -[skipn].
+rewrite skipn_length;
+omega.
+Qed.
+
+Program Definition vec_update_dec {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_dec (projT1 v) m t) _.
+Next Obligation.
+unfold update_list_dec.
+rewrite update_list_inc_length.
++ destruct v. apply e.
++ destruct H.
+  destruct v. simpl (projT1 _). rewrite e.
+  omega.
+Qed.
+
+Program Definition vec_update_inc {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_inc (projT1 v) m t) _.
+Next Obligation.
+rewrite update_list_inc_length.
++ destruct v. apply e.
++ destruct H.
+  destruct v. simpl (projT1 _). rewrite e.
+  omega.
+Qed.
+
+Program Definition vec_map {S T} (f : S -> T) {n} (v : vec S n) : vec T n := existT _ (List.map f (projT1 v)) _.
+Next Obligation.
+destruct v as [l H].
+cbn.
+unfold length_list.
+rewrite map_length.
+apply H.
+Qed.
+
+Program Definition just_vec {A n} (v : vec (option A) n) : option (vec A n) :=
+  match just_list (projT1 v) with
+  | None => None
+  | Some v' => Some (existT _ v' _)
+  end.
+Next Obligation.
+rewrite <- (just_list_length_Z _ _ Heq_anonymous).
+destruct v.
+assumption.
+Qed.
+
+Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v.
+
+Program Definition vec_of_list {A} n (l : list A) : option (vec A n) :=
+  if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None.
+Next Obligation.
+symmetry.
+apply Z.eqb_eq.
+assumption.
+Qed.
+
+Definition vec_of_list_len {A} (l : list A) : vec A (length_list l) := existT _ l (eq_refl _).
+
+Definition map_bind {A B} (f : A -> option B) (a : option A) : option B :=
+match a with
+| Some a' => f a'
+| None => None
+end.
\ No newline at end of file
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 86bbe601..8abcd218 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -22,7 +22,7 @@ val vector_length = {
   ocaml: "length",
   lem: "length_list",
   c: "length",
-  coq: "length_list"
+  coq: "vec_length"
 } : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
 
 overload length = {bitvector_length, vector_length}
@@ -68,7 +68,7 @@ val bitvector_access = {
 val plain_vector_access = {
   ocaml: "access",
   lem: "access_list_dec",
-  coq: "access_list_dec",
+  coq: "vec_access_dec",
   c: "vector_access"
 } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
 
@@ -84,7 +84,7 @@ val bitvector_update = {
 val plain_vector_update = {
   ocaml: "update",
   lem: "update_list_dec",
-  coq: "update_list_dec",
+  coq: "vec_update_dec",
   c: "vector_update"
 } : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)