proposition: Lemma wf_join_Branch: forall A opt k1 k2 v1 m2 (t1 t2: ptrie A), let m := Key.branching_bit k1 k2 in Key.match_prefix k1 k2 m2 = false -> wf opt (Leaf k1 v1) -> wf opt (Branch k2 m2 t1 t2) -> wf opt (join k1 (Leaf k1 v1) k2 (Branch k2 m2 t1 t2)).
proof: Proof. intros; inv H0; inv H1. - rename H into HO. generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') HO). intros [H [n' [HP HQ]]]. unfold join. generalize (Key.branching_bit_spec _ _ H). intros [n [HA [HB HC]]]. apply HA in HQ. subst n'. case_eq (Key.zerobit k1 (Key.branching_bit k1 k2)); intros. + econstructor. * discriminate. * discriminate. * rewrite ! (Key.zerobit_spec _ _ _ Hbrb). f_equal. fold m. destruct (lt_dec brb' n). { eapply Key.mask_spec; eauto. } { destruct (eq_nat_dec brb' n). - subst n. rewrite (Key.zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite H0. eapply Key.mask_spec; eauto. - elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * eauto. * eapply Key.mask_spec'; auto. exact HA. * auto. * destruct (lt_dec brb' n); eauto. destruct (eq_nat_dec brb' n). { subst n. rewrite (Key.zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (Key.zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (Key.testbit k1 brb'); destruct (Key.testbit k2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * auto. * intros. eapply Key.mask_spec. exact HA. auto. * auto. * intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. destruct (lt_dec brb' n); try lia. destruct (eq_nat_dec brb' n). { subst n. rewrite (Key.zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (Key.zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (Key.testbit k1 brb'); destruct (Key.testbit k2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * econstructor; eauto. { eapply Key.mask_spec'; auto. exact HA. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } * econstructor. { auto. } { auto. } { erewrite Key.zerobit_spec; eauto. eapply negb_false_iff. erewrite Key.zerobit_spec in H0; eauto. eapply negb_true_iff in H0. destruct (Key.testbit k2 n); congruence; auto. } { eapply Key.mask_spec'; auto. exact HA. } { auto. } { auto. } { destruct (lt_dec n brbit'). exact l. rewrite (Key.zerobit_spec _ _ _ HA) in H0. apply negb_true_iff in H0. assert (Key.testbit k2 n = false) by (eapply Hlength0; lia). congruence. } { auto. } { auto. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } { auto. } { auto. } + econstructor. * discriminate. * discriminate. * rewrite ! (Key.zerobit_spec _ _ _ Hbrb). f_equal. fold m. destruct (lt_dec brb' n). { eapply Key.mask_spec; eauto. } { destruct (eq_nat_dec brb' n). - subst n. rewrite (Key.zerobit_spec _ _ _ HA) in H0. eapply negb_false_iff in H0. rewrite ! (Key.zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (Key.testbit k1 brb'); destruct (Key.testbit k2 brb'); auto; congruence. - elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * eauto. * eapply Key.mask_spec'; auto. exact HA. * auto. * destruct (lt_dec brb' n); eauto. destruct (eq_nat_dec brb' n). { subst n. rewrite (Key.zerobit_spec _ _ _ HA) in H0. eapply negb_false_iff in H0. rewrite ! (Key.zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (Key.testbit k1 brb'); destruct (Key.testbit k2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * auto. * intros. eapply Key.mask_spec. exact HA. auto. * auto. * intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. destruct (lt_dec brb' n); try lia. destruct (eq_nat_dec brb' n). { subst n. rewrite (Key.zerobit_spec _ _ _ HA) in H0. eapply negb_false_iff in H0. rewrite ! (Key.zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (Key.testbit k1 brb'); destruct (Key.testbit k2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * econstructor. { auto. } { auto. } { erewrite Key.zerobit_spec; eauto. eapply negb_true_iff. erewrite Key.zerobit_spec in H0; eauto. eapply negb_false_iff in H0. destruct (Key.testbit k2 n); congruence; auto. } { eapply Key.mask_spec'; auto. exact HA. } { auto. } { auto. } { exact HP. } { auto. } { auto. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } { auto. } { auto. } * econstructor; eauto. { eapply Key.mask_spec'; auto. exact HA. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } - rename H into HO. assert (Hmask': Key.mask k2 m2 = k2). { inv H4; try congruence; auto. } generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') HO). intros [H [n' [HP HQ]]]. unfold join. generalize (Key.branching_bit_spec _ _ H). intros [n [HA [HB HC]]]. apply HA in HQ. subst n'. case_eq (Key.zerobit k1 (Key.branching_bit k1 k2)); intros. + econstructor. * discriminate. * discriminate. * eauto. * intros. eapply Key.mask_spec. exact HA. auto. * econstructor; eauto. { eapply Key.mask_spec'; auto. exact HA. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } * econstructor. { auto. } { auto. } { erewrite Key.zerobit_spec; eauto. eapply negb_false_iff. erewrite Key.zerobit_spec in H0; eauto. eapply negb_true_iff in H0. destruct (Key.testbit k2 n); congruence; auto. } { eapply Key.mask_spec'; auto. exact HA. } { auto. } { auto. } { exact HP. } { auto. } { auto. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } { auto. } { auto. } + econstructor. * discriminate. * discriminate. * eauto. * intros. eapply Key.mask_spec. exact HA. auto. * econstructor. { auto. } { auto. } { erewrite Key.zerobit_spec; eauto. eapply negb_true_iff. erewrite Key.zerobit_spec in H0; eauto. eapply negb_false_iff in H0. destruct (Key.testbit k2 n); congruence; auto. } { eapply Key.mask_spec'; auto. exact HA. } { auto. } { auto. } { exact HP. } { auto. } { auto. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } { auto. } { auto. } * econstructor; eauto. { eapply Key.mask_spec'; auto. exact HA. } { intros; eapply Key.mask_spec. exact HA. auto. } { intros. rewrite (proj1 (Key.mask_spec _ _ _ HA)); auto. } Qed.
imports: Lia Cdcl.Coqlib