proposition: Lemma gso': forall (A: Type) opt (i j: elt) (x: A) (m: ptrie A), wf opt m -> i <> j -> get' i (set' j x m) = get' i m.
proof: Proof. induction 1; intros. - simpl. rewrite elt_eqb_is_dec. destruct (elt_eq i j); simpl ; congruence. - simpl. rewrite! elt_eqb_is_dec. destruct (elt_eq j k); simpl; auto. + simpl. rewrite elt_eqb_is_dec. destruct (elt_eq i k); destruct (elt_eq i j); simpl ; congruence. + unfold join. case_eq (Key.zerobit j (Key.branching_bit j k)); intros; simpl; case_eq (Key.zerobit i (Key.branching_bit j k)); intros; simpl; repeat rewrite elt_eqb_is_dec ; destruct (elt_eq i j); destruct (elt_eq i k); simpl; try congruence. * subst i. generalize (Key.branching_bit_spec j k n). intros [n' [HA [HB HC]]]. elim HC. erewrite Key.zerobit_spec in H0; eauto. erewrite Key.zerobit_spec in H1; eauto. eapply negb_true_iff in H0. eapply negb_true_iff in H1. congruence. * subst i. generalize (Key.branching_bit_spec j k n). intros [n' [HA [HB HC]]]. elim HC. erewrite Key.zerobit_spec in H0; eauto. erewrite Key.zerobit_spec in H1; eauto. eapply negb_false_iff in H0. eapply negb_false_iff in H1. congruence. - simpl. repeat rewrite elt_eqb_is_dec. destruct (elt_eq j k); simpl; auto. + simpl. rewrite elt_eqb_is_dec. destruct (elt_eq i k); destruct (elt_eq i j); simpl; congruence. + unfold join. case_eq (Key.zerobit j (Key.branching_bit j k)); intros; simpl; case_eq (Key.zerobit i (Key.branching_bit j k)); intros; simpl; rewrite elt_eqb_is_dec ; destruct (elt_eq i j); destruct (elt_eq i k); simpl; try congruence. * subst i. generalize (Key.branching_bit_spec j k n). intros [n' [HA [HB HC]]]. elim HC. erewrite Key.zerobit_spec in H0; eauto. erewrite Key.zerobit_spec in H1; eauto. eapply negb_true_iff in H0. eapply negb_true_iff in H1. congruence. * subst i. generalize (Key.branching_bit_spec j k n). intros [n' [HA [HB HC]]]. elim HC. erewrite Key.zerobit_spec in H0; eauto. erewrite Key.zerobit_spec in H1; eauto. eapply negb_false_iff in H0. eapply negb_false_iff in H1. congruence. - simpl. case_eq (Key.match_prefix j prefix brbit); intros. + case_eq (Key.zerobit j brbit); intros; simpl; destruct (Key.zerobit i brbit); simpl; auto. + unfold join. case_eq (Key.zerobit j (Key.branching_bit j prefix)); intros; simpl; case_eq (Key.zerobit i (Key.branching_bit j prefix)); intros; simpl; repeat rewrite elt_eqb_is_dec ; destruct (elt_eq i j); simpl; try congruence. * case_eq (Key.zerobit i brbit); intros. { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_true_iff in H3. rewrite negb_true_iff in H4. congruence. } { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_true_iff in H3. rewrite negb_true_iff in H4. congruence. } * case_eq (Key.zerobit i brbit); intros. { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_false_iff in H3. rewrite negb_false_iff in H4. congruence. } { generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_false_iff in H3. rewrite negb_false_iff in H4. congruence. } - simpl. case_eq (Key.match_prefix j prefix brbit); intros. + case_eq (Key.zerobit j brbit); intros; simpl; destruct (Key.zerobit i brbit); simpl; auto. + unfold join. case_eq (Key.zerobit j (Key.branching_bit j prefix)); intros; simpl; case_eq (Key.zerobit i (Key.branching_bit j prefix)); intros; simpl; repeat rewrite elt_eqb_is_dec ; destruct (elt_eq i j); try congruence. * case_eq (Key.zerobit i brbit); intros. { assert (Hmask' : Key.mask prefix brbit = prefix) by (inv H; try congruence; auto). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_true_iff in H3. rewrite negb_true_iff in H4. congruence. } { assert (Hmask' : Key.mask prefix brbit = prefix) by (inv H; try congruence; auto). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_true_iff in H3. rewrite negb_true_iff in H4. congruence. } * case_eq (Key.zerobit i brbit); intros. { assert (Hmask' : Key.mask prefix brbit = prefix) by (inv H; try congruence; auto). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_false_iff in H3. rewrite negb_false_iff in H4. congruence. } { assert (Hmask' : Key.mask prefix brbit = prefix) by (inv H; try congruence; auto). generalize (proj1 (Key.match_prefix_spec' _ _ _ _ Hbrbit' Hmask') H2). intros [HO [n0 [HP HQ]]]. symmetry; eapply get_not_same_prefix; eauto. generalize (Key.branching_bit_spec _ _ HO). intros [n1 [HX [HY HZ]]]. eapply HX in HQ. subst n1. rewrite (Key.zerobit_spec _ _ _ HX) in H3. rewrite (Key.zerobit_spec _ _ _ HX) in H4. rewrite negb_false_iff in H3. rewrite negb_false_iff in H4. congruence. } Qed.
imports: Lia Cdcl.Coqlib