diff options
Diffstat (limited to 'src/PArray/PArray.v')
| -rw-r--r-- | src/PArray/PArray.v | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/src/PArray/PArray.v b/src/PArray/PArray.v index 03f1abd..891db84 100644 --- a/src/PArray/PArray.v +++ b/src/PArray/PArray.v @@ -27,9 +27,9 @@ Module IntOrderedType <: OrderedType. Definition t := int. - Definition eq x y := (x == y) = true. + Definition eq x y := (x =? y) = true. - Definition lt x y := (x < y) = true. + Definition lt x y := (x <? y) = true. Lemma eq_refl x : eq x x. Proof. unfold eq. rewrite eqb_spec. reflexivity. Qed. @@ -48,9 +48,9 @@ Module IntOrderedType <: OrderedType. Definition compare x y : Compare lt eq x y. Proof. - case_eq (x < y); intro e. + case_eq (x <? y); intro e. exact (LT e). - case_eq (x == y); intro e2. + case_eq (x =? y); intro e2. exact (EQ e2). apply GT. unfold lt. rewrite <- Bool.not_false_iff_true, <- Bool.not_true_iff_false, ltb_spec, eqb_spec in *; intro e3. @@ -59,7 +59,7 @@ Module IntOrderedType <: OrderedType. Definition eq_dec x y : { eq x y } + { ~ eq x y }. Proof. - case_eq (x == y); intro e. + case_eq (x =? y); intro e. left; exact e. right. intro H. rewrite H in e. discriminate. Defined. @@ -78,7 +78,7 @@ Definition make {A:Type} (l:int) (d:A) : array A := (Map.empty A, d, l). Definition get {A:Type} (t:array A) (i:int) : A := let (td, l) := t in let (t, d) := td in - if i < l then + if i <? l then match Map.find i t with | Some x => x | None => d @@ -90,7 +90,7 @@ Definition default {A:Type} (t:array A) : A := Definition set {A:Type} (t:array A) (i:int) (a:A) : array A := let (td,l) := t in - if l <= i then + if l <=? i then t else let (t,d) := td in @@ -115,14 +115,14 @@ Definition max_length := max_int. Require FSets.FMapFacts. Module P := FSets.FMapFacts.WProperties_fun IntOrderedType Map. -Lemma get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t. +Lemma get_outofbound : forall A (t:array A) i, (i <? length t) = false -> t.[i] = default t. intros A t i; unfold get. destruct t as ((t, d), l). unfold length; intro Hi; rewrite Hi; clear Hi. reflexivity. Qed. -Lemma get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. +Lemma get_set_same : forall A t i (a:A), (i <? length t) = true -> t.[i<-a].[i] = a. intros A t i a. destruct t as ((t, d), l). unfold set, get, length. @@ -143,7 +143,7 @@ Lemma get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. intros A t i j a Hij. destruct t as ((t, d), l). unfold set, get, length. -case (l <= i). +case (l <=? i). reflexivity. rewrite P.F.add_neq_o. reflexivity. @@ -156,17 +156,17 @@ Lemma default_set : forall A t i (a:A), default (t.[i<-a]) = default t. intros A t i a. destruct t as ((t, d), l). unfold default, set. -case (l <= i); reflexivity. +case (l <=? i); reflexivity. Qed. Lemma get_make : forall A (a:A) size i, (make size a).[i] = a. intros A a size i. unfold make, get. rewrite P.F.empty_o. -case (i < size); reflexivity. +case (i <? size); reflexivity. Qed. -Lemma leb_length : forall A (t:array A), length t <= max_length = true. +Lemma leb_length : forall A (t:array A), length t <=? max_length = true. intros A t. generalize (length t); clear t. intro i. @@ -177,10 +177,10 @@ apply to_Z_bounded. Qed. Lemma length_make : forall A size (a:A), - length (make size a) = if size <= max_length then size else max_length. + length (make size a) = if size <=? max_length then size else max_length. intros A size a. unfold length, make. -replace (size <= max_length) with true. +replace (size <=? max_length) with true. reflexivity. symmetry. rewrite leb_spec. @@ -194,7 +194,7 @@ Lemma length_set : forall A t i (a:A), intros A t i a. destruct t as ((t, d), l). unfold length, set. -case (l <= i); reflexivity. +case (l <=? i); reflexivity. Qed. Lemma get_copy : forall A (t:array A) i, (copy t).[i] = t.[i]. @@ -211,7 +211,7 @@ Qed. (* Axiom array_ext : forall A (t1 t2:array A), length t1 = length t2 -> - (forall i, i < length t1 = true -> t1.[i] = t2.[i]) -> + (forall i, i <? length t1 = true -> t1.[i] = t2.[i]) -> default t1 = default t2 -> t1 = t2. *) @@ -229,7 +229,7 @@ Qed. Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t. unfold default, get, set. destruct t as ((t, d), l). -case_eq (i < l). +case_eq (i <? l). intro H; generalize H. rewrite ltb_spec. rewrite Z.lt_nge. @@ -252,10 +252,10 @@ reflexivity. Qed. Lemma get_not_default_lt A (t:array A) x : - t.[x] <> default t -> (x < length t) = true. + t.[x] <> default t -> (x <? length t) = true. unfold get, default, length. destruct t as ((t, d), l). -case (x < l); tauto. +case (x <? l); tauto. Qed. (* |