proposition: Lemma gcombine': forall (A: Type) (c: A -> A -> A) (t1 t2: ptrie A) opt i, wf opt t1 -> wf opt t2 -> get' i (combine' c t1 t2) = match get' i t1, get' i t2 with | None, None => None | None, Some x2 => Some x2 | Some x1, None => Some x1 | Some x1, Some x2 => Some (c x1 x2) end.
proof: Proof. induction t1; induction t2; intros; simpl; try reflexivity. - destruct_elt_eq i k; simpl; auto. - case_eq (Key.zerobit i brbit); intros; simpl; auto. + destruct (get' i t2_1); auto. + destruct (get' i t2_2); auto. - destruct_elt_eq i k; simpl; auto. - destruct_elt_eq i k. + subst. eapply gis'. eauto. + erewrite gio'; eauto. simpl. destruct_elt_eq i k0; auto. - destruct_elt_eq i k. + subst. eapply gis'; eauto. + erewrite gio'; eauto. simpl. destruct (Key.zerobit i brbit); destruct (get' i t2_1); destruct (get' i t2_2); auto. - destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); auto. - destruct_elt_eq i k. + subst; eapply gis'; eauto. + erewrite gio'; eauto. simpl. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); auto. - rewrite andb_comm. Local Transparent insert'. simpl. erewrite <- ! (combine_aux_combine' c prefix brbit t1_1 t1_2 t2_2). erewrite <- ! (combine_aux_combine' c prefix brbit t1_1 t1_2 t2_1). Local Opaque combine'. destruct_elt_eq brbit brbit0. + destruct_elt_eq prefix prefix0. * simpl. subst. inv H; inv H0. { case_eq (Key.zerobit i brbit0); intros. - eapply IHt1_1; eauto. replace brbit' with brbit'0; auto. symmetry; eapply Hbrbit'. eapply (proj2 (Hbrbit'0 _) eq_refl). - eapply IHt1_2; eauto. replace brbit' with brbit'0; auto. symmetry; eapply Hbrbit'. eapply (proj2 (Hbrbit'0 _) eq_refl). } { case_eq (Key.zerobit i brbit0); intros. - eapply IHt1_1; eauto. replace brbit' with brbit'0; auto. symmetry; eapply Hbrbit'. eapply (proj2 (Hbrbit'0 _) eq_refl). - eapply IHt1_2; eauto. replace brbit' with brbit'0; auto. symmetry; eapply Hbrbit'. eapply (proj2 (Hbrbit'0 _) eq_refl). } * subst. simpl. case_eq (Key.ltb brbit0 brbit0); intros. { inv H; eapply Key.ltb_spec in H1; eauto; lia. } { simpl. unfold join; auto. case_eq (Key.zerobit prefix (Key.branching_bit prefix prefix0)); intros. - simpl. case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. + case_eq (Key.zerobit i brbit0); intros. * inv H; inv H0. { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t2_1 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t1_1); auto. - elim HC. rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t2_1 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t1_1); auto. - elim HC. assert (Hlength: forall n, (n >= brbit')%nat -> Key.testbit prefix n = false) by (inv H8; auto; congruence). assert (Hlength0: forall n, (n >= brbit')%nat -> Key.testbit prefix0 n = false) by (inv H7; auto; congruence). rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } * inv H; inv H0. { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t2_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t1_2); auto. - elim HC. rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t2_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t1_2); auto. - elim HC. assert (Hlength: forall n, (n >= brbit')%nat -> Key.testbit prefix n = false) by (inv H8; auto; congruence). assert (Hlength0: forall n, (n >= brbit')%nat -> Key.testbit prefix0 n = false) by (inv H7; auto; congruence). rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } + inv H; inv H0. * generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). { assert (get' i t1_1 = None). - eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_false_iff in H3. congruence. - assert (get' i t1_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_false_iff in H3. congruence. + rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t2_1); destruct (get' i t2_2); auto. } { elim HC. rewrite Hlength; try lia. rewrite Hlength0; lia. } * generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). { assert (get' i t1_1 = None). - eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_false_iff in H3. congruence. - assert (get' i t1_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_true_iff in H2. eapply negb_false_iff in H3. congruence. + rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t2_1); destruct (get' i t2_2); auto. } { elim HC. assert (Hlength: forall n, (n >= brbit')%nat -> Key.testbit prefix n = false) by (inv H7; auto; congruence). assert (Hlength0: forall n, (n >= brbit')%nat -> Key.testbit prefix0 n = false) by (inv H6; auto; congruence). rewrite Hlength; try lia. rewrite Hlength0; lia. } - simpl. case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. + case_eq (Key.zerobit i brbit0); intros. * inv H; inv H0. { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t1_1 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t2_1); auto. - elim HC. rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t1_1 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t2_1); auto. - elim HC. assert (Hlength: forall n, (n >= brbit')%nat -> Key.testbit prefix n = false) by (inv H8; auto; congruence). assert (Hlength0: forall n, (n >= brbit')%nat -> Key.testbit prefix0 n = false) by (inv H7; auto; congruence). rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } * inv H; inv H0. { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t1_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t2_2); auto. - elim HC. rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } { generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). - assert (get' i t1_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_true_iff in H3. rewrite H3; destruct (Key.testbit prefix n'); congruence. + rewrite H. destruct (get' i t2_2); auto. - elim HC. assert (Hlength: forall n, (n >= brbit')%nat -> Key.testbit prefix n = false) by (inv H8; auto; congruence). assert (Hlength0: forall n, (n >= brbit')%nat -> Key.testbit prefix0 n = false) by (inv H7; auto; congruence). rewrite Hlength; try lia. rewrite Hlength0; try lia; auto. } + inv H; inv H0. * generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). { assert (get' i t2_1 = None). - eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_false_iff in H3. congruence. - assert (get' i t2_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_false_iff in H3. congruence. + rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t1_1); destruct (get' i t1_2); auto. } { elim HC. rewrite Hlength; try lia. rewrite Hlength0; lia. } * generalize (Key.branching_bit_spec _ _ n). intros [n' [HA [HB HC]]]. generalize (proj2 (Hbrbit'0 _) eq_refl); intros HD; eapply Hbrbit' in HD. subst brbit'0. destruct (lt_dec n' brbit'). { assert (get' i t2_1 = None). - eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_false_iff in H3. congruence. - assert (get' i t2_2 = None). + eapply get_not_same_prefix; eauto. erewrite Key.zerobit_spec in H2; eauto. erewrite Key.zerobit_spec in H3; eauto. eapply negb_false_iff in H2. eapply negb_false_iff in H3. congruence. + rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t1_1); destruct (get' i t1_2); auto. } { elim HC. assert (Hlength: forall n, (n >= brbit')%nat -> Key.testbit prefix n = false) by (inv H7; auto; congruence). assert (Hlength0: forall n, (n >= brbit')%nat -> Key.testbit prefix0 n = false) by (inv H6; auto; congruence). rewrite Hlength; try lia. rewrite Hlength0; lia. } } + simpl. case_eq (Key.ltb brbit brbit0); intros. * case_eq (Key.match_prefix prefix0 prefix brbit); intros; simpl. { case_eq (Key.zerobit prefix0 brbit); intros. - simpl. case_eq (Key.zerobit i brbit); intros. + erewrite IHt1_1; eauto. generalize H; intros HO. inv H. * eapply (wf_Some_Branch HO); eauto. * eapply wf_Some_None; eauto. + inv H; inv H0. * erewrite Key.zerobit_spec in H3; eauto. erewrite Key.zerobit_spec in H4; eauto. apply negb_true_iff in H3. apply negb_false_iff in H4. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) H1). intros HLT. assert (get' i t2_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t2_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t1_2); auto. * erewrite Key.zerobit_spec in H3; eauto. erewrite Key.zerobit_spec in H4; eauto. apply negb_true_iff in H3. apply negb_false_iff in H4. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) H1). intros HLT. assert (get' i t2_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t2_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t1_2); auto. - simpl. case_eq (Key.zerobit i brbit); intros. + inv H; inv H0. * erewrite Key.zerobit_spec in H3; eauto. erewrite Key.zerobit_spec in H4; eauto. apply negb_false_iff in H3. apply negb_true_iff in H4. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) H1). intros HLT. assert (get' i t2_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t2_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t1_1); auto. * erewrite Key.zerobit_spec in H3; eauto. erewrite Key.zerobit_spec in H4; eauto. apply negb_false_iff in H3. apply negb_true_iff in H4. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) H1). intros HLT. assert (get' i t2_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t2_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit0); destruct (get' i t1_1); auto. + erewrite IHt1_2; eauto. generalize H; intros HO. inv H. * eapply (wf_Some_Branch HO); eauto. * eapply wf_Some_None; eauto. } { case_eq (Key.ltb brbit0 brbit); intros. - inv H; inv H0; eapply Key.ltb_spec in H1; eauto; eapply Key.ltb_spec in H3; eauto; lia. - simpl. inv H; inv H0. + generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. unfold join; simpl. case_eq (Key.zerobit prefix (Key.branching_bit prefix prefix0)); intros. * simpl. case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. { assert (get' i t2_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t2_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H4, H6. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } { assert (get' i t1_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. - assert (get' i t1_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. + rewrite H4, H6. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } * simpl. case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. { assert (get' i t1_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. - assert (get' i t1_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. + rewrite H4, H6. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } { assert (get' i t2_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t2_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H4, H6. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } + assert (Hmask': Key.mask prefix brbit = prefix) by (inv H7; auto; congruence). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. unfold join; simpl. case_eq (Key.zerobit prefix (Key.branching_bit prefix prefix0)); intros. * simpl. case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. { assert (get' i t2_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t2_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H4, H5. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } { assert (get' i t1_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. - assert (get' i t1_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_true_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. + rewrite H4, H5. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } * simpl. case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. { assert (get' i t1_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. - assert (get' i t1_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_true_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. congruence. + rewrite H4, H5. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } { assert (get' i t2_1 = None). - rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t2_2 = None). + rewrite Key.branching_bit_sym in HA. erewrite Key.zerobit_spec in H; eauto. erewrite Key.zerobit_spec in H0; eauto. apply negb_false_iff in H; apply negb_false_iff in H0. eapply get_not_same_prefix with (n := n'); eauto. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H4, H5. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } } * simpl. case_eq (Key.ltb brbit0 brbit); intros. { case_eq (Key.match_prefix prefix prefix0 brbit0); intros; simpl. - case_eq (Key.zerobit prefix brbit0); intros. + simpl. case_eq (Key.zerobit i brbit0); intros. * generalize H0; intros HO. inv H0; eapply IHt2_1; eauto. { eapply (wf_Some_Branch HO). } { eapply wf_Some_None; eauto. } * inv H; inv H0. { erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4. apply negb_false_iff in H5. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H2). intros HLT. assert (get' i t1_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t1_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit); destruct (get' i t2_2); auto. } { erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4. apply negb_false_iff in H5. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H2). intros HLT. assert (get' i t1_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t1_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit); destruct (get' i t2_2); auto. } + simpl. case_eq (Key.zerobit i brbit0); intros. * inv H; inv H0. { erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_false_iff in H4. apply negb_true_iff in H5. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H2). intros HLT. assert (get' i t1_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t1_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit); destruct (get' i t2_1); auto. } { erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_false_iff in H4. apply negb_true_iff in H5. generalize (proj1 (Key.ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H2). intros HLT. assert (get' i t1_1 = None). { eapply get_not_same_prefix; eauto. congruence. } assert (get' i t1_2 = None). { eapply get_not_same_prefix; eauto. congruence. } rewrite H, H0. destruct (Key.zerobit i brbit); destruct (get' i t2_1); auto. } * generalize H0; intros HO. inv H0; eapply IHt2_2; eauto. { eapply (wf_Some_Branch HO). } { eapply wf_Some_None; eauto. } - unfold join; simpl. case_eq (Key.zerobit prefix (Key.branching_bit prefix prefix0)); simpl; intros. + case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. * inv H; inv H0. { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t2_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_true_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. - assert (get' i t2_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_true_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } { assert (Hmask'0: Key.mask prefix0 brbit0 = prefix0) by (inv H8; auto; congruence). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t2_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_true_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. - assert (get' i t2_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_true_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } * inv H; inv H0. { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t1_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t1_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } { assert (Hmask'0: Key.mask prefix0 brbit0 = prefix0) by (inv H8; auto; congruence). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t1_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t1_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } + case_eq (Key.zerobit i (Key.branching_bit prefix prefix0)); intros. * inv H; inv H0. { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t1_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t1_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } { assert (Hmask'0: Key.mask prefix0 brbit0 = prefix0) by (inv H8; auto; congruence). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t1_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. - assert (get' i t1_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_true_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto; try congruence. eapply lt_trans; eauto. eapply Key.ltb_spec; eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit0 then get' i t2_1 else get' i t2_2); destruct (Key.zerobit i brbit); auto. } * inv H; inv H0. { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t2_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_false_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. - assert (get' i t2_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_false_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } { assert (Hmask'0: Key.mask prefix0 brbit0 = prefix0) by (inv H8; auto; congruence). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit'0 Hmask'0) H3). intros [Hne [n' [HLT Hbr]]]. generalize (Key.branching_bit_spec _ _ Hne). intros [n'' [HA [HB HC]]]. eapply HA in Hbr. subst n''. assert (get' i t2_1 = None). - erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_false_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. - assert (get' i t2_2 = None). + erewrite Key.zerobit_spec in H4; eauto. erewrite Key.zerobit_spec in H5; eauto. apply negb_false_iff in H4; apply negb_false_iff in H5. eapply get_not_same_prefix with (n := n'); eauto. + rewrite H, H0. destruct (if Key.zerobit i brbit then get' i t1_1 else get' i t1_2); destruct (Key.zerobit i brbit0); auto. } } { inv H; inv H0. - destruct (lt_dec brbit' brbit'0). + generalize (proj2 (Key.ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) l). unfold Key.ltb in H1; intros; congruence. + destruct (eq_nat_dec brbit'0 brbit'). * subst. elim n. apply Key.testbit_spec; intros. case_eq (K.testbit brbit n1); intros. { eapply Hbrbit' in H; eauto. subst n1. symmetry. eapply Hbrbit'0; eauto. } { case_eq (K.testbit brbit0 n1); intros; auto. eapply Hbrbit'0 in H0; eauto. subst n1. generalize (proj2 (Hbrbit' _) eq_refl). congruence. } * assert (brbit'0 < brbit')%nat by lia. generalize (proj2 (Key.ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H). unfold Key.ltb in H2; intros; congruence. - destruct (lt_dec brbit' brbit'0). + generalize (proj2 (Key.ltb_spec _ _ _ _ Hbrbit' Hbrbit'0) l). unfold Key.ltb in H1; intros; congruence. + destruct (eq_nat_dec brbit'0 brbit'). * subst. elim n. apply Key.testbit_spec; intros. case_eq (K.testbit brbit n1); intros. { eapply Hbrbit' in H; eauto. subst n1. symmetry. eapply Hbrbit'0; eauto. } { case_eq (K.testbit brbit0 n1); intros; auto. eapply Hbrbit'0 in H0; eauto. subst n1. generalize (proj2 (Hbrbit' _) eq_refl). congruence. } * assert (brbit'0 < brbit')%nat by lia. generalize (proj2 (Key.ltb_spec _ _ _ _ Hbrbit'0 Hbrbit') H). unfold Key.ltb in H2; intros; congruence. } Qed.
imports: Lia Cdcl.Coqlib