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

Merge branch 'msammler/fix_imap_seq0' into 'master'

fix imap_seq and imap_seq0 to make them useful

See merge request iris/stdpp!151
parents 93b578a5 94c07daa
...@@ -38,14 +38,14 @@ Section seq. ...@@ -38,14 +38,14 @@ Section seq.
Qed. Qed.
Lemma fmap_S_seq j n : S <$> seq j n = seq (S j) n. Lemma fmap_S_seq j n : S <$> seq j n = seq (S j) n.
Proof. apply (fmap_add_seq 1). Qed. Proof. apply (fmap_add_seq 1). Qed.
Lemma imap_seq {A} (l : list A) (g : nat A) i : Lemma imap_seq {A B} (l : list A) (g : nat B) i :
imap (λ j _, g (i + j)) l = g <$> seq i (length l). imap (λ j _, g (i + j)) l = g <$> seq i (length l).
Proof. Proof.
revert i. induction l as [|x l IH]; [done|]. revert i. induction l as [|x l IH]; [done|].
csimpl. intros n. rewrite <-IH, <-plus_n_O. f_equal. csimpl. intros n. rewrite <-IH, <-plus_n_O. f_equal.
apply imap_ext; simpl; auto with lia. apply imap_ext; simpl; auto with lia.
Qed. Qed.
Lemma imap_seq_0 {A} (l : list A) (g : nat A) : Lemma imap_seq_0 {A B} (l : list A) (g : nat B) :
imap (λ j _, g j) l = g <$> seq 0 (length l). imap (λ j _, g j) l = g <$> seq 0 (length l).
Proof. rewrite (imap_ext _ (λ i o, g (0 + i))); [|done]. apply imap_seq. Qed. Proof. rewrite (imap_ext _ (λ i o, g (0 + i))); [|done]. apply imap_seq. Qed.
Lemma lookup_seq_lt j n i : i < n seq j n !! i = Some (j + i). Lemma lookup_seq_lt j n i : i < n seq j n !! i = Some (j + i).
......
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