proposition: Lemma gis': forall (A: Type) opt c (i: key) (x: A) (m: ptrie A), wf opt m -> get' i (insert' c i x m) = match get' i m with | None => Some x | Some y => Some (c x y) end.
proof: Proof. induction 1; intros. - simpl. rewrite (eqb_refl); congruence. - simpl. repeat rewrite eqb_is_dec ; destruct (eq i k); auto. + simpl; rewrite eqb_refl; congruence. + unfold join. generalize (branching_bit_spec _ _ n). intros [m' [HA HB]]. case_eq (zerobit i (branching_bit i k)); intros; simpl; rewrite H; rewrite eqb_is_dec ; destruct (eq i i); simpl; congruence. - simpl. repeat rewrite eqb_is_dec ; destruct (eq i k); auto. + simpl; rewrite eqb_refl; congruence. + unfold join. case_eq (zerobit i (branching_bit i k)); intros; simpl; rewrite H; rewrite (eqb_refl); congruence. - simpl. case_eq (match_prefix i prefix brbit); intros. + case_eq (zerobit i brbit); intros; simpl; rewrite H2; auto. + generalize (proj1 (match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H1). intros [Hne [n [HA HB]]]. generalize (branching_bit_spec _ _ Hne). intros [n' [HX [HY HZ]]]. eapply HX in HB; subst. unfold join. case_eq (zerobit i (branching_bit i prefix)); intros; simpl; rewrite H2; rewrite eqb_refl ; try congruence. * case_eq (zerobit i brbit); intros. { assert (get' i l = None). - eapply get_not_same_prefix; eauto. - rewrite H4; auto. } { assert (get' i r = None). - eapply get_not_same_prefix; eauto. - rewrite H4; auto. } * case_eq (zerobit i brbit); intros. { assert (get' i l = None). - eapply get_not_same_prefix; eauto. - rewrite H4; auto. } { assert (get' i r = None). - eapply get_not_same_prefix; eauto. - rewrite H4; auto. } - simpl. case_eq (match_prefix i prefix brbit); intros. + case_eq (zerobit i brbit); intros; simpl; rewrite H2; auto. + unfold join. eapply match_prefix_spec' in H1; auto. * destruct H1 as [HO [n [HA HB]]]. case_eq (zerobit i (branching_bit i prefix)); intros; simpl; rewrite H1; rewrite (eqb_refl); try congruence. { generalize (branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB; subst. case_eq (zerobit i brbit); intros. - assert (get' i l = None). + eapply get_not_same_prefix; eauto. + rewrite H3; auto. - assert (get' i r = None). + eapply get_not_same_prefix; eauto. + rewrite H3; auto. } { generalize (branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB; subst. case_eq (zerobit i brbit); intros. - assert (get' i l = None). + eapply get_not_same_prefix; eauto. + rewrite H3; auto. - assert (get' i r = None). + eapply get_not_same_prefix; eauto. + rewrite H3; auto. } * inv H; auto; congruence. * inv H; auto; congruence. Qed.
imports: List Bool ZArith Lia