Library Stdlib.Array.PArray

From Stdlib Require Import Uint63.
From Stdlib Require Export PrimArray ArrayAxioms.

Local Open Scope uint63_scope.
Local Open Scope array_scope.

Notation array := PrimArray.array (only parsing).
Notation make := PrimArray.make (only parsing).
Notation get := PrimArray.get (only parsing).
Notation default := PrimArray.default (only parsing).
Notation set := PrimArray.set (only parsing).
Notation length := PrimArray.length (only parsing).
Notation copy := PrimArray.copy (only parsing).

Notation max_length := PrimArray.max_length (only parsing).

Notation get_out_of_bounds := ArrayAxioms.get_out_of_bounds (only parsing).
Notation get_set_same := ArrayAxioms.get_set_same (only parsing).
Notation get_set_other := ArrayAxioms.get_set_other (only parsing).
Notation default_set := ArrayAxioms.default_set (only parsing).
Notation get_make := ArrayAxioms.get_make (only parsing).
Notation leb_length := ArrayAxioms.leb_length (only parsing).
Notation length_make := ArrayAxioms.length_make (only parsing).
Notation length_set := ArrayAxioms.length_set (only parsing).
Notation get_copy := ArrayAxioms.get_copy (only parsing).
Notation length_copy := ArrayAxioms.length_copy (only parsing).
Notation array_ext := ArrayAxioms.array_ext (only parsing).


Lemma default_copy A (t:array A) : default (copy t) = default t.

Lemma default_make A (a : A) size : default (make size a) = a.

Lemma get_set_same_default A (t : array A) (i : int) :
  t.[i <- default t].[i] = default t.

Lemma get_not_default_lt A (t:array A) x :
 t.[x] <> default t -> (x <? length t) = true.