Wiezniowie.v 4.6 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596
  1. From mathcomp Require Import all_ssreflect.
  2. From mathcomp Require Import ssralg.
  3. Set Implicit Arguments.
  4. Unset Strict Implicit.
  5. Unset Printing Implicit Defensive.
  6. Require Import GrupaPrzemiennaModulo.
  7. Open Scope ring_scope.
  8. Section Wiezniowie.
  9. (* W więzieniu jest n więźniów. Zakładamy, że n > 0 *)
  10. Variable n' : nat.
  11. Notation n := n'.+1.
  12. (* Każdy więzień ma na czole liczbę od 0 do n (czyli spośród 'I_n) *)
  13. Variable wiezniowie : n.-tuple 'I_n.
  14. (* Postać rozwiązania to rodzina algorytmów.
  15. Indeksem rodziny jest numer więźnia (0..N-1) - pierwszy argument.
  16. Wejściem algorytmu są liczby widziane na czołach pozostałych (krotka n-1 liczb) - drugi argument.
  17. Wyjściem algorytmu jest domniemana liczba na czole więźnia.
  18. *)
  19. Definition rozwiazanie := (* numer więźnia *) 'I_n ->
  20. (* liczby widziane u pozostałych *) n.-1.-tuple 'I_n ->
  21. (* domanimana liczba na swoim czole *) 'I_n.
  22. (* Wycięcie więźnia w taki sposób to szczegół techniczny, można by to robić jakkolwiek inaczej, o ile byłby lemat o odwracalności (przywroc_pozostali) *)
  23. Definition pozostali (lp: 'I_n): n.-1.-tuple 'I_n := [tuple of (behead (rot lp wiezniowie))].
  24. (* Więzień zgadł, jeśli liczba na jego czole jest taka, jaką policzył jego algorytm *)
  25. Definition zgadl (algorytm :rozwiazanie) (lp: 'I_n) :=
  26. tnth wiezniowie lp == algorytm lp (pozostali lp).
  27. Definition poprawne_rozwiazanie (algorytm :rozwiazanie): Prop := exists wiezien, zgadl algorytm wiezien.
  28. (* Rozwiązanie zagadki - wyjaśnienie w "rozwiazanie.md" *)
  29. (* Z taką definicją pracuje się łatwiej niż z: \sum_(i <- liczby) i *)
  30. Definition suma_modulo (liczby : seq 'I_n): 'I_n := foldr (fun a b => a + b) ord0 liczby.
  31. Definition algorytm_wygrywajacy: rozwiazanie :=
  32. fun lp pozostali => lp - (suma_modulo pozostali).
  33. (* Poniżej są już tylko lematy przygotowujące do ostatecznego twierdzenia, że algorytm_wygrywajacy jest zawsze poprawnym rozwiązaniem *)
  34. (* przywróć więźnia spowrotem do puli, po wycięciu go. Konstrukcja jest taka, aby łatwo było dowieźć lemat o odwracalności przywroc_pozostali *)
  35. Definition przywroc (lp : 'I_n) (pozostali: n.-1.-tuple 'I_n) : n.-tuple 'I_n :=
  36. [tuple of rotr lp (thead [tuple of rot lp wiezniowie] :: pozostali)].
  37. Lemma przywroc_pozostali (lp :'I_n): przywroc lp (pozostali lp) = wiezniowie.
  38. apply /eqP; rewrite /pozostali /przywroc /eq_op /=.
  39. rewrite -[rotr lp [tuple of thead [tuple of rot lp wiezniowie] :: behead [tuple of rot lp wiezniowie]]]/_.
  40. rewrite -tuple_eta rotK //.
  41. Qed.
  42. (* suma modulo jest rozdzielna ze względu na łączenie krotek *)
  43. Lemma suma_modulo_plusplus s1 s2 : suma_modulo (s1 ++ s2) = (suma_modulo s1 + suma_modulo s2).
  44. Proof.
  45. by elim: s1 => /=; [rewrite GRing.add0r | move => x s1 ->; rewrite GRing.addrA].
  46. Qed.
  47. (* suma modulo jest taka sama dla wsystkich permutacji krotki *)
  48. Lemma suma_modulo_perm p q: perm_eq p q -> suma_modulo p = suma_modulo q.
  49. apply/catCA_perm_subst: p q => s1 s2 s3.
  50. rewrite !suma_modulo_plusplus GRing.addrA [(_ s1) + (_ s2)]GRing.addrC GRing.addrA //.
  51. Qed.
  52. Lemma suma_modulo_cons s a : a + suma_modulo s = suma_modulo (a :: s). done. Qed.
  53. (* jeśli dorzuci się liczbę na czole więźnia do sumy modulo pozostałych, to otrzyma się sumę modulo wszystkich *)
  54. Lemma suma_modulo_pozostalych lp : suma_modulo wiezniowie = (tnth wiezniowie lp) + suma_modulo (pozostali lp).
  55. rewrite -{1}(przywroc_pozostali lp) /przywroc /= suma_modulo_cons.
  56. apply: suma_modulo_perm.
  57. rewrite perm_rot.
  58. suff ->: thead [tuple of rot lp wiezniowie] = tnth wiezniowie lp by rewrite perm_cons perm_refl.
  59. rewrite /rot /thead !(tnth_nth ord0) nth_cat.
  60. case: ifP; [rewrite nth_drop addn0 |
  61. (* (val 'I_n) będzie zawsze mniejsze niż (size_tuple n-tuple) *)
  62. rewrite ltnNge leqn0 size_drop subn_eq0 size_tuple -leqNgt -[lp <= n']/(lp < n) ltn_ord];
  63. done.
  64. Qed.
  65. Lemma algorytm_wygrywajacy_jest_zawsze_poprawny: poprawne_rozwiazanie algorytm_wygrywajacy.
  66. Proof.
  67. rewrite /poprawne_rozwiazanie /algorytm_wygrywajacy /zgadl.
  68. exists (suma_modulo wiezniowie).
  69. rewrite {2}(suma_modulo_pozostalych (suma_modulo wiezniowie)).
  70. rewrite -GRing.addrA GRing.addrN GRing.addr0 //.
  71. Qed.
  72. End Wiezniowie.
  73. Close Scope ring_scope.
  74. (* Tak dla pewności, powtórzenie tego samego poza sekcją *)
  75. Lemma rozwiazanie_dziala_zawsze :
  76. forall (n' : nat) (wiezniowie: (n'.+1).-tuple 'I_n'.+1),
  77. poprawne_rozwiazanie wiezniowie (@algorytm_wygrywajacy n').
  78. Proof. exact algorytm_wygrywajacy_jest_zawsze_poprawny. Qed.