\ 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.