proposition: Lemma search_some : forall {A B: Type} (f: key -> A -> option B) opt (m: ptrie A) (r:B) (WF: wf opt m), search f m = Some r -> exists k v, get' k m = Some v /\ f k v = Some r.
proof: Proof. intros. rewrite search_fold in H. rewrite fold_elements' in H. assert (exists k v, In (k,v) (elements' m nil) /\ f k v = Some r). { revert r H. set (F:= (fun (a : option B) (p : key * A) => match a with | Some r0 => Some r0 | None => f (fst p) (snd p) end)). assert (forall r l, fold_left F l (Some r) = Some r). { induction l; simpl; auto. } induction (elements' m nil); simpl. - intros. discriminate. - intros. destruct (f (fst a) (snd a)) eqn:EQ. + rewrite H in H0. inv H0. exists (fst a), (snd a). split ; auto. left. destruct a; reflexivity. + apply IHl in H0. destruct H0 as (k1&v1&IN & FS). exists k1,v1. split ; tauto. } destruct H0 as (k&v&IN&FS). exists k,v. split ; auto. generalize (in_elements' m _ _ _ _ WF IN). simpl. tauto. Qed.
imports: List Bool ZArith Lia