proposition: Lemma wf_xcombine': forall (A: Type) c (t1 t2: ptrie A) opt, wf opt t1 -> wf opt t2 -> wf opt (xcombine' c t1 t2).
proof: Proof. induction t1; induction t2; intros. - simpl; econstructor. - simpl; auto. - simpl; auto. - simpl; auto. - simpl. destruct_eq k k0. + inv H; econstructor; eauto. + eapply wf_join_Leaf; eauto. - unfold xcombine'. eapply wf_insert'; eauto. - simpl; auto. - unfold xcombine'. eapply wf_insert'; eauto. - simpl. erewrite <- ! (combine_aux_xcombine' c prefix brbit t1_1 t1_2 t2_2). erewrite <- ! (combine_aux_xcombine' c prefix brbit t1_1 t1_2 t2_1). Local Opaque xcombine'. destruct_eq brbit brbit0. + destruct_eq prefix prefix0. * simpl; subst. inv H; inv H0; econstructor; eauto. { eapply xcombine'_not_empty. left; auto. } { eapply xcombine'_not_empty. left; auto. } { eapply IHt1_1; eauto. assert (brbit'0 = brbit'). - generalize (proj2 (Hbrbit'0 _) eq_refl). intros; symmetry; eapply Hbrbit'; auto. - subst; auto. } { eapply IHt1_2; eauto. assert (brbit'0 = brbit'). - generalize (proj2 (Hbrbit'0 _) eq_refl). intros; symmetry; eapply Hbrbit'; auto. - subst; auto. } { eapply xcombine'_not_empty. left; auto. } { eapply xcombine'_not_empty. left; auto. } { eapply IHt1_1; eauto. assert (brbit'0 = brbit'). - generalize (proj2 (Hbrbit'0 _) eq_refl). intros; symmetry; eapply Hbrbit'; auto. - subst; auto. } { eapply IHt1_2; eauto. assert (brbit'0 = brbit'). - generalize (proj2 (Hbrbit'0 _) eq_refl). intros; symmetry; eapply Hbrbit'; auto. - subst; auto. } * subst. case_eq (ltb brbit0 brbit0); intros. { inv H; inv H0; eapply ltb_spec in H1; eauto; lia. } { simpl. eapply wf_join_Branch_Branch_0; eauto. } + case_eq (ltb brbit brbit0); intros. * case_eq (match_prefix prefix0 prefix brbit); intros. { rewrite andb_comm. simpl. case_eq (zerobit prefix0 brbit); intros. - inv H; inv H0; econstructor; trivial. + eapply xcombine'_not_empty; eauto; right; discriminate. + exact Hincr. + assumption. + assumption. + eapply IHt1_1; eauto. econstructor; try eassumption. * eapply ltb_spec; eauto. * generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit' Hmask') H2). intros; symmetry; eapply H; eauto. + assumption. + eapply xcombine'_not_empty; eauto; right; discriminate. + eassumption. + assumption. + eapply IHt1_1; eauto. econstructor; try eassumption. * inv H7; auto; congruence. * inv H6; auto; congruence. * eapply ltb_spec; eauto. * assert (Hmask': mask prefix brbit = prefix) by (inv H7; auto; congruence). generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit' Hmask') H2). intros; symmetry; eapply H; eauto. + assumption. - inv H; inv H0; econstructor; trivial. + eapply xcombine'_not_empty; eauto; right; discriminate. + exact Hincr. + assumption. + assumption. + assumption. + eapply IHt1_2; eauto. econstructor; try eassumption. * eapply ltb_spec; eauto. * generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit' Hmask') H2). intros; symmetry; eapply H; eauto. + eapply xcombine'_not_empty; eauto; right; discriminate. + eassumption. + assumption. + assumption. + eapply IHt1_2; eauto. econstructor; try eassumption. * inv H7; auto; congruence. * inv H6; auto; congruence. * eapply ltb_spec; eauto. * assert (Hmask': mask prefix brbit = prefix) by (inv H7; auto; congruence). generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit' Hmask') H2). intros; symmetry; eapply H; eauto. } { rewrite andb_comm; simpl. case_eq (ltb brbit0 brbit); intros. - inv H; inv H0. + eapply ltb_spec in H1; eauto. eapply ltb_spec in H3; eauto. assert (brbit'0 = brbit') by lia. subst. elim n. eapply testbit_spec; intros. case_eq (testbit brbit n0); case_eq (testbit brbit0 n0); intros; auto. * eapply Hbrbit' in H0. subst n0. generalize (proj2 (Hbrbit'0 _) eq_refl); intros; congruence. * eapply Hbrbit'0 in H. subst n0. generalize (proj2 (Hbrbit' _) eq_refl); intros; congruence. + eapply ltb_spec in H1; eauto. eapply ltb_spec in H3; eauto. assert (brbit'0 = brbit') by lia. subst. elim n. eapply testbit_spec; intros. case_eq (testbit brbit n0); case_eq (testbit brbit0 n0); intros; auto. * eapply Hbrbit' in H0. subst n0. generalize (proj2 (Hbrbit'0 _) eq_refl); intros; congruence. * eapply Hbrbit'0 in H. subst n0. generalize (proj2 (Hbrbit' _) eq_refl); intros; congruence. - simpl. eapply wf_join_Branch_Branch_2; eauto. } * rewrite andb_comm; simpl. case_eq (ltb brbit0 brbit); intros. { case_eq (match_prefix prefix prefix0 brbit0); intros. - simpl. case_eq (zerobit prefix brbit0); intros. + inv H; inv H0; econstructor; eauto. * eapply xcombine'_not_empty; eauto; left; discriminate. * eapply IHt2_1; eauto. econstructor; try eassumption. { eapply ltb_spec; eauto. } { generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit'0 Hmask'0) H3). intros; symmetry; eapply H; eauto. } * eapply xcombine'_not_empty; eauto; left; discriminate. * eapply IHt2_1; eauto. econstructor; try eassumption. { inv H7; auto; congruence. } { inv H8; auto; congruence. } { eapply ltb_spec; eauto. } { assert (Hmask'0: mask prefix0 brbit0 = prefix0) by (inv H7; auto; congruence). generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit'0 Hmask'0) H3). intros; symmetry; eapply H; eauto. } + inv H; inv H0; econstructor; eauto. * eapply xcombine'_not_empty; eauto; left; discriminate. * eapply IHt2_2; eauto. econstructor; try eassumption. { eapply ltb_spec; eauto. } { generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit'0 Hmask'0) H3). intros; symmetry; eapply H; eauto. } * eapply xcombine'_not_empty; eauto; left; discriminate. * eapply IHt2_2; eauto. econstructor; try eassumption. { inv H7; auto; congruence. } { inv H8; auto; congruence. } { eapply ltb_spec; eauto. } { assert (Hmask'0: mask prefix0 brbit0 = prefix0) by (inv H7; auto; congruence). generalize (proj1 (match_prefix_spec _ _ _ _ Hbrbit'0 Hmask'0) H3). intros; symmetry; eapply H; eauto. } - simpl. eapply wf_join_Branch_Branch_1; eauto. } { inv H; inv H0. - destruct (eq_nat_dec brbit'0 brbit'). + subst. elim n. eapply testbit_spec; intros. case_eq (testbit brbit n0); case_eq (testbit brbit0 n0); intros; auto. * eapply Hbrbit' in H0. subst n0. generalize (proj2 (Hbrbit'0 _) eq_refl); intros; congruence. * eapply Hbrbit'0 in H. subst n0. generalize (proj2 (Hbrbit' _) eq_refl); intros; congruence. + destruct (lt_dec brbit' brbit'0). * generalize (proj2 (ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) l). intros; congruence. * assert (brbit'0 < brbit')%nat by lia. generalize (proj2 (ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H). intros; congruence. - destruct (eq_nat_dec brbit'0 brbit'). + subst. elim n. eapply testbit_spec; intros. case_eq (testbit brbit n0); case_eq (testbit brbit0 n0); intros; auto. * eapply Hbrbit' in H0. subst n0. generalize (proj2 (Hbrbit'0 _) eq_refl); intros; congruence. * eapply Hbrbit'0 in H. subst n0. generalize (proj2 (Hbrbit' _) eq_refl); intros; congruence. + destruct (lt_dec brbit' brbit'0). * generalize (proj2 (ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) l). intros; congruence. * assert (brbit'0 < brbit')%nat by lia. generalize (proj2 (ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H). intros; congruence. } Qed.
imports: List Bool ZArith Lia