proposition: Lemma pathbdir_correct p : pathb p = true -> pathbdir (shouldswap p) (map normalize_direction p) = true.
proof: Proof. induction p as [ | [x y] [ | [y' z] l] IHl ]. - intro. auto. - intro. simpl. unfold normalize_direction. simpl. destruct (x <=? y); auto. - change (pathb ((x, y) :: (y', z) :: l)) with ((y =? y') && pathb ((y', z) :: l))%bool. destruct (y =? y') eqn:E. 2:discriminate. rewrite Bool.andb_true_l. intros HP. specialize (IHl HP). apply Nat.eqb_eq in E. subst y'. simpl (map _ _) in *. unfold normalize_direction at 1 2. unfold normalize_direction at 1 in IHl. simpl fst in *. simpl snd in *. simpl (shouldswap _) in *. destruct (y <=? z) eqn:Eyz, (x <=? y) eqn:Exy; simpl (negb _) in *. all: rewrite pathbdir_rewrite, IHl, Nat.eqb_refl. all: simpl (andb true true). all: auto. all: apply Bool.orb_true_r. Qed.
imports: Arith List Permutation