diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-29 20:52:58 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-29 20:52:58 +0200 |
| commit | 64645357edd12bcd3b1d1b5735b7226e89d2a623 (patch) | |
| tree | f498b473c543b33f96855107264ec74b8e2ddb67 | |
| parent | 7399f3a30bd1685b9573f1ab1dc6b516590fe8e5 (diff) | |
| parent | 01d83fcfb40d3f6cae6b3fd83ae7eeac25c7bd15 (diff) | |
| download | smtcoq-64645357edd12bcd3b1d1b5735b7226e89d2a623.tar.gz smtcoq-64645357edd12bcd3b1d1b5735b7226e89d2a623.zip | |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
| -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. +*) (* |