proposition: Lemma wf_set': forall A opt k x (t: ptrie A), wf opt t -> wf opt (Leaf k x) -> wf opt (set' k x t).
proof: Proof. induction 1; intros. - simpl; auto. - simpl. destruct (eqb k k0) eqn:EQ; auto. rewrite eqb_false in EQ. eapply wf_join_Leaf; eauto; try constructor; auto. - simpl. destruct (eqb k k0) eqn:EQ; auto. rewrite eqb_false in EQ. eapply wf_join_Leaf; eauto; try constructor; auto. - simpl. case_eq (match_prefix k prefix brbit); intros. + case_eq (zerobit k brbit); intros; econstructor; trivial; try eassumption. * eapply set'_not_empty; eauto. * apply IHwf1. constructor; auto. intros; symmetry. eapply match_prefix_spec; eauto. * eapply set'_not_empty; eauto. * apply IHwf2. constructor; auto. intros; symmetry. eapply match_prefix_spec; eauto. + generalize H2. intros HX. eapply (match_prefix_spec') in H2; eauto. destruct H2 as [HO [n [HA HB]]]. eapply wf_join_Branch; eauto. econstructor; trivial; try eassumption. - simpl. case_eq (match_prefix k prefix brbit); intros. + case_eq (zerobit k brbit); intros; econstructor; trivial; try eassumption. * eapply set'_not_empty; eauto. * apply IHwf1. constructor; auto. inv H; congruence. intros; symmetry. eapply match_prefix_spec; eauto. inv H; congruence. * eapply set'_not_empty; eauto. * apply IHwf2. constructor; auto. inv H; congruence. intros; symmetry. eapply match_prefix_spec; eauto. inv H; congruence. + generalize H2; intros HX. eapply (match_prefix_spec') in H2; eauto. destruct H2 as [n [HA HB]]. eapply wf_join_Branch; eauto; try econstructor; trivial; try eassumption. inv H; congruence. Qed.
imports: List Bool ZArith Lia