fact: Definition point_to_point (cells : seq cell) (source target : pt) : option (seq (annotated_point * annotated_point)) := let source_is := find_origin_cells cells source in let target_is := find_origin_cells cells target in if Nat.ltb 0 (List.length source_is) && Nat.ltb 0 (List.length target_is) then if Nat.ltb 0 (List.length (intersection source_is target_is)) then Some ((Apt source source_is, Apt target target_is) :: nil) else let ocp := cell_path cells (head 0%nat source_is) (head 0%nat target_is) in match ocp with Some cp => if 2 <=? List.length cp then if existsb (Nat.eqb (nth 0 cp 0%nat)) source_is then if existsb (Nat.eqb (nth (List.length cp - 2) cp 0%nat)) target_is then Some (door_to_door cells (head 0%nat source_is) (nth 0 cp 0%nat) (Some source) (Some target) (seq.behead cp )) else Some (door_to_door cells (head 0%nat source_is) (nth 0 cp 0%nat) (Some source) None (seq.behead cp) ++ path_reverse (point_to_door cells (Apt target target_is) (nth (List.length cp - 1) cp 0%nat) (nth (List.length cp - 2) cp 0%nat))) else if existsb (Nat.eqb (nth ((List.length cp) - 2) cp 0%nat)) target_is then Some ((point_to_door cells (Apt source source_is) (head 0%nat source_is) (nth 0 cp 0%nat)) ++ door_to_door cells (head 0%nat source_is) (nth 0 cp 0%nat) None (Some target) (seq.behead cp)) else Some (point_to_door cells (Apt source source_is) (head 0%nat source_is) (nth 0 cp 0%nat) ++ door_to_door cells (head 0%nat source_is) (nth 0 cp 0%nat) None None (seq.behead cp) ++ path_reverse (point_to_door cells (Apt target target_is) (nth (List.length cp - 1) cp 0%nat) (nth (List.length cp - 2) cp 0%nat))) else match common_vert_edge (nth (head 0%nat source_is) cells dummy_cell) (nth (head 0%nat target_is) cells dummy_cell) with | Some v => if on_vert_edge source v || on_vert_edge target v then Some ((Apt source source_is, Apt target target_is) :: nil) else Some (point_to_door cells (Apt source source_is) (head 0%nat source_is) (head 0%nat target_is) ++ path_reverse (point_to_door cells (Apt target target_is) (head 0%nat source_is) (head 0%nat target_is))) | None => None end | None => None end else None.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL