proposition: Lemma get_some_implies: forall {A: Type} [m: ptrie A] [k: key] [v: A] [opt], wf opt m -> get' k m = Some v -> match m with | Empty => False | Leaf k' v' => k = k' | Branch prefix brbit _ _ => forall brbit', is_mask brbit brbit' -> (forall n, (n < brbit')%nat -> testbit k n = testbit prefix n) end.
proof: Proof. induction m; intros. - simpl in H0; inv H0. - simpl in H0. destruct_eq k0 k; congruence. - simpl in H0. case_eq (zerobit k brbit); intros; rewrite H3 in H0. + inv H. * generalize (IHm1 _ _ _ H7 H0). intros HA. inv H7; try tauto. { subst k0. generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. symmetry. eapply Hprefix0. auto. } { generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. specialize (HA _ Hbrbit'0). rewrite HA; try lia. rewrite Hprefix0; try lia; auto. } * generalize (IHm1 _ _ _ H7 H0). intros HA. inv H7; try tauto. { subst k0. generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. symmetry. eapply Hprefix0. auto. } { generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. specialize (HA _ Hbrbit'0). rewrite HA; try lia. rewrite Hprefix0; try lia; auto. } + inv H. * generalize (IHm2 _ _ _ H10 H0). intros HA. inv H10; try tauto. { subst k0. generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. symmetry. eapply Hprefix0. auto. } { generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. specialize (HA _ Hbrbit'0). rewrite HA; try lia. rewrite Hprefix0; try lia; auto. } * generalize (IHm2 _ _ _ H10 H0). intros HA. inv H10; try tauto. { subst k0. generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. symmetry. eapply Hprefix0. auto. } { generalize (is_mask_same H1 Hbrbit'). intros; subst brbit'0. specialize (HA _ Hbrbit'0). rewrite HA; try lia. rewrite Hprefix0; try lia; auto. } Qed.
imports: List Bool ZArith Lia