From 01d83fcfb40d3f6cae6b3fd83ae7eeac25c7bd15 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Mon, 29 Jun 2020 20:51:46 +0200
Subject: Remove invalid axiom (see #71)

---
 src/versions/standard/Array/PArray_standard.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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.
+*)
 
 
 (* 
-- 
cgit