proposition: Lemma ptrie_extensional: forall (A: Type) (t1 t2: ptrie A) o, wf o t1 -> wf o t2 -> (forall k, get' k t1 = get' k t2) -> t1 = t2.
proof: Proof. induction t1; intros. - destruct t2; auto. + generalize (H1 k); simpl; intros. rewrite eqb_refl in H2; congruence. + generalize (not_empty_get' H0 ltac:(congruence)). intros [k [v HA]]. rewrite <- H1 in HA. simpl in HA; congruence. - destruct t2. + generalize (H1 k); simpl; intros. rewrite eqb_refl in H2; congruence. + generalize (H1 k); generalize (H1 k0); simpl. rewrite! eqb_refl; destruct_eq k0 k; destruct_eq k k0; congruence. + assert (Ht2_1: t2_1 <> Empty) by (inv H0; auto). assert (Ht2_2: t2_2 <> Empty) by (inv H0; auto). assert (Ho1: exists o1, wf o1 t2_1) by (inv H0; eauto). destruct Ho1 as [o1 Ho1]. assert (Ho2: exists o2, wf o2 t2_2) by (inv H0; eauto). destruct Ho2 as [o2 Ho2]. generalize (H1 k); simpl; destruct (eq k k); try congruence; intros. apply eq_sym in H2. case_eq (zerobit k brbit); intros; rewrite H3 in H2. * generalize (not_empty_get' Ho2 Ht2_2). intros [k' [v' HA]]. case_eq (zerobit k' brbit); intros. { assert (get' k' t2_2 = None) by (inv H0; eapply get_not_same_lr; eauto); congruence. } { generalize (H1 k'); simpl. destruct_eq k' k; try congruence. rewrite H4; congruence. } * generalize (not_empty_get' Ho1 Ht2_1). intros [k' [v' HA]]. case_eq (zerobit k' brbit); intros. { generalize (H1 k'); simpl. destruct_eq k' k; try congruence. rewrite H4; congruence. } { assert (get' k' t2_1 = None) by (inv H0; eapply get_not_same_lr; eauto); congruence. } - destruct t2. + generalize (not_empty_get' H ltac:(congruence)). intros [k [v HA]]. rewrite H1 in HA; simpl in HA; congruence. + assert (Ht1_1: t1_1 <> Empty) by (inv H; auto). assert (Ht1_2: t1_2 <> Empty) by (inv H; auto). assert (Ho1: exists o1, wf o1 t1_1) by (inv H; eauto). destruct Ho1 as [o1 Ho1]. assert (Ho2: exists o2, wf o2 t1_2) by (inv H; eauto). destruct Ho2 as [o2 Ho2]. generalize (H1 k); simpl; destruct (eq k k); try congruence; intros. case_eq (zerobit k brbit); intros; rewrite H3 in H2. * generalize (not_empty_get' Ho2 Ht1_2). intros [k' [v' HA]]. 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'); simpl. destruct_eq k' k; try congruence. rewrite H4; congruence. } * generalize (not_empty_get' Ho1 Ht1_1). intros [k' [v' HA]]. case_eq (zerobit k' brbit); intros. { generalize (H1 k'); simpl. destruct_eq k' k; try congruence. rewrite H4; congruence. } { assert (get' k' t1_1 = None) by (inv H; eapply get_not_same_lr; eauto); congruence. } + generalize (proj2 (beq_correct' _ _ (fun a b => true) _ _ _ H H0) ltac:(intros; rewrite H1; destruct (get' x (Branch prefix0 brbit0 t2_1 t2_2)); auto)). intros. simpl in H2. destruct_eq prefix prefix0; simpl in H2; try congruence. subst prefix0. destruct_eq brbit brbit0; simpl in H2; try congruence. subst brbit0. f_equal; auto. * inv H; inv H0; eapply IHt1_1; eauto. { assert (brbit'0 = brbit') by (eapply is_mask_same; eauto). subst brbit'0. eauto. } { intros. generalize (H1 k); simpl. case_eq (zerobit k brbit); intros; auto. erewrite ! (get_not_same_lr); eauto. } { assert (brbit'0 = brbit') by (eapply is_mask_same; eauto). subst brbit'0. eauto. } { intros. generalize (H1 k); simpl. case_eq (zerobit k brbit); intros; auto. erewrite ! (get_not_same_lr); eauto. } * inv H; inv H0; eapply IHt1_2; eauto. { assert (brbit'0 = brbit') by (eapply is_mask_same; eauto). subst brbit'0. eauto. } { intros. generalize (H1 k); simpl. case_eq (zerobit k brbit); intros; auto. erewrite ! (get_not_same_lr); eauto. } { assert (brbit'0 = brbit') by (eapply is_mask_same; eauto). subst brbit'0. eauto. } { intros. generalize (H1 k); simpl. case_eq (zerobit k brbit); intros; auto. erewrite ! (get_not_same_lr); eauto. } Qed.
imports: List Bool ZArith Lia