proposition: Lemma beq_correct': forall (A B: Type) (eq_elt: A -> B -> bool) (t1: ptrie A) (t2: ptrie B) opt, wf opt t1 -> wf opt t2 -> beq' eq_elt t1 t2 = true <-> (forall (x: key), match get' x t1, get' x t2 with | None, None => True | Some y1, Some y2 => eq_elt y1 y2 = true | _, _ => False end).
proof: Proof. induction t1; intros; split; intros. { simpl in H1. destruct t2; inv H1. simpl; reflexivity. } { simpl in H1. generalize (proj1 (bempty H0)). intros HA. erewrite HA; simpl; auto. intros; generalize (H1 x); destruct (get' x t2); tauto. } { destruct t2; simpl in H1; inv H1. simpl. destruct_eq k k0; simpl in H3; inv H3. destruct_eq x k0; simpl; auto. rewrite H2. reflexivity. } { simpl in H1. destruct t2. - generalize (H1 k); rewrite eqb_refl; simpl; tauto. - generalize (H1 k); rewrite eqb_refl; simpl; try congruence. destruct_eq k k0; tauto. - generalize (H1 k); rewrite eqb_refl; simpl; try congruence. case_eq (zerobit k brbit); intros. + assert (t2_2 <> Empty) by (inv H0; auto). assert (exists o, wf o t2_2) by (inv H0; eauto). destruct H5. generalize (not_empty_get' H5 H4). intros [k' [v' HA]]. generalize (H1 k'); simpl. assert (get' k t2_2 = None) by (inv H0; eapply get_not_same_lr; eauto). destruct_eq k' k; try congruence. rewrite HA; case_eq (zerobit k' brbit); intros; try tauto. assert (get' k' t2_2 = None) by (inv H0; eapply get_not_same_lr; eauto). congruence. + assert (t2_1 <> Empty) by (inv H0; auto). assert (exists o, wf o t2_1) by (inv H0; eauto). destruct H5. generalize (not_empty_get' H5 H4). intros [k' [v' HA]]. generalize (H1 k'); simpl. assert (get' k t2_1 = None) by (inv H0; eapply get_not_same_lr; eauto). destruct_eq k' k; try congruence. rewrite HA; case_eq (zerobit k' brbit); intros; try tauto. assert (get' k' t2_1 = None) by (inv H0; eapply get_not_same_lr; eauto). congruence. } { destruct t2; simpl in H1; inv H1. destruct_eq prefix prefix0; destruct_eq brbit brbit0; simpl in H3; inv H3. simpl. rewrite H2. apply andb_true_iff in H2. destruct H2. rewrite H1. rewrite H2. inv H; inv H0. - generalize (is_mask_same Hbrbit' Hbrbit'0). intros; subst brbit'0. generalize (proj1 (IHt1_1 _ _ H6 H4) H1); intros HA. generalize (proj1 (IHt1_2 _ _ H9 H13) H2); intros HB. case_eq (zerobit x brbit0); intros. + apply HA. + apply HB. - generalize (is_mask_same Hbrbit' Hbrbit'0). intros; subst brbit'0. generalize (proj1 (IHt1_1 _ _ H6 H5) H1); intros HA. generalize (proj1 (IHt1_2 _ _ H9 H8) H2); intros HB. case_eq (zerobit x brbit0); intros. + apply HA. + apply HB. } { destruct t2; simpl in H1. - generalize (not_empty_get' H ltac:(congruence)). intros [k [v HA]]. simpl in HA. generalize (H1 k); simpl in HA; rewrite HA; tauto. - case_eq (zerobit k brbit); intros. + assert (HA: t1_2 <> Empty) by (inv H; auto). assert (HB: exists o, wf o t1_2) by (inv H; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB HA). intros [k' [v' HC]]. generalize (H1 k'). rewrite HC. case_eq (zerobit k' brbit); intros. * assert (get' k' t1_2 = None) by (inv H; eapply get_not_same_lr; eauto). congruence. * destruct_eq k' k; try congruence; tauto. + assert (HA: t1_1 <> Empty) by (inv H; auto). assert (HB: exists o, wf o t1_1) by (inv H; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB HA). intros [k' [v' HC]]. generalize (H1 k'). rewrite HC. case_eq (zerobit k' brbit); intros. * destruct_eq k' k; try congruence; tauto. * assert (get' k' t1_1 = None) by (inv H; eapply get_not_same_lr; eauto). congruence. - destruct (eq prefix prefix0). + subst prefix0. assert (Hbrbit: exists brbit', is_mask brbit brbit' /\ (forall n, (n >= brbit')%nat -> testbit prefix n = false)) by (inv H; eauto). destruct Hbrbit as [brbit' [Hbrbit Hprefix]]. assert (Hbrbit0: exists brbit0', is_mask brbit0 brbit0' /\ (forall n, (n >= brbit0')%nat -> testbit prefix n = false)) by (inv H0; eauto). destruct Hbrbit0 as [brbit0' [Hbrbit0 Hprefix']]. assert (Hmask: mask prefix brbit = prefix). { eapply testbit_spec. intros. generalize (mask_spec prefix _ _ Hbrbit). intros [HA HB]. destruct (lt_dec n brbit'). - apply HA; auto. - rewrite Hprefix; try lia. rewrite HB; auto; lia. } assert (Hmask': mask prefix brbit0 = prefix). { eapply testbit_spec. intros. generalize (mask_spec prefix _ _ Hbrbit0). intros [HA HB]. destruct (lt_dec n brbit0'). - apply HA; auto. - rewrite Hprefix'; try lia. rewrite HB; auto; lia. } destruct (Nat.eq_dec brbit' brbit0'). * subst brbit0'. generalize (is_mask_same' Hbrbit0 Hbrbit). intros; subst brbit0. simpl. destruct_eq prefix prefix; try congruence. destruct_eq brbit brbit; try congruence; simpl. assert (Ho1: exists o1, wf o1 t1_1 /\ wf o1 t2_1) by (inv H; inv H0; generalize (is_mask_same Hbrbit'0 Hbrbit'); intros; subst; eauto). assert (Ho2: exists o2, wf o2 t1_2 /\ wf o2 t2_2) by (inv H; inv H0; generalize (is_mask_same Hbrbit'0 Hbrbit'); intros; subst; eauto). destruct Ho1 as [o1 [HA HB]]. destruct Ho2 as [o2 [HC HD]]. rewrite (proj2 (IHt1_1 _ _ HA HB)), (proj2 (IHt1_2 _ _ HC HD)); simpl; auto. { intros. generalize (H1 x). case_eq (zerobit x brbit); intros. - assert (get' x t1_2 = None) by (inv H; eapply get_not_same_lr; eauto). assert (get' x t2_2 = None) by (inv H0; eapply get_not_same_lr; eauto). rewrite H4, H5. auto. - auto. } { intros. generalize (H1 x). case_eq (zerobit x brbit); intros. - auto. - assert (get' x t1_1 = None) by (inv H; eapply get_not_same_lr; eauto). assert (get' x t2_1 = None) by (inv H0; eapply get_not_same_lr; eauto). rewrite H4, H5. auto. } * assert (brbit' < brbit0' \/ brbit0' < brbit')%nat by lia. destruct H2. { assert (HA: testbit prefix brbit' = false) by (eapply Hprefix; lia). assert (Ht1_2: t1_2 <> Empty) by (inv H; assumption). assert (HB: exists o, wf o t1_2) by (inv H; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB Ht1_2). intros [k [v HC]]. case_eq (zerobit k brbit); intros. - assert (get' k t1_2 = None) by (inv H; eapply get_not_same_lr; eauto). congruence. - generalize (H1 k); rewrite H3; rewrite HC. case_eq (get' k (Branch prefix brbit0 t2_1 t2_2)); intros. + generalize (get_some_implies H0 H4 _ Hbrbit0 _ H2). intros HD. erewrite zerobit_spec in H3; eauto. rewrite HD in H3. rewrite HA in H3. simpl in H3. congruence. + simpl in H4. rewrite H4 in H5. elim H5. } { assert (HA: testbit prefix brbit0' = false) by (eapply Hprefix'; lia). assert (Ht2_2: t2_2 <> Empty) by (inv H0; assumption). assert (HB: exists o, wf o t2_2) by (inv H0; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB Ht2_2). intros [k [v HC]]. case_eq (zerobit k brbit0); intros. - assert (get' k t2_2 = None) by (inv H0; eapply get_not_same_lr; eauto). congruence. - generalize (H1 k); rewrite H3; rewrite HC. case_eq (get' k (Branch prefix brbit t1_1 t1_2)); intros. + generalize (get_some_implies H H4 _ Hbrbit _ H2). intros HD. erewrite zerobit_spec in H3; eauto. rewrite HD in H3. rewrite HA in H3. simpl in H3. congruence. + simpl in H4. rewrite H4 in H5. elim H5. } + assert (Hbrbit: exists brbit', is_mask brbit brbit' /\ (forall n, (n >= brbit')%nat -> testbit prefix n = false)) by (inv H; eauto). destruct Hbrbit as [brbit' [Hbrbit Hprefix]]. assert (Hbrbit0: exists brbit0', is_mask brbit0 brbit0' /\ (forall n, (n >= brbit0')%nat -> testbit prefix0 n = false)) by (inv H0; eauto). destruct Hbrbit0 as [brbit0' [Hbrbit0 Hprefix']]. assert (Hmask: mask prefix brbit = prefix). { eapply testbit_spec. intros. generalize (mask_spec prefix _ _ Hbrbit). intros [HA HB]. destruct (lt_dec n0 brbit'). - apply HA; auto. - rewrite Hprefix; try lia. rewrite HB; auto; lia. } assert (Hmask': mask prefix0 brbit0 = prefix0). { eapply testbit_spec. intros. generalize (mask_spec prefix0 _ _ Hbrbit0). intros [HA HB]. destruct (lt_dec n0 brbit0'). - apply HA; auto. - rewrite Hprefix'; try lia. rewrite HB; auto; lia. } destruct (lt_dec brbit' brbit0'). * case_eq (testbit prefix0 brbit'); intros. { assert (HA: t1_1 <> Empty) by (inv H; auto). assert (HB: exists o, wf o t1_1) by (inv H; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB HA). intros [k' [v' HC]]. generalize (H1 k'). rewrite HC. case_eq (zerobit k' brbit); intros. - case_eq (get' k' (Branch prefix0 brbit0 t2_1 t2_2)); intros. + generalize (get_some_implies H0 H5 _ Hbrbit0 _ l). intros. erewrite zerobit_spec in H3; eauto. eapply negb_true_iff in H3. rewrite H6 in H3. rewrite H2 in H3. congruence. + simpl in H5; rewrite H5 in H4. elim H4. - assert (get' k' t1_1 = None) by (inv H; eapply get_not_same_lr; eauto). congruence. } { assert (HA: t1_2 <> Empty) by (inv H; auto). assert (HB: exists o, wf o t1_2) by (inv H; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB HA). intros [k' [v' HC]]. generalize (H1 k'). rewrite HC. case_eq (zerobit k' brbit); intros. - assert (get' k' t1_2 = None) by (inv H; eapply get_not_same_lr; eauto). congruence. - case_eq (get' k' (Branch prefix0 brbit0 t2_1 t2_2)); intros. + generalize (get_some_implies H0 H5 _ Hbrbit0 _ l). intros. erewrite zerobit_spec in H3; eauto. eapply negb_false_iff in H3. rewrite H6 in H3. rewrite H2 in H3. congruence. + simpl in H5; rewrite H5 in H4. elim H4. } * destruct (lt_dec brbit0' brbit'). { case_eq (testbit prefix brbit0'); intros. { assert (HA: t2_1 <> Empty) by (inv H0; auto). assert (HB: exists o, wf o t2_1) by (inv H0; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB HA). intros [k' [v' HC]]. generalize (H1 k'). rewrite HC. case_eq (zerobit k' brbit0); intros. - case_eq (get' k' (Branch prefix brbit t1_1 t1_2)); intros. + generalize (get_some_implies H H5 _ Hbrbit _ l). intros. erewrite zerobit_spec in H3; eauto. eapply negb_true_iff in H3. rewrite H6 in H3. rewrite H2 in H3. congruence. + simpl in H5; rewrite H5 in H4. elim H4. - assert (get' k' t2_1 = None) by (inv H0; eapply get_not_same_lr; eauto). congruence. } { assert (HA: t2_2 <> Empty) by (inv H0; auto). assert (HB: exists o, wf o t2_2) by (inv H0; eauto). destruct HB as [o HB]. generalize (not_empty_get' HB HA). intros [k' [v' HC]]. generalize (H1 k'). rewrite HC. case_eq (zerobit k' brbit0); intros. - assert (get' k' t2_2 = None) by (inv H0; eapply get_not_same_lr; eauto). congruence. - case_eq (get' k' (Branch prefix brbit t1_1 t1_2)); intros. + generalize (get_some_implies H H5 _ Hbrbit _ l). intros. erewrite zerobit_spec in H3; eauto. eapply negb_false_iff in H3. rewrite H6 in H3. rewrite H2 in H3. congruence. + simpl in H5; rewrite H5 in H4. elim H4. } } { assert (brbit0' = brbit') by lia. subst. clear n1; clear n0. generalize (branching_bit_spec _ _ n). intros [p [HA [HB HC]]]. generalize (not_empty_get' H ltac:(congruence)). intros [k [v HD]]. assert (p < brbit')%nat. { destruct (lt_dec p brbit'); auto. rewrite Hprefix in HC; try lia. rewrite Hprefix' in HC; try congruence; lia. } generalize (get_some_implies H HD _ Hbrbit _ H2). intros HE. generalize (H1 k). simpl in HD; rewrite HD. generalize (is_mask_same' Hbrbit Hbrbit0). intros; subst. case_eq (get' k (Branch prefix0 brbit0 t2_1 t2_2)); intros. - generalize (get_some_implies H0 H3 _ Hbrbit _ H2). intros HF. elim HC; congruence. - simpl in H3; rewrite H3 in H4. elim H4. } } Qed.
imports: List Bool ZArith Lia