proposition: Lemma elements_remove: forall (A: Type) i v (m: ptrie A) o, wf o m -> get' i m = Some v -> exists l1 l2, elements' m nil = l1 ++ (i,v) :: l2 /\ elements' (remove' i m) nil = l1 ++ l2.
proof: Proof. induction m; intros. - simpl in H0; inv H0. - generalize (get_some_implies _ H H0). intros; subst i. simpl in H0. simpl; eauto. exists nil, nil. rewrite elt_eqb_refl in *; try congruence. split; auto. rewrite app_nil_l. inv H0; auto. - generalize (get_some_implies _ H H0). intros HA. simpl in H0. rewrite elements_branch'. simpl. assert (Hmask: exists brbit', Key.is_mask brbit brbit' /\ Key.mask prefix brbit = prefix). { inv H; eexists; split; eauto. eapply Key.testbit_spec. intros. generalize (Key.mask_spec prefix _ _ Hbrbit'). intros [HX HY]. destruct (lt_dec n brbit'). - rewrite HX; auto. - rewrite Hprefix; try lia. apply HY; lia. } destruct Hmask as [brbit' [Hmask1 Hmask2]]. generalize (proj2 (Key.match_prefix_spec _ _ _ _ Hmask1 Hmask2) (HA _ Hmask1)). intros HB. rewrite HB. case_eq (Key.zerobit i brbit); intros. + rewrite H1 in H0. assert (exists o1, wf o1 m1) by (inv H; eauto). destruct H2 as [o1 Ho1]. generalize (IHm1 o1 Ho1 H0). intros [l1 [l2 [HC HD]]]. rewrite HC. exists l1, (l2 ++ elements' m2 nil). split. * rewrite app_assoc_reverse. rewrite app_comm_cons. reflexivity. * destruct m1. { inv H; congruence. } { simpl in H0. destruct_elt_eq i k; try congruence. inv H0. simpl. simpl in HD. rewrite elt_eqb_refl in *; try congruence. simpl in HD. simpl. generalize (app_eq_nil l1 l2 (eq_sym HD)). intros [HX HY]; subst. simpl. reflexivity. } { generalize (remove_branch_not_empty Ho1 eq_refl i). intros HE. assert (Hm2: m2 <> Empty) by (inv H; auto). rewrite branch_not_empty; eauto. rewrite elements_branch'. rewrite HD. apply app_assoc_reverse. } + rewrite H1 in H0. assert (exists o2, wf o2 m2) by (inv H; eauto). destruct H2 as [o2 Ho2]. generalize (IHm2 o2 Ho2 H0). intros [l1 [l2 [HC HD]]]. rewrite HC. exists (elements' m1 nil ++ l1), l2. split. * rewrite app_assoc_reverse. reflexivity. * destruct m2. { inv H; congruence. } { simpl in H0. destruct_elt_eq i k; try congruence. inv H0. simpl. simpl in HD. rewrite elt_eqb_refl in *; try congruence. simpl in HD. simpl. generalize (app_eq_nil l1 l2 (eq_sym HD)). intros [HX HY]; subst. destruct m1; unfold branch; try reflexivity. rewrite ! app_nil_r. reflexivity. } { generalize (remove_branch_not_empty Ho2 eq_refl i). intros HE. assert (Hm1: m1 <> Empty) by (inv H; auto). rewrite branch_not_empty; eauto. rewrite elements_branch'. rewrite HD. apply app_assoc. } Qed.
imports: Lia Cdcl.Coqlib