Commit e4542668 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Use List.repeat from Coq's standard library instead of list_repeat

parent 7563a5df
......@@ -737,7 +737,7 @@ Lemma store_argument_sound:
Proof.
intros.
assert (UNDEF: list_forall2 memval_lessdef
(list_repeat (size_chunk_nat chunk) Undef)
(List.repeat Undef (size_chunk_nat chunk))
(encode_val chunk w)).
{
rewrite <- (encode_val_length chunk w).
......
......@@ -887,7 +887,7 @@ Qed.
Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
forall p n,
ofs <= p -> p + Z.of_nat n <= ofs + len ->
Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)).
Mem.loadbytes m b p (Z.of_nat n) = Some (List.repeat (Byte Byte.zero) n).
Lemma store_zeros_loadbytes:
forall m b p n m',
......@@ -901,8 +901,8 @@ Proof.
+ subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. lia.
rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ.
replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by lia.
change (list_repeat (S n0) (Byte Byte.zero))
with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)).
change (List.repeat (Byte Byte.zero) (S n0))
with ((Byte Byte.zero :: nil) ++ List.repeat (Byte Byte.zero) n0).
apply Mem.loadbytes_concat.
eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p).
eapply store_zeros_unchanged; eauto. intros; lia.
......@@ -924,11 +924,11 @@ Definition bytes_of_init_data (i: init_data): list memval :=
| Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n))
| Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
| Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
| Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero)
| Init_space n => List.repeat (Byte Byte.zero) (Z.to_nat n)
| Init_addrof id ofs =>
match find_symbol ge id with
| Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs)
| None => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef
| None => List.repeat Undef (if Archi.ptr64 then 8%nat else 4%nat)
end
end.
......@@ -1020,7 +1020,7 @@ Lemma store_zeros_read_as_zero:
read_as_zero m' b p n.
Proof.
intros; red; intros.
transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))).
transitivity (Some(decode_val chunk (List.repeat (Byte Byte.zero) (size_chunk_nat chunk)))).
apply Mem.loadbytes_load; auto. rewrite size_chunk_conv.
eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto.
f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity.
......
......@@ -371,14 +371,14 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
| Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n))
| Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n))
| Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
| Vptr b ofs, Mint32 => if Archi.ptr64 then list_repeat 4%nat Undef else inj_value Q32 v
| Vptr b ofs, Mint32 => if Archi.ptr64 then List.repeat Undef 4%nat else inj_value Q32 v
| Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
| Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else list_repeat 8%nat Undef
| Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else List.repeat Undef 8%nat
| Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
| Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
| _, Many32 => inj_value Q32 v
| _, Many64 => inj_value Q64 v
| _, _ => list_repeat (size_chunk_nat chunk) Undef
| _, _ => List.repeat Undef (size_chunk_nat chunk)
end.
Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
......@@ -674,10 +674,10 @@ Local Transparent inj_value.
constructor; auto. unfold inj_bytes; intros. exploit list_in_map_inv; eauto.
intros (b & P & Q); exists b; auto.
}
assert (D: shape_encoding chunk v (list_repeat (size_chunk_nat chunk) Undef)).
assert (D: shape_encoding chunk v (List.repeat Undef (size_chunk_nat chunk))).
{
intros. rewrite EQ; simpl; constructor; auto.
intros. eapply in_list_repeat; eauto.
intros. eapply repeat_spec; eauto.
}
generalize (encode_val_length chunk v). intros LEN.
unfold encode_val; unfold encode_val in LEN;
......@@ -882,21 +882,21 @@ Qed.
Lemma repeat_Undef_inject_any:
forall f vl,
list_forall2 (memval_inject f) (list_repeat (length vl) Undef) vl.
list_forall2 (memval_inject f) (List.repeat Undef (length vl)) vl.
Proof.
induction vl; simpl; constructor; auto. constructor.
Qed.
Lemma repeat_Undef_inject_encode_val:
forall f chunk v,
list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v).
list_forall2 (memval_inject f) (List.repeat Undef (size_chunk_nat chunk)) (encode_val chunk v).
Proof.
intros. rewrite <- (encode_val_length chunk v). apply repeat_Undef_inject_any.
Qed.
Lemma repeat_Undef_inject_self:
forall f n,
list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef).
list_forall2 (memval_inject f) (List.repeat Undef n) (List.repeat Undef n).
Proof.
induction n; simpl; constructor; auto. constructor.
Qed.
......@@ -915,7 +915,7 @@ Theorem encode_val_inject:
Val.inject f v1 v2 ->
list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
Proof.
Local Opaque list_repeat.
Local Opaque List.repeat.
intros. inversion H; subst; simpl; destruct chunk;
auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val.
- destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self.
......
......@@ -1153,26 +1153,6 @@ Proof.
destruct l; simpl; auto.
Qed.
(** A list of [n] elements, all equal to [x]. *)
Fixpoint list_repeat {A: Type} (n: nat) (x: A) {struct n} :=
match n with
| O => nil
| S m => x :: list_repeat m x
end.
Lemma length_list_repeat:
forall (A: Type) n (x: A), length (list_repeat n x) = n.
Proof.
induction n; simpl; intros. auto. decEq; auto.
Qed.
Lemma in_list_repeat:
forall (A: Type) n (x: A) y, In y (list_repeat n x) -> y = x.
Proof.
induction n; simpl; intros. elim H. destruct H; auto.
Qed.
(** * Definitions and theorems over boolean types *)
Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool :=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment