proposition: Lemma wf_branch: forall A prefix brb brb' lr p m m' (t1 t2: ptrie A) (Hlr: Key.zerobit p brb = lr) (Hincr: (brb' < m')%nat) (Hbrb: Key.is_mask brb brb') (Hlength: forall n, (n >= brb')%nat -> Key.testbit prefix n = false) (Hprefix: forall n, (n < brb')%nat -> Key.testbit prefix n = Key.testbit p n), (forall n, (n >= m')%nat -> Key.testbit p n = false) -> wf (Some (p, m, m', true)) t1 -> wf (Some (p, m, m', false)) t2 -> wf (Some (prefix, brb, brb', lr)) (branch p m t1 t2).
proof: Proof. unfold branch; intros. inv H0; try constructor; auto. - inv H1; try econstructor; trivial. + erewrite ! Key.zerobit_spec; try eassumption. f_equal; symmetry; apply Hprefix0; auto. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + intros. rewrite Hprefix; auto. apply Hprefix0. lia. + erewrite ! Key.zerobit_spec; try eassumption. f_equal; symmetry; apply Hprefix0; auto. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + instantiate (1 := brbit'); lia. + assumption. + assumption. + intros. rewrite Hprefix; try lia. rewrite Hprefix0; auto; lia. + assumption. + assumption. - inv H1; try econstructor; trivial. + erewrite ! Key.zerobit_spec; try eassumption. f_equal; symmetry; apply Hprefix0; auto. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + intros. rewrite Hprefix; try lia. rewrite Hprefix0; auto; lia. + congruence. + congruence. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + eassumption. + auto. + auto. + constructor; auto. + constructor; auto. + congruence. + congruence. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + eassumption. + assumption. + assumption. + constructor; auto. + econstructor; trivial; try eassumption. - inv H1; try econstructor; trivial. + erewrite ! Key.zerobit_spec; try eassumption. f_equal; symmetry; apply Hprefix0; auto. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + instantiate (1 := brbit'). lia. + assumption. + assumption. + intros. rewrite Hprefix; try lia. rewrite Hprefix0; auto; lia. + congruence. + congruence. + congruence. + congruence. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + eassumption. + assumption. + assumption. + econstructor; trivial; eassumption. + econstructor; auto. + congruence. + congruence. + generalize (Key.mask_spec prefix _ _ Hbrb). intros [HA HB]. eapply Key.testbit_spec; intros. destruct (lt_dec n brb'). * apply HA; auto. * rewrite HB; try lia; auto. rewrite Hlength; auto; lia. + eassumption. + assumption. + assumption. + econstructor; trivial; try apply H7; try apply H8; try eassumption. + econstructor; trivial; try eapply H6; try eapply H9; try eassumption. Qed.
imports: Lia Cdcl.Coqlib