\ Untitled - /g/pasta 2.4
From Little Camel, 4 Years ago, written in Plain Text.
Embed
1. Require Import Arith.
2. Require Import Omega.
3. Require Import List.
4. Require Import Permutation.
5. Import ListNotations.
6.
7. Definition edges_traversed (path : list nat) : list (nat*nat) :=
8.   combine path (tl path).
9.
10. Definition sort2 (x : nat*nat) : nat*nat :=
11.   let (a, b) := x in (min a b, max a b).
12.
13. Definition eulerian_path (path : list nat) (edges : list (nat*nat)) : Prop :=
14.   Permutation (map sort2 (edges_traversed path)) (map sort2 edges).
15.
16. Fixpoint toggle (xs : list nat) (y : nat) :=
17.   match xs with
18.   | [] => [y]
19.   | x :: zs => if eq_nat_dec x y then zs else x :: toggle zs y
20.   end.
21.
22. Definition odd_count (xs : list nat) : list nat :=
23.   fold_left toggle xs [].
24.
25. Fixpoint endpoints (edges : list (nat*nat)) :=
26.   match edges with
27.   | [] => []
28.   | (x, y) :: ps => x :: y :: endpoints ps
29.   end.
30.
31. Definition num_odd_degree_vertices (edges : list (nat*nat)) : nat :=
32.   length (odd_count (endpoints edges)).
33.
34. Lemma odd_count_double :
35.   forall x, odd_count [x; x] = [].
36. Proof.
37.   intro x.
38.   change ((if eq_nat_dec x x then [] else [x; x]) = []).
39.   destruct (eq_nat_dec x x); trivial; tauto.
40. Qed.
41.
42. Lemma Permutation_toggle :
43.   forall xs ys z, Permutation xs ys -> Permutation (toggle xs z) (toggle ys z).
44. Proof.
45.   intros xs ys z H.
46.   induction H as [|x xs ys H IH|x y zs|xs ys zs H1 IH1 H2 IH2].
47.   - trivial.
48.   - simpl.
49.     destruct (eq_nat_dec x z); auto.
50.   - simpl.
51.     destruct (eq_nat_dec x z) as [A|A], (eq_nat_dec y z) as [B|B]; try (repeat subst; trivial).
52.     apply perm_swap.
53.   - apply (perm_trans (l' := toggle ys z)); trivial.
54. Qed.
55.
56. Lemma Permutation_toggle_swap :
57.   forall zs x y, Permutation (toggle (toggle zs x) y) (toggle (toggle zs y) x).
58. Proof.
59.   induction zs as [|z zs IH]; intros x y.
60.   - simpl.
61.     destruct (eq_nat_dec x y), (eq_nat_dec y x); trivial; try omega.
62.     apply perm_swap.
63.   - simpl.
64.     destruct (eq_nat_dec z x), (eq_nat_dec z y); repeat subst; simpl.
65.     + trivial.
66.     + destruct (eq_nat_dec x x); trivial; tauto.
67.     + destruct (eq_nat_dec y y); trivial; tauto.
68.     + destruct (eq_nat_dec z x), (eq_nat_dec z y); auto; tauto.
69. Qed.
70.
71. Lemma Permutation_odd_count :
72.   forall xs ys, Permutation xs ys -> Permutation (odd_count xs) (odd_count ys).
73. Proof.
74.   intros xs ys H.
75.   unfold odd_count.
76.   set (bs' := []).
77.   generalize bs' as bs.
78.   induction H as [|x xs ys H IH|x y zs|xs ys zs H1 IH1 H2 IH2]; intro bs.
79.   - trivial.
80.   - apply IH.
81.   - simpl.
82.     set (ps' := toggle (toggle bs y) x).
83.     set (qs' := toggle (toggle bs x) y).
84.     assert (Permutation ps' qs') as H' by apply Permutation_toggle_swap.
85.     generalize ps' qs' H'.
86.     induction zs as [|z zs IH].
87.     + trivial.
88.     + intros ps qs H.
89.       apply IH, Permutation_toggle, H.
90.   - apply (perm_trans (l' := fold_left toggle ys bs)); trivial.
91. Qed.
92.
93. Lemma Permutation_endpoints :
94.   forall ps qs, Permutation ps qs -> Permutation (endpoints ps) (endpoints qs).
95. Proof.
96.   intros ps qs H.
97.   induction H as [|[x1 x2] xs ys H IH|[x1 x2] [y1 y2] zs|xs ys zs H1 IH1 H2 IH2].
98.   - trivial.
99.   - apply perm_skip, perm_skip, IH.
100.   - change (Permutation ([y1; y2; x1; x2] ++ endpoints zs) ([x1; x2; y1; y2] ++ endpoints zs)).
101.     apply Permutation_app; trivial.
102.     change (Permutation ([y1; y2] ++ [x1; x2]) ([x1; x2] ++ [y1; y2])).
103.     apply Permutation_app_comm.
104.   - apply (perm_trans (l' := endpoints ys)); trivial.
105. Qed.
106.
107. Lemma Permutation_endpoints_sort2 :
108.   forall edges, Permutation (endpoints edges) (endpoints (map sort2 edges)).
109. Proof.
110.   induction edges as [|[x y] ps IH].
111.   - trivial.
112.   - simpl.
113.     destruct (le_dec x y) as [H|H].
114.     + rewrite min_l, max_r by trivial.
115.       auto.
116.     + assert (y <= x) as H2 by omega.
117.       rewrite min_r, max_l by trivial.
118.       rewrite perm_swap.
119.       apply perm_skip, perm_skip, IH.
120. Qed.
121.
122. Lemma num_odd_degree_vertices_edges_traversed :
123.   forall path, num_odd_degree_vertices (edges_traversed path) <= 2.
124. Proof.
125.   destruct path as [|w xs]; [compute; auto|].
126.   induction xs as [|x ys IH]; [compute; auto|].
127.   destruct ys as [|y zs].
128.   - change (length (if eq_nat_dec w x then [] else [w; x]) <= 2).
129.     destruct (eq_nat_dec w x); trivial.
130.   - set (ys := y :: endpoints (combine (y :: zs) (zs))).
131.     change (length (odd_count (w :: ys)) <= 2) in IH.
132.     change (length (odd_count (w :: x :: x :: ys)) <= 2).
133.     rewrite (Permutation_length (l' := odd_count (x :: x :: w :: ys))).
134.     + change (length (fold_left toggle (w :: ys) (odd_count [x; x])) <= 2).
135.       rewrite odd_count_double.
136.       trivial.
137.     + apply Permutation_odd_count.
138.       rewrite perm_swap.
139.       apply perm_skip, perm_swap.
140. Qed.
141.
142. Theorem degree_theorem :
143.   forall path edges, eulerian_path path edges -> num_odd_degree_vertices edges <= 2.
144. Proof.
145.   intros path edges H.
146.   unfold num_odd_degree_vertices.
147.   rewrite (Permutation_length (l' := odd_count (endpoints (edges_traversed path)))).
148.   - apply num_odd_degree_vertices_edges_traversed.
149.   - apply Permutation_odd_count.
150.     rewrite (Permutation_endpoints_sort2 edges).
151.     rewrite (Permutation_endpoints_sort2 (edges_traversed path)).
152.     apply Permutation_endpoints.
153.     unfold eulerian_path in H.
154.     auto with *.
155. Qed.
156.
157. Definition autism_test := [(0,1);(0,1);(0,2);(0,2);(0,3);(0,3);(0,4);(0,5);(0,5);(1,2);(1,3);(1,4);(2,4);(2,5);(3,4);(4,5)].
158.
159. Theorem autism :
160.   ~ exists path, eulerian_path path autism_test.
161. Proof.
162.   intros [path H].
163.   apply degree_theorem in H.
164.   compute in H.
165.   omega.
166. Qed.