proposition: Theorem konigsberg_bridges : let E := [(0, 1); (0, 2); (0, 3); (1, 2); (1, 2); (2, 3); (2, 3)] in forall p, path p -> eulerian E p -> False.
proof: Proof. intros E p Hpath Hperm. rewrite <-pathb_correct in Hpath. unfold eulerian in Hperm. replace (map normalize_direction E) with E in Hperm by reflexivity. apply pathbdir_correct in Hpath. revert Hperm Hpath. generalize (map normalize_direction p). intros l Hperm. generalize (shouldswap p). cut (pathbdir true l || pathbdir false l = false)%bool. { intros H b Hpath. destruct b; rewrite Hpath in H. discriminate. destruct (pathbdir true l); discriminate. } clear p. revert l Hperm. intros l Pl. assert (Hlen : length E = length l). { apply Permutation_length; auto. } assert (HE : forall x, In x l -> x = (0, 1) \/ x = (0, 2) \/ x = (0, 3) \/ x = (1, 2) \/ x = (2, 3)). { intros x i. apply Permutation_in with (l' := E) in i. 2:apply Permutation_sym, Pl. simpl in i. repeat (destruct i as [ <- | i ]; try tauto). } destruct l as [ | p0 l ]. inversion Hlen. destruct l as [ | p1 l ]. inversion Hlen. destruct l as [ | p2 l ]. inversion Hlen. destruct l as [ | p3 l ]. inversion Hlen. destruct l as [ | p4 l ]. inversion Hlen. destruct l as [ | p5 l ]. inversion Hlen. destruct l as [ | p6 l ]. inversion Hlen. destruct l as [ | ]. 2: inversion Hlen. clear Hlen. apply Permutation_sym in Pl. pose proof permutation_remove pe _ _ _ Pl as Pl1. pose proof permutation_remove pe _ _ _ Pl1 as Pl2. pose proof permutation_remove pe _ _ _ Pl2 as Pl3. pose proof permutation_remove pe _ _ _ Pl3 as Pl4. pose proof permutation_remove pe _ _ _ Pl4 as Pl5. pose proof permutation_remove pe _ _ _ Pl5 as Pl6. apply prune in Pl1. apply prune in Pl2. apply prune in Pl3. apply prune in Pl4. apply prune in Pl5. apply prune in Pl6. pose proof HE p0 ltac:(do 0 right; left; reflexivity) as E0. pose proof HE p1 ltac:(do 1 right; left; reflexivity) as E1. pose proof HE p2 ltac:(do 2 right; left; reflexivity) as E2. pose proof HE p3 ltac:(do 3 right; left; reflexivity) as E3. pose proof HE p4 ltac:(do 4 right; left; reflexivity) as E4. pose proof HE p5 ltac:(do 5 right; left; reflexivity) as E5. pose proof HE p6 ltac:(do 6 right; left; reflexivity) as E6. Ltac d H := destruct H as [ -> | [ -> | [ -> | [ -> | -> ]]]]. Ltac t E P := d E; try reflexivity; try inversion P. d E0. all: t E1 Pl1. all: t E2 Pl2. all: t E3 Pl3. all: t E4 Pl4. all: t E5 Pl5. all: t E6 Pl6. Qed.
imports: Arith List Permutation