proposition: Lemma grs': forall (A: Type) opt (i: elt) (m: ptrie A), wf opt m -> get' i (remove' i m) = None.
proof: Proof. induction 1; intros. - reflexivity. - simpl. rewrite! elt_eqb_is_dec ; destruct (elt_eq k i); simpl; auto. rewrite elt_eqb_is_dec. destruct (elt_eq i k); simpl; congruence. - simpl. rewrite elt_eqb_is_dec; destruct (elt_eq k i); simpl; auto. rewrite elt_eqb_is_dec; destruct (elt_eq i k); simpl;congruence. - simpl. case_eq (Key.match_prefix i prefix brbit); intros. + case_eq (Key.zerobit i brbit); intros. * unfold branch. case_eq (remove' i l); intros. { 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 (remove' i r); intros. - simpl. rewrite elt_eqb_is_dec ; destruct (elt_eq i k); auto. subst i. inv H; congruence. - rewrite <- H3. simpl. rewrite H2. auto. - rewrite <- H3. simpl. rewrite H2. auto. } { case_eq (remove' i r); intros. - inv H; simpl. case_eq (Key.zerobit i brbit0); intros; eapply get_not_same_prefix; eauto. + erewrite Key.zerobit_spec in Hlr0; eauto. erewrite Key.zerobit_spec in H2; eauto. rewrite negb_true_iff in Hlr0. rewrite negb_false_iff in H2. congruence. + erewrite Key.zerobit_spec in Hlr0; eauto. erewrite Key.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 Key.match_prefix_spec' in H1; auto. destruct H1 as [HO [n [HA HB]]]. simpl. case_eq (Key.zerobit i brbit); intros. * eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (Key.branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB; subst; auto. * eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (Key.branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB; subst; auto. * assumption. - simpl. case_eq (Key.match_prefix i prefix brbit); intros. + case_eq (Key.zerobit i brbit); intros. * unfold branch. case_eq (remove' i l); intros. { 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 (remove' i r); intros. - simpl. rewrite elt_eqb_is_dec ; destruct (elt_eq i k); auto. subst i. inv H; congruence. - rewrite <- H3. simpl. rewrite H2. auto. - rewrite <- H3. simpl. rewrite H2. auto. } { case_eq (remove' i r); intros. - inv H; simpl. case_eq (Key.zerobit i brbit0); intros; eapply get_not_same_prefix; eauto. + erewrite Key.zerobit_spec in Hlr; eauto. erewrite Key.zerobit_spec in H2; eauto. rewrite negb_true_iff in Hlr. rewrite negb_false_iff in H2. congruence. + erewrite Key.zerobit_spec in Hlr; eauto. erewrite Key.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 Key.match_prefix_spec' in H1; auto. destruct H1 as [HO [n [HA HB]]]. simpl. case_eq (Key.zerobit i brbit); intros. * eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (Key.branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB; subst; auto. * eapply get_not_same_prefix; eauto. apply not_eq_sym. generalize (Key.branching_bit_spec _ _ HO). intros [n' [HX [HY HZ]]]. eapply HX in HB; subst; auto. * inv H; auto; congruence. * inv H; auto; congruence. Qed.
imports: Lia Cdcl.Coqlib