proposition: Lemma updater_snd: forall (A B: Type) acc (f:A -> B) g (j: key) o (m: ptrie A) (WF: wf o m), snd (updater f g acc j m) = match get' j m with | None => acc | Some j => f j end.
proof: Proof. induction 1; simpl; intros. - reflexivity. - destruct (eqb j k);auto. destruct (g (f v)); auto. - destruct (eqb j k);auto. destruct (g (f v)); auto. - destruct (match_prefix j prefix brbit)eqn:EQ; auto. { destruct (zerobit j brbit)eqn:Z. + destruct (updater f g acc j l). simpl in *. congruence. + destruct (updater f g acc j r). simpl in *. congruence. } { eapply match_prefix_spec' in EQ; eauto. destruct EQ as [HO [n [HA HB]]]. simpl. destruct (zerobit j brbit)eqn:Z. assert (get' j l = None). { eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB. subst; auto. } rewrite H ; auto. assert (get' j r = None). { eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB. subst; auto. } rewrite H ; auto. } - destruct (match_prefix j prefix brbit)eqn:EQ; auto. { destruct (zerobit j brbit)eqn:Z. + destruct (updater f g acc j l). simpl in *. congruence. + destruct (updater f g acc j r). simpl in *. congruence. } { eapply match_prefix_spec' in EQ; eauto. destruct EQ as [HO [n [HA HB]]]. simpl. destruct (zerobit j brbit)eqn:Z. assert (get' j l = None). { eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB. subst; auto. } rewrite H ; auto. assert (get' j r = None). { eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB. subst; auto. } rewrite H ; auto. inv WF1 ; auto. inv WF2 ; auto. congruence. } Qed.
imports: List Bool ZArith Lia