Commit fe63b525 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'insert_replicate' into 'master'

Add `insert_replicate_strong`.

See merge request iris/stdpp!178
parents de08bf75 78856dfd
......@@ -1226,6 +1226,15 @@ Proof.
Qed.
Lemma insert_replicate x n i : <[i:=x]>(replicate n x) = replicate n x.
Proof. revert i. induction n; intros [|?]; f_equal/=; auto. Qed.
Lemma insert_replicate_lt x y n i :
i < n
<[i:=y]>(replicate n x) = replicate i x ++ y :: replicate (n - S i) x.
Proof.
revert i. induction n as [|n IH]; [ by lia | ].
intros [|i] Hi; simpl.
- by rewrite Nat.sub_0_r.
- by rewrite IH by lia.
Qed.
Lemma elem_of_replicate_inv x n y : x replicate n y x = y.
Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate n x.
......
Supports Markdown
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