ciag-q-do-n.v 6.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198
  1. From mathcomp Require Import all_ssreflect.
  2. From mathcomp Require Import algebra.rat.
  3. From mathcomp Require Import ssrint seq.
  4. Set Implicit Arguments.
  5. Unset Strict Implicit.
  6. Unset Printing Implicit Defensive.
  7. (* każdy skończony ciąg liczb wymiernych da się zakodować liczbą naturalną *)
  8. Definition hipoteza :=
  9. exists f : nat -> seq rat, forall qs : seq rat, exists n, f n = qs.
  10. (* Najpierw potrzeba funkcji parującej.
  11. Ta jest prosta, ale nie jest bijekcją.
  12. Za Stefan G. Simpson - "Subsystems of Second Order Arithmetic" (II.2)
  13. *)
  14. Definition zgniec (para: nat*nat) : nat := let (i, j) := para in ((i+j)^2)+i.
  15. Check Nat.sqrt.
  16. Definition odgniec (k: nat): (nat*nat) :=
  17. let m := Nat.sqrt k in
  18. let i := k - (m^2) in
  19. (i,m-i).
  20. (* Jeśli będę chciał potem poszpanować, to zmienię powyższą funkcję parującą na bijekcję *)
  21. (*
  22. 0 1 3 6 A F
  23. 2 4 7 B 10
  24. 5 8 C 11
  25. 9 D 12
  26. E
  27. m-ty wiersz n-ta kolmna
  28. *)
  29. Definition zgniec' (para: nat*nat) : nat :=
  30. let (m, n) := para in (((m+n)*(m+n+1)) %/ 2)+m.
  31. Definition odgniec' (n : nat) : nat * nat :=
  32. let fix f (a nr_przek na_przek : nat) : nat * nat :=
  33. match a with
  34. | O => (nr_przek, na_przek)
  35. | n.+1 => if nr_przek == na_przek then f n nr_przek.+1 0 else f n nr_przek na_przek.+1
  36. end
  37. in let (nr_przek, na_przek) := f n 0 0
  38. in (na_przek, nr_przek - na_przek).
  39. (* No ale podmiankę zachowam se na koniec *)
  40. Lemma roznica_miedzy_kwadratami n : n.+1^2 = n^2 + 2*n +1.
  41. Proof.
  42. rewrite -addn1 sqrnD -![n^2 + _ + _]addnA [1 ^2 + 2*_]addnC -[1^2]/1 muln1 //.
  43. Qed.
  44. (* Lemat pomocniczy do zgniec_odgniec;
  45. w pewnym sensie, to słabsza wersja różnicy między kwadratami *)
  46. Lemma sqrt_ij i j : Nat.sqrt ((i + j) ^ 2 + i) = (i+j).
  47. Proof.
  48. apply: PeanoNat.Nat.sqrt_unique.
  49. rewrite -[(_ * _)%coq_nat]/((i+j) * (i+j)) -[(_ * _)%coq_nat]/((i+j).+1 * (i+j).+1) !mulnn.
  50. split; [by apply /leP; apply: leq_addr| apply /ltP].
  51. rewrite roznica_miedzy_kwadratami -(@addnA ((i+j)^2) (2*(i+j)) 1) ltn_add2l.
  52. rewrite mul2n -addnn -[i in X in X < _]addn0 -[_ + _ + 1 ]addnA -[i+ j + _ ]addnA.
  53. rewrite ltn_add2l addnA addn1.
  54. apply: ltn0Sn.
  55. Qed.
  56. Lemma a_plus_b_minus_a a b : a + b - a = b.
  57. Proof.
  58. by rewrite -[a in X in _+_-X=_]addn0 subnDl subn0.
  59. Qed.
  60. (* Podstawowy lemat mówiący, że 2 liczby naturalne można zakodować za pomocą jednej
  61. cała reszta dowodu bazuje na zgniataniu i odgniataniu par liczb naturalnych *)
  62. Lemma zgniec_odgniec k : odgniec (zgniec k) = k.
  63. Proof.
  64. case: k => i j.
  65. by rewrite /zgniec /odgniec !sqrt_ij pair_equal_spec !a_plus_b_minus_a.
  66. Qed.
  67. (* Liczby całkowite można zakodować parą liczb natualnych
  68. możliwych kodowań jest dużo, to tutaj nie jest eleganckie,
  69. ale łatwo się dowodzi jego odwracalność*)
  70. Definition int_do_nat(z : int) : nat :=
  71. match z with
  72. | ssrint.Posz n => zgniec (n, 0)
  73. | ssrint.Negz n => zgniec (n, 1)
  74. end.
  75. Definition nat_do_int(n : nat) :=
  76. let (a, b) := odgniec n in
  77. if b == 0 then Posz a else Negz a.
  78. Lemma zgniec_odgniec_int z : nat_do_int (int_do_nat z) = z.
  79. Proof.
  80. by case : z => n; rewrite /nat_do_int /int_do_nat zgniec_odgniec.
  81. Qed.
  82. (* Liczby wymierne można zakodować parą liczb całkowitych *)
  83. Definition rat_do_nat (r : rat) : nat :=
  84. let (a, b) := rat.valq r in zgniec(int_do_nat a, int_do_nat b).
  85. (* udziwnienia przy definicji a' i b' mają na celu
  86. ułatwienie spełnienia wymagań konstruktora Rat *)
  87. Definition nat_do_rat (n : nat): rat .
  88. pose (ab := odgniec n).
  89. pose (a := nat_do_int ab.1).
  90. pose (b := nat_do_int ab.2).
  91. Open Scope order_scope.
  92. pose (b' := (if (Posz 0) < b then b else (Posz 1))).
  93. Close Scope order_scope.
  94. pose (a' := if (coprime `|a| `|b'|) then a else (Posz 1)).
  95. refine (@Rat (a', b') _ ).
  96. apply /andP; split;
  97. [by rewrite /b'; case: ifP | rewrite /a'; case: ifP => //= _; apply: coprime1n].
  98. Defined.
  99. Lemma zgniec_odgniec_rat r : nat_do_rat (rat_do_nat r) = r.
  100. Proof.
  101. apply /eqP; case : r => [[a b]] H.
  102. rewrite -[_ == _]/(valq _ == valq _) -[valq (Rat H)]/(a,b) /rat_do_nat -[valq (Rat H)]/(a,b).
  103. (* H nie znajduje się teraz w celu, będzie potrzebne dopiero na końcu *)
  104. rewrite /nat_do_rat; apply /eqP.
  105. rewrite [(a,b) in RHS]surjective_pairing pair_equal_spec !zgniec_odgniec !zgniec_odgniec_int.
  106. move: H => /andP [zero_ltn_b wzgl_pierwsze]. (* teraz H jest potrzebne *)
  107. split; [by case: ifP => //; rewrite zero_ltn_b wzgl_pierwsze | by rewrite zero_ltn_b].
  108. Qed.
  109. (* Kodowanie ciągu liczb wymiernych o długości n:
  110. (n, (a1, a2, a3, a4, ..., a_n, 0),
  111. gdzie a_n to zakodowany n-ty wyrac ciągu.
  112. Liczba na końcu to wartownik, mogło by go nie być, ale tak było mi łatwiej *)
  113. Definition seq_do_nat (sq : seq rat) : nat :=
  114. zgniec ((length sq), foldr (fun r z => zgniec ((rat_do_nat r), z)) 0 sq).
  115. (* Funkcja pomocnicza do odkodowywania.
  116. Jeśli ciąg jest zakodowany jako (n, (a1, a2, a3,....)),
  117. to pierwszy argument funkcji to n, a drugi to (a1, a2 ...) *)
  118. Fixpoint odgniec_seq' dlugosc wartosci :=
  119. match dlugosc with
  120. | 0 => [::]
  121. | n.+1 => let (a_i, reszta) := odgniec wartosci in (nat_do_rat a_i) :: (odgniec_seq' n reszta)
  122. end.
  123. Definition nat_do_seq (n : nat): seq rat :=
  124. let (dlugosc, wartosci) := odgniec n in odgniec_seq' dlugosc wartosci.
  125. (* pomocnicze lematy do wykonywania pojedyńczego kroku obliczeń *)
  126. Lemma fold1krok {A B : Type} (f : A -> B -> B) z q qs : foldr f z (q::qs) = f q (foldr f z qs).
  127. Proof. done. Qed.
  128. Lemma fold0 {A B : Type} (f : A -> B -> B) z: foldr f z [::] = z.
  129. Proof. done. Qed.
  130. Lemma odgniec1krok dlugosc wartosci :
  131. odgniec_seq' dlugosc.+1 wartosci =
  132. let (a_i, reszta) := odgniec wartosci in (nat_do_rat a_i) :: (odgniec_seq' dlugosc reszta).
  133. Proof. done. Qed.
  134. (* Dodatkowo, przy poprawnym rozkodowywaniu wartosci=0, ale to nie istotne *)
  135. Lemma odgniec0 wartosci : odgniec_seq' 0 wartosci = [::].
  136. Proof. done. Qed.
  137. Lemma seq_do_nat1krok q sq :
  138. seq_do_nat (q :: sq) =
  139. zgniec (length (q ::sq), zgniec (rat_do_nat q, foldr (fun r z => zgniec ((rat_do_nat r), z)) 0 sq)).
  140. Proof. done. Qed.
  141. (* Koniec nudnych lematów, teraz zasadnicze mięsko *)
  142. Lemma nat_do_seq_glowa q qs :
  143. nat_do_seq (seq_do_nat (q :: qs)) = q :: (nat_do_seq (seq_do_nat qs)).
  144. Proof.
  145. rewrite seq_do_nat1krok {1}/nat_do_seq zgniec_odgniec.
  146. rewrite odgniec1krok. (* czemu "length" się otwiera? nie powinno *)
  147. rewrite zgniec_odgniec zgniec_odgniec_rat.
  148. apply (f_equal (fun qs => q :: qs)).
  149. by rewrite /seq_do_nat /nat_do_seq zgniec_odgniec.
  150. Qed.
  151. Lemma zgniec_odgniec_seq qs : nat_do_seq (seq_do_nat qs) = qs.
  152. Proof.
  153. elim : qs => // q qs H.
  154. rewrite -[in RHS]H.
  155. apply: nat_do_seq_glowa.
  156. Qed.
  157. Lemma twierdzenie: hipoteza.
  158. Proof.
  159. exists nat_do_seq => qs.
  160. exists (seq_do_nat qs).
  161. apply: zgniec_odgniec_seq.
  162. Qed.
  163. (* Teraz udowodnić, że istnieje bijekcja N <-> [Q],
  164. taką bijekcją jest zgniec' i odgniec' *)