proposition: Lemma wf_join_Leaf: forall A opt k1 k2 (v1 v2: A), let m := branching_bit k1 k2 in k1 <> k2 -> wf opt (Leaf k1 v1) -> wf opt (Leaf k2 v2) -> wf opt (join k1 (Leaf k1 v1) k2 (Leaf k2 v2)).
proof: Proof. intros; inv H0; inv H1. - unfold join. generalize (branching_bit_spec _ _ H). intros [n [HA [HB HC]]]. case_eq (zerobit k1 (branching_bit k1 k2)); intros. + econstructor. * discriminate. * discriminate. * rewrite ! (zerobit_spec _ _ _ Hbrb). f_equal. fold m. 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 k1 brb'); destruct (testbit k2 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 k1 brb'); destruct (testbit k2 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 k1 brb'); destruct (testbit k2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * econstructor; eauto. { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } * econstructor; eauto. { erewrite zerobit_spec; eauto. eapply negb_false_iff. erewrite zerobit_spec in H0; eauto. eapply negb_true_iff in H0. destruct (testbit k2 n); congruence; auto. } { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } + econstructor. * discriminate. * discriminate. * rewrite ! (zerobit_spec _ _ _ Hbrb). f_equal. fold m. 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 k1 brb'); destruct (testbit k2 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 k1 brb'); destruct (testbit k2 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 k1 brb'); destruct (testbit k2 brb'); auto; congruence. } { elim HC. rewrite <- Hprefix; try lia; auto. apply Hprefix0; lia. } * econstructor; eauto. { erewrite zerobit_spec; eauto. eapply negb_true_iff. erewrite zerobit_spec in H0; eauto. eapply negb_false_iff in H0. destruct (testbit k2 n); congruence; auto. } { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } * econstructor; eauto. { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } - unfold join. generalize (branching_bit_spec _ _ H). intros [n [HA [HB HC]]]. case_eq (zerobit k1 (branching_bit k1 k2)); intros. + econstructor. * discriminate. * discriminate. * eauto. * intros. eapply mask_spec. exact HA. auto. * econstructor; eauto. { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } * econstructor; eauto. { erewrite zerobit_spec; eauto. eapply negb_false_iff. erewrite zerobit_spec in H0; eauto. eapply negb_true_iff in H0. destruct (testbit k2 n); congruence; auto. } { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } + econstructor. * discriminate. * discriminate. * eauto. * intros. eapply mask_spec. exact HA. auto. * econstructor; eauto. { erewrite zerobit_spec; eauto. eapply negb_true_iff. erewrite zerobit_spec in H0; eauto. eapply negb_false_iff in H0. destruct (testbit k2 n); congruence; auto. } { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } * econstructor; eauto. { eapply mask_spec'; auto. exact HA. } { intros; eapply mask_spec. exact HA. auto. } { intros. rewrite (proj1 (mask_spec _ _ _ HA)); auto. } Qed.
imports: List Bool ZArith Lia