proposition: Lemma gus: forall (A: Type) f opt (i: key) (m: ptrie A), wf opt m -> get' i (update f i m) = match get' i m with | None => None | Some v => f v end.
proof: Proof. induction 1; intros. - reflexivity. - simpl. rewrite! eqb_is_dec ; destruct (eq i k); simpl; auto. destruct (f v); simpl; auto. rewrite eqb_refl; reflexivity. rewrite eqb_is_dec. destruct (eq i k); simpl; congruence. - simpl. rewrite eqb_is_dec; destruct (eq i k); simpl; auto. destruct (f v); simpl; auto. rewrite eqb_refl; reflexivity. rewrite eqb_is_dec; destruct (eq i k); simpl;congruence. - simpl. case_eq (match_prefix i prefix brbit); intros. + case_eq (zerobit i brbit); intros. * unfold branch. case_eq (update f i l); intros. { rewrite H3 in *. simpl in IHwf1. rewrite <- IHwf1. eapply get_not_same_lr; eauto. } { rewrite <- H3. destruct r; auto. - simpl. rewrite H2; auto. - simpl. rewrite H2; auto. } { rewrite <- H3. destruct r; auto. - simpl. rewrite H2; auto. - simpl. rewrite H2; auto. } * unfold branch. destruct l; auto. { case_eq (update f i r); intros. - simpl. rewrite eqb_is_dec ; destruct (eq i k); auto. subst i. inv H; congruence. simpl. rewrite H3 in IHwf2; simpl; auto. - rewrite <- H3. simpl. rewrite H2. auto. - rewrite <- H3. simpl. rewrite H2. auto. } { case_eq (update f i r); intros. - rewrite H3 in IHwf2. simpl in IHwf2. rewrite <- IHwf2. inv H; simpl. case_eq (zerobit i brbit0); intros; eapply get_not_same_prefix; eauto. + erewrite zerobit_spec in Hlr0; eauto. erewrite zerobit_spec in H2; eauto. rewrite negb_true_iff in Hlr0. rewrite negb_false_iff in H2. congruence. + erewrite zerobit_spec in Hlr0; eauto. erewrite zerobit_spec in H2; eauto. rewrite negb_true_iff in Hlr0. rewrite negb_false_iff in H2. congruence. - rewrite <- H3. simpl. rewrite H2. auto. - rewrite <- H3. simpl. rewrite H2. auto. } + eapply match_prefix_spec' in H1; eauto. destruct H1 as [HO [n [HA HB]]]. simpl. case_eq (zerobit i brbit); intros. * assert (get' i 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 H2. reflexivity. * assert (get' i 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 H2; reflexivity. - simpl. case_eq (match_prefix i prefix brbit); intros. + case_eq (zerobit i brbit); intros. * unfold branch. case_eq (update f i l); intros. { rewrite H3 in IHwf1. rewrite <- IHwf1. simpl. eapply get_not_same_lr; eauto. } { rewrite <- H3. destruct r; auto. - simpl. rewrite H2; auto. - simpl. rewrite H2; auto. } { rewrite <- H3. destruct r; auto. - simpl. rewrite H2; auto. - simpl. rewrite H2; auto. } * unfold branch. destruct l; auto. { case_eq (update f i r); intros. - simpl. rewrite eqb_is_dec ; destruct (eq i k); auto. subst i. inv H; congruence. simpl. rewrite <- IHwf2. rewrite H3. reflexivity. - rewrite <- H3. simpl. rewrite H2. auto. - rewrite <- H3. simpl. rewrite H2. auto. } { case_eq (update f i r); intros. - rewrite <- IHwf2. rewrite H3. simpl. inv H; simpl. case_eq (zerobit i brbit0); intros; eapply get_not_same_prefix; eauto. + erewrite zerobit_spec in Hlr; eauto. erewrite zerobit_spec in H2; eauto. rewrite negb_true_iff in Hlr. rewrite negb_false_iff in H2. congruence. + erewrite zerobit_spec in Hlr; eauto. erewrite zerobit_spec in H2; eauto. rewrite negb_true_iff in Hlr. rewrite negb_false_iff in H2. congruence. - rewrite <- H3. simpl. rewrite H2. auto. - rewrite <- H3. simpl. rewrite H2. auto. } + eapply match_prefix_spec' in H1; auto. destruct H1 as [HO [n [HA HB]]]. simpl. case_eq (zerobit i brbit); intros. * assert (get' i 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 H2 ; reflexivity. * assert (get' i 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 H2;reflexivity. * inv H; auto; congruence. * inv H; auto; congruence. Qed.
imports: List Bool ZArith Lia