search

DmxLarchey / Breadth-First-Numbering

Coq implementation of Breadth-First Numbering à la Okasaki
Other
0 stars 0 forks source link

Bfn forest #14

Closed DmxLarchey closed 5 years ago

DmxLarchey commented 5 years ago

At last I finished the correctness proof of bfn_level which corresponds to bfnum' and bfnum in Okasaki's paper. Could you review the file bfn_level.v in branch bfn_forest before I merge it into cleanup? I spend a lot of time for the proof of bfn_level_spec_1 until I found it derived from forest_rebuild_id, forest_rebuild_lt and the existence of a breadth-first numbering ...

DmxLarchey commented 5 years ago

If you look at how case_eq is implemented, it is something like

match l as l' return l = l' -> P l' with
  | nil => fun E => _
  | x::l' => fun E => _
end eq_refl

case_eq l is shorter to write if you know what it extracts to ...