proposition: Lemma gro': forall (A: Type) opt (i j: key) (m: ptrie A), wf opt m -> i <> j -> get' i (remove' j m) = get' i m.
proof: Proof. induction 1; intros. - reflexivity. - simpl. repeat rewrite eqb_is_dec. destruct (eq k j); simpl; repeat rewrite eqb_is_dec; destruct (eq i k); simpl; try congruence. - simpl. repeat rewrite eqb_is_dec; destruct (eq k j); simpl; repeat rewrite eqb_is_dec; destruct (eq i k); simpl; congruence. - simpl. case_eq (match_prefix j prefix brbit); intros. + case_eq (zerobit j brbit); intros. * unfold branch. case_eq (remove' j l); intros. { case_eq (zerobit i brbit); intros; auto. rewrite <- IHwf1; auto. rewrite H4; simpl. eapply get_not_same_lr; eauto. } { destruct r. - rewrite <- H4. rewrite IHwf1; auto. case_eq (zerobit i brbit); intros; auto. simpl. eapply get_not_same_lr; eauto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } { destruct r. - rewrite <- H4. rewrite IHwf1; auto. case_eq (zerobit i brbit); intros; auto. simpl. eapply get_not_same_lr; eauto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } * unfold branch. destruct l; auto. { rewrite IHwf2; auto. case_eq (zerobit i brbit); intros; auto. simpl. eapply get_not_same_lr; eauto. } { case_eq (remove' j r); intros. - case_eq (zerobit i brbit); intros; auto. symmetry. simpl. repeat rewrite eqb_is_dec; destruct (eq i k). + subst k. inv H; congruence. + rewrite <- IHwf2; auto. rewrite H4. reflexivity. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } { case_eq (remove' j r); intros. - simpl. case_eq (zerobit i brbit); intros; auto. rewrite <- IHwf2; auto. rewrite H4; simpl. case_eq (zerobit i brbit0); intros. + inv H. eapply get_not_same_prefix; eauto. erewrite zerobit_spec in Hlr0; eauto. erewrite zerobit_spec in H5; eauto. congruence. + inv H. eapply get_not_same_prefix; eauto. erewrite zerobit_spec in Hlr0; eauto. erewrite zerobit_spec in H5; eauto. congruence. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } + simpl. auto. - simpl. case_eq (match_prefix j prefix brbit); intros. + case_eq (zerobit j brbit); intros. * unfold branch. case_eq (remove' j l); intros. { case_eq (zerobit i brbit); intros; auto. rewrite <- IHwf1; auto. rewrite H4; simpl. eapply get_not_same_lr; eauto. } { destruct r. - rewrite <- H4. rewrite IHwf1; auto. case_eq (zerobit i brbit); intros; auto. simpl. eapply get_not_same_lr; eauto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } { destruct r. - rewrite <- H4. rewrite IHwf1; auto. case_eq (zerobit i brbit); intros; auto. simpl. eapply get_not_same_lr; eauto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } * unfold branch. destruct l; auto. { rewrite IHwf2; auto. case_eq (zerobit i brbit); intros; auto. simpl. eapply get_not_same_lr; eauto. } { case_eq (remove' j r); intros. - case_eq (zerobit i brbit); intros; auto. symmetry. simpl. repeat rewrite eqb_is_dec;destruct (eq i k). + subst k. inv H; congruence. + rewrite <- IHwf2; auto. rewrite H4. reflexivity. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } { case_eq (remove' j r); intros. - simpl. case_eq (zerobit i brbit); intros; auto. rewrite <- IHwf2; auto. rewrite H4; simpl. case_eq (zerobit i brbit0); intros. + inv H. eapply get_not_same_prefix; eauto. erewrite zerobit_spec in Hlr; eauto. erewrite zerobit_spec in H5; eauto. congruence. + inv H. eapply get_not_same_prefix; eauto. erewrite zerobit_spec in Hlr; eauto. erewrite zerobit_spec in H5; eauto. congruence. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. - rewrite <- H4. simpl. case_eq (zerobit i brbit); intros; auto. } + simpl. auto. Qed.
imports: List Bool ZArith Lia