diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-29 20:56:51 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-29 20:56:51 +0200 |
commit | 22c6b47cd482534e5c789f2f367cff9a0d6ace64 (patch) | |
tree | 03fdab289071379e9f414bb4c944a07d38d08863 /src/versions/standard/Array | |
parent | 011ae52fbef03a4d0275ff4242ca44c4c1269201 (diff) | |
parent | 01d83fcfb40d3f6cae6b3fd83ae7eeac25c7bd15 (diff) | |
download | smtcoq-22c6b47cd482534e5c789f2f367cff9a0d6ace64.tar.gz smtcoq-22c6b47cd482534e5c789f2f367cff9a0d6ace64.zip |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11
Diffstat (limited to 'src/versions/standard/Array')
-rw-r--r-- | src/versions/standard/Array/PArray_standard.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index ee0dd96..99a7e65 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -112,12 +112,14 @@ Axiom get_init : forall A f size (def:A) i, Axiom default_init : forall A f size (def:A), default (init size f def) = def. -(* Rename this ? *) +(* Not true in this implementation (see #71, many thanks to Andres Erbsen) *) +(* Axiom get_ext : forall A (t1 t2:array A), length t1 = length t2 -> (forall i, i < length t1 = true -> t1.[i] = t2.[i]) -> default t1 = default t2 -> t1 = t2. +*) (* Definition *) Definition to_list {A:Type} (t:array A) := @@ -366,6 +368,7 @@ Definition eqb {A:Type} (Aeqb: A->A->bool) (t1 t2:array A) := Aeqb (default t1) (default t2) && forallbi (fun i a1 => Aeqb a1 (t2.[i])) t1. +(* Lemma reflect_eqb : forall (A:Type) (Aeqb:A->A->bool), (forall a1 a2, reflect (a1 = a2) (Aeqb a1 a2)) -> forall t1 t2, reflect (t1 = t2) (eqb Aeqb t1 t2). @@ -385,6 +388,7 @@ Proof. intros i _; rewrite <- (reflect_iff _ _ (HA _ _));trivial. rewrite <- not_true_iff_false, <- (reflect_iff _ _ (HA _ _)) in H0;apply H0;trivial. Qed. +*) (* |