proposition: Lemma natmap_fold_raw_ind {A B} (P : B → natmap_raw A → Prop) (f : nat → A → B → B) j (b : B) : P b [] → (∀ i x l b', natmap_wf l → mjoin (l !! i) = None → P b' l → P (f (i + j) x b') (natmap_partial_alter_raw (λ _, Some x) i l)) → ∀ l, natmap_wf l → P (natmap_fold_raw f j b l) l.
proof: Proof. intros Hemp Hinsert l Hl. revert P b j Hemp Hinsert. induction l as [|mx l IH]; intros P b j Hemp Hinsert; simpl in *; [done|]. assert (natmap_wf l) as Hl' by (by destruct l). replace (mx :: l) with (natmap_cons_canon mx l) by (destruct mx, l; done || by destruct Hl). apply (IH Hl' (λ r l, P r (natmap_cons_canon mx l)) _ (S j)). { destruct mx as [x|]; [|done]. change (natmap_cons_canon (Some x) []) with (natmap_partial_alter_raw (λ _, Some x) 0 []). by apply (Hinsert 0). } intros i x l' b' ??. rewrite <-Nat.add_succ_comm. replace (natmap_cons_canon mx (natmap_partial_alter_raw (λ _, Some x) i l')) with (natmap_partial_alter_raw (λ _, Some x) (S i) (natmap_cons_canon mx l')) by (by destruct i, mx, l'). apply Hinsert; [by apply natmap_cons_canon_wf|by destruct mx, l']. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)