Commit 04607292 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make ptree_pop_correct more usable.

parent 7a6bdb10
......@@ -635,15 +635,13 @@ Definition ptree_pop (p : ptree) : T * pheap :=
Theorem ptree_pop_correct :
forall p,
match ptree_pop p with
| (v, PHnone) => ptree_to_list p = v :: nil
| (v, PHsome q) => permut (ptree_to_list p) (v :: ptree_to_list q)
| (v, q) => permut (v :: pheap_to_list q) (ptree_to_list p)
end.
Proof.
intros [v [|l]].
easy.
apply permut_refl.
simpl.
apply permut_cons.
apply permut_sym.
apply ptree_merge_pairs_correct.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment