proposition: Lemma wf_join_Branch_Branch_0: forall A opt p1 m (l1 r1: ptrie A) p2 l2 r2, p1 <> p2 -> wf opt (Branch p1 m l1 r1) -> wf opt (Branch p2 m l2 r2) -> wf opt (join p1 (Branch p1 m l1 r1) p2 (Branch p2 m l2 r2)).
proof: Proof. intros. generalize (branching_bit_spec _ _ H). intros [n [HA [HB HC]]]. inv H0; inv H1. - generalize (proj2 (Hbrbit'0 _) eq_refl); intros Heq. apply Hbrbit' in Heq. subst brbit'0. unfold join. case_eq (zerobit p1 (branching_bit p1 p2)); intros. + econstructor; try 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_false_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. } * assumption. * eapply mask_spec'; eauto. * assumption. * 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. } * assumption. * intros; eapply mask_spec; eauto. * assumption. * 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; trivial. { eapply mask_spec'; eauto. } { destruct (lt_dec n brbit'); try eassumption. elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { eapply mask_spec; eauto. } { assumption. } { assumption. } * econstructor; trivial. { erewrite zerobit_spec in H0; eauto. erewrite zerobit_spec; eauto. eapply negb_true_iff in H0. eapply negb_false_iff. destruct (testbit p2 n); congruence. } { eapply mask_spec'; eauto. } { destruct (lt_dec n brbit'); try eassumption. elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { intros; rewrite <- HB; auto. eapply mask_spec; eauto. } { assumption. } { assumption. } + econstructor; try 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_false_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. } * assumption. * eapply mask_spec'; eauto. * assumption. * 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. } * assumption. * intros; eapply mask_spec; eauto. * assumption. * 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; trivial. { erewrite zerobit_spec in H0; eauto. erewrite zerobit_spec; eauto. eapply negb_false_iff in H0. eapply negb_true_iff. destruct (testbit p2 n); congruence. } { eapply mask_spec'; eauto. } { destruct (lt_dec n brbit'); try eassumption. elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { intros; rewrite <- HB; auto. eapply mask_spec; eauto. } { assumption. } { assumption. } * econstructor; trivial. { eapply mask_spec'; eauto. } { destruct (lt_dec n brbit'); try eassumption. elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { eapply mask_spec; eauto. } { assumption. } { assumption. } - generalize (proj2 (Hbrbit'0 _) eq_refl); intros Heq. apply Hbrbit' in Heq. subst brbit'0. unfold join. case_eq (zerobit p1 (branching_bit p1 p2)); intros. + econstructor; try discriminate. * eassumption. * intros; eapply mask_spec; eauto. * econstructor; trivial. { eapply mask_spec'; eauto. } { inv H5; auto; congruence. } { destruct (lt_dec n brbit'); try eassumption. assert (Hlength : forall n : nat, (n >= brbit')%nat -> testbit p1 n = false) by (inv H5; try congruence; auto). assert (Hlength0 : forall n : nat, (n >= brbit')%nat -> testbit p2 n = false) by (inv H4; try congruence; auto). elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { eapply mask_spec; eauto. } { assumption. } { assumption. } * econstructor; trivial. { erewrite zerobit_spec in H0; eauto. erewrite zerobit_spec; eauto. eapply negb_true_iff in H0. eapply negb_false_iff. destruct (testbit p2 n); congruence. } { eapply mask_spec'; eauto. } { inv H4; auto; congruence. } { destruct (lt_dec n brbit'); try eassumption. assert (Hlength : forall n : nat, (n >= brbit')%nat -> testbit p1 n = false) by (inv H5; try congruence; auto). assert (Hlength0 : forall n : nat, (n >= brbit')%nat -> testbit p2 n = false) by (inv H4; try congruence; auto). elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { intros; rewrite <- HB; auto. eapply mask_spec; eauto. } { assumption. } { assumption. } + econstructor; try discriminate. * eassumption. * intros; eapply mask_spec; eauto. * econstructor; trivial. { erewrite zerobit_spec in H0; eauto. erewrite zerobit_spec; eauto. eapply negb_false_iff in H0. eapply negb_true_iff. destruct (testbit p2 n); congruence. } { eapply mask_spec'; eauto. } { inv H4; auto; congruence. } { destruct (lt_dec n brbit'); try eassumption. assert (Hlength : forall n : nat, (n >= brbit')%nat -> testbit p1 n = false) by (inv H5; try congruence; auto). assert (Hlength0 : forall n : nat, (n >= brbit')%nat -> testbit p2 n = false) by (inv H4; try congruence; auto). elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { intros; rewrite <- HB; auto. eapply mask_spec; eauto. } { assumption. } { assumption. } * econstructor; trivial. { eapply mask_spec'; eauto. } { inv H5; auto; congruence. } { destruct (lt_dec n brbit'); try eassumption. assert (Hlength : forall n : nat, (n >= brbit')%nat -> testbit p1 n = false) by (inv H5; try congruence; auto). assert (Hlength0 : forall n : nat, (n >= brbit')%nat -> testbit p2 n = false) by (inv H4; try congruence; auto). elim HC. rewrite Hlength; try lia; rewrite Hlength0; try lia; auto. } { assumption. } { assumption. } { eapply mask_spec; eauto. } { eapply mask_spec; eauto. } { assumption. } { assumption. } Qed.
imports: List Bool ZArith Lia