diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-29 20:51:46 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-29 20:51:46 +0200 |
| commit | 01d83fcfb40d3f6cae6b3fd83ae7eeac25c7bd15 (patch) | |
| tree | 3954fbf088dd6f7f3ac313002d26614ce9075edc /src/versions/standard/Array/PArray_standard.v | |
| parent | 2c553f5537e9bbcceaf488ad164d6178476fb017 (diff) | |
| download | smtcoq-01d83fcfb40d3f6cae6b3fd83ae7eeac25c7bd15.tar.gz smtcoq-01d83fcfb40d3f6cae6b3fd83ae7eeac25c7bd15.zip | |
Remove invalid axiom (see #71)
Diffstat (limited to 'src/versions/standard/Array/PArray_standard.v')
| -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 e116339..83bc943 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -110,12 +110,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) := @@ -364,6 +366,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). @@ -383,6 +386,7 @@ Proof. intros i _; rewrite <- (reflect_iff _ _ (HA _ _));trivial. rewrite <- not_true_iff_false, <- (reflect_iff _ _ (HA _ _)) in H0;apply H0;trivial. Qed. +*) (* |