saw-core-coq: Give proper definitions to genWithProof and atWithProof

[RyanGlScott]

When generating Coq code, Heapster frequently translates array updates to code involving updBVVec and repeatBVVec. These, in turn, are defined in terms of the genWithProof and atWithProof axioms. Because these are axioms, they do not reduce in Coq, which makes them more difficult to use in practice. There isn't any good reason for them to be axioms on the Coq side, however, as we can define them relatively easily. Something like this should suffice:

Program Fixpoint
  genWithProof
    (n : nat)
    (a : Type) :
    (forall (i : nat), IsLtNat i n -> a) -> Vec n a :=
  match n as n' return (forall (i : nat), IsLtNat i n' -> a) -> Vec n' a with
  | O   => fun _ => VectorDef.nil a
  | S m => fun f => VectorDef.cons a (f 0 _) m (genWithProof' m a (fun i prf => f (S i) _))
  end.
Next Obligation.
  apply le_n_S. apply le_0_n.
Qed.
Next Obligation.
  apply le_n_S. exact prf.
Qed.

Program Fixpoint
  atWithProof
    (n : nat)
    (a : Type)
    (v : Vec n a)
    (i : nat) :
    IsLtNat i n -> a :=
  match i as i', n as n' return Vec n' a -> IsLtNat i' n' -> a with
  | _,   O   => fun _ prf =>
                match Nat.nlt_0_r _ prf with end
  | O,   S y => fun v' prf => VectorDef.hd v'
  | S x, S y => fun v' prf => atWithProof' y a (VectorDef.tl v') x _
  end v.
Next Obligation.
  apply le_S_n. exact prf.
Qed.

[eddywestbrook]

Yep, these both seem reasonable. Except you might want to use Defined instead of Qed if you want them to reduce.