proposition: Lemma search_fold : forall {A B: Type} (f: key -> A -> option B) (m: ptrie A), search f m = fold' (fun acc k v => match acc with | None => f k v | Some r => Some r end) m None.
proof: Proof. intros A B f. set (F := (fun (acc : option B) (k : key) (v : A) => match acc with | Some r => Some r | None => f k v end)). assert (FOUND : forall m x, fold' F m (Some x) = Some x). { induction m ; simpl ; auto. intros. rewrite IHm1. auto. } induction m; simpl. - reflexivity. - auto. - rewrite IHm1. destruct (fold' F m1 None) eqn:E1. rewrite FOUND. reflexivity. auto. Qed.
imports: List Bool ZArith Lia