proposition: Lemma wf_join_Branch_Branch_1: forall A opt p1 m1 (l1 r1: ptrie A) p2 m2 l2 r2 (HLT: ltb m2 m1 = true), match_prefix p1 p2 m2 = false -> wf opt (Branch p1 m1 l1 r1) -> wf opt (Branch p2 m2 l2 r2) -> wf opt (join p1 (Branch p1 m1 l1 r1) p2 (Branch p2 m2 l2 r2)).
proof: Proof. intros; inv H0; inv H1. - rename H into HO. generalize (proj1 (match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) HO). intros [H [n' [HP HQ]]]. unfold join. generalize (branching_bit_spec _ _ H). intros [n [HA [HB HC]]]. apply HA in HQ. subst n'. case_eq (zerobit p1 (branching_bit p1 p2)); intros. + econstructor. * discriminate. * discriminate. * rewrite ! (zerobit_spec _ _ _ Hbrb). f_equal. destruct (lt_dec brb' n). { eapply mask_spec; eauto. } { destruct (eq_nat_dec brb' n). - subst n. rewrite (zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (testbit p1 brb'); destruct (testbit p2 brb'); auto; congruence. - elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * eauto. * eapply mask_spec'; auto. exact HA. * auto. * destruct (lt_dec brb' n); eauto. destruct (eq_nat_dec brb' n). { subst n. rewrite (zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (testbit p1 brb'); destruct (testbit p2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * auto. * intros. eapply mask_spec. exact HA. auto. * auto. * intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. destruct (lt_dec brb' n); try lia. destruct (eq_nat_dec brb' n). { subst n. rewrite (zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (testbit p1 brb'); destruct (testbit p2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * rewrite <- H0. econstructor; trivial. { eapply mask_spec'; eauto. } { rewrite (zerobit_spec _ _ _ HA) in H0. apply negb_true_iff in H0. eapply Nat.lt_trans; try eassumption. eapply ltb_spec; try eapply HLT; eauto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { eapply mask_spec; eauto. } { assumption. } { assumption. } * econstructor. { auto. } { auto. } { erewrite zerobit_spec; eauto. eapply negb_false_iff. erewrite zerobit_spec in H0; eauto. eapply negb_true_iff in H0. destruct (testbit p2 n); congruence; auto. } { eapply mask_spec'; auto. exact HA. } { auto. } { auto. } { eassumption. } { auto. } { auto. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } { auto. } { auto. } + econstructor. * discriminate. * discriminate. * rewrite ! (zerobit_spec _ _ _ Hbrb). f_equal. destruct (lt_dec brb' n). { eapply mask_spec; eauto. } { destruct (eq_nat_dec brb' n). - subst n. rewrite (zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (testbit p1 brb'); destruct (testbit p2 brb'); auto; congruence. - elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * eauto. * eapply mask_spec'; auto. exact HA. * auto. * destruct (lt_dec brb' n); eauto. destruct (eq_nat_dec brb' n). { subst n. rewrite (zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (testbit p1 brb'); destruct (testbit p2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * auto. * intros. eapply mask_spec. exact HA. auto. * auto. * intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. destruct (lt_dec brb' n); try lia. destruct (eq_nat_dec brb' n). { subst n. rewrite (zerobit_spec _ _ _ HA) in H0. eapply negb_true_iff in H0. rewrite ! (zerobit_spec _ _ _ Hbrb) in Hlr. elim HC. destruct (testbit p1 brb'); destruct (testbit p2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * econstructor. { auto. } { auto. } { erewrite zerobit_spec; eauto. eapply negb_true_iff. erewrite zerobit_spec in H0; eauto. eapply negb_false_iff in H0. destruct (testbit p2 n); congruence; auto. } { eapply mask_spec'; auto. exact HA. } { auto. } { auto. } { eassumption. } { auto. } { auto. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } { auto. } { auto. } * rewrite <- H0. econstructor; trivial. { eapply mask_spec'; eauto. } { rewrite (zerobit_spec _ _ _ HA) in H0. apply negb_true_iff in H0. eapply Nat.lt_trans; try eassumption. eapply ltb_spec; try eapply HLT; eauto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { eapply mask_spec; eauto. } { assumption. } { assumption. } - rename H into HO. assert (Hmask'0: mask p2 m2 = p2) by (inv H4; auto; congruence). generalize (proj1 (match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) HO). intros [H [n' [HP HQ]]]. unfold join. generalize (branching_bit_spec _ _ H). intros [n [HA [HB HC]]]. apply HA in HQ. subst n'. case_eq (zerobit p1 (branching_bit p1 p2)); intros. + econstructor. * discriminate. * discriminate. * eauto. * intros. eapply mask_spec. exact HA. auto. * econstructor. { auto. } { auto. } { erewrite zerobit_spec; eauto. eapply negb_true_iff. erewrite zerobit_spec in H0; eauto. eapply negb_true_iff in H0. assumption. } { eapply mask_spec'; auto. exact HA. } { inv H5; auto; congruence. } { auto. } { eapply Nat.lt_trans; try eassumption. eapply ltb_spec; try eapply HLT; eauto. } { auto. } { auto. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } { auto. } { auto. } * econstructor; try eassumption. { erewrite zerobit_spec; eauto. erewrite zerobit_spec in H0; eauto. rewrite negb_true_iff in H0. rewrite negb_false_iff. destruct (testbit p2 n); auto; congruence. } { eapply mask_spec'; eauto. } { eapply mask_spec; auto. } { intros; rewrite <- HB; auto; eapply mask_spec; eauto. } + econstructor. * discriminate. * discriminate. * eauto. * intros. eapply mask_spec. exact HA. auto. * econstructor. { auto. } { auto. } { erewrite zerobit_spec; eauto. eapply negb_true_iff. erewrite zerobit_spec in H0; eauto. eapply negb_false_iff in H0. destruct (testbit p2 n); congruence; auto. } { eapply mask_spec'; auto. exact HA. } { auto. } { auto. } { eassumption. } { auto. } { auto. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } { auto. } { auto. } * rewrite <- H0. econstructor; trivial. { eapply mask_spec'; eauto. } { inv H5; auto; congruence. } { rewrite (zerobit_spec _ _ _ HA) in H0. apply negb_true_iff in H0. eapply Nat.lt_trans; try eassumption. eapply ltb_spec; try eapply HLT; eauto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { eapply mask_spec; eauto. } { assumption. } { assumption. } Qed.
imports: List Bool ZArith Lia