F2: Liczby konaturalne [TODO]

Zdefiniuj liczby konaturalne oraz ich relację bipodobieństwa. Pokaż, że jest to relacja równoważności.

Ltac inv H := inversion H; subst; clear H; auto.

Ltac invle H n m :=
  let n' := fresh n "'" in
  let m' := fresh m "'" in
  let H1 := fresh H "1" in
  let H2 := fresh H "2" in
  let H3 := fresh H "3" in
    destruct H as [[| (n' & m' & H1 & H2 & H3)]].
(* end hide *)

Lemma sim_refl :
  forall n : conat, sim n n.

Lemma sim_sym :
  forall n m : conat, sim n m -> sim m n.

Lemma sim_trans :
  forall a b c : conat, sim a b -> sim b c -> sim a c.

Dzięki poniższemu będziemy mogli używac taktyki rewrite do przepisywania sim tak samo jak =.

Require Import Setoid.

Instance Equivalence_sim : Equivalence sim.

Zero, następnik i nieskończoność

Zdefiniuj zero, następnik oraz liczbę omega - jest to nieskończona liczba konaturalna, która jest sama swoim poprzednikiem. Udowodnij ich kilka podstawowych właściwości.

Lemma succ_pred :
  forall n m : conat,
    n = succ m <-> pred n = Some m.

Lemma zero_not_omega :
  ~ sim zero omega.

Lemma sim_succ_omega :
  forall n : conat, sim n (succ n) -> sim n omega.

Lemma succ_omega :
  omega = succ omega.

Lemma sim_succ :
  forall n m : conat, sim n m -> sim (succ n) (succ m).

Lemma sim_succ_inv :
  forall n m : conat, sim (succ n) (succ m) -> sim n m.

Dodawanie

Zdefiniuj dodawanie liczb konaturalnych i udowodnij jego podstawowe właściwości.

Lemma add_zero_l :
  forall n : conat, sim (add zero n) n.

Lemma add_zero_r :
  forall n : conat, sim (add n zero) n.

Lemma sim_add_zero :
  forall n m : conat,
    sim (add n m) zero -> sim n zero /\ sim m zero.

Lemma add_omega_l :
  forall n : conat, sim (add omega n) omega.

Lemma add_omega_r :
  forall n : conat, sim (add n omega) omega.

Lemma add_succ_l :
  forall n m : conat, sim (add (succ n) m) (add n (succ m)).

Lemma add_succ_r :
  forall n m : conat, sim (add n (succ m)) (add (succ n) m).

Lemma add_succ_l' :
  forall n m : conat, sim (add (succ n) m) (succ (add n m)).

Lemma add_succ_r' :
  forall n m : conat, sim (add n (succ m)) (succ (add n m)).

Lemma add_assoc :
  forall a b c : conat, sim (add (add a b) c) (add a (add b c)).

Lemma add_comm :
  forall n m : conat, sim (add n m) (add m n).

Lemma sim_add_zero_l :
  forall n m : conat,
    sim (add n m) zero -> sim n zero.

Lemma sim_add_zero_r :
  forall n m : conat,
    sim (add n m) zero -> sim m zero.

Lemma sim_add :
  forall n n' m m' : conat,
    sim n n' -> sim m m' -> sim (add n m) (add n' m').

Porządek

Zdefiniuj relację <= na liczbach konaturalnych i udowodnij jej podstawowe właściwości.

Lemma le_0_l :
  forall n : conat, le zero n.

Lemma le_0_r :
  forall n : conat, le n zero -> n = zero.

Lemma le_succ :
  forall n m : conat, le n m -> le (succ n) (succ m).

Lemma le_succ_conv :
  forall n m : conat,
    le (succ n) (succ m) -> le n m.

Lemma le_refl :
  forall n : conat, le n n.

Lemma le_trans :
  forall a b c : conat, le a b -> le b c -> le a c.

Lemma le_univalent :
  forall n m : conat,
    le n m -> le m n -> sim n m.

Lemma le_sim :
  forall n1 n2 m1 m2 : conat,
    sim n1 n2 -> sim m1 m2 -> le n1 m1 -> le n2 m2.

Lemma le_omega_r :
  forall n : conat, le n omega.

Lemma le_omega_l :
  forall n : conat, le omega n -> sim n omega.

Lemma le_succ_r :
  forall n m : conat, le n m -> le n (succ m).

Lemma le_add_l :
  forall a b c : conat,
    le a b -> le a (add b c).

Lemma le_add_r :
  forall a b c : conat,
    le a c -> le a (add b c).

Lemma le_add :
  forall n1 n2 m1 m2 : conat,
    le n1 n2 -> le m1 m2 -> le (add n1 m1) (add n2 m2).

Lemma le_add_l' :
  forall n m : conat, le n (add n m).

Lemma le_add_r' :
  forall n m : conat, le m (add n m).

Lemma le_add_l'' :
  forall n n' m : conat,
    le n n' -> le (add n m) (add n' m).

Lemma le_add_r'' :
  forall n m m' : conat,
    le m m' -> le (add n m) (add n m').

Minimum i maksimum

Zdefiniuj funkcje min i max i udowodnij ich właściwości.

Lemma min_zero_l :
  forall n : conat, min zero n = zero.

Lemma min_zero_r :
  forall n : conat, min n zero = zero.

Lemma min_omega_l :
  forall n : conat, sim (min omega n) n.

Lemma min_omega_r :
  forall n : conat, sim (min n omega) n.

Lemma min_succ :
  forall n m : conat,
    sim (min (succ n) (succ m)) (succ (min n m)).

Lemma max_zero_l :
  forall n : conat, sim (max zero n) n.

Lemma max_zero_r :
  forall n : conat, sim (max n zero) n.

Lemma max_omega_l :
  forall n : conat, sim (max omega n) omega.

Lemma max_omega_r :
  forall n : conat, sim (max n omega) omega.

Lemma max_succ :
  forall n m : conat,
    sim (max (succ n) (succ m)) (succ (max n m)).

Lemma min_assoc :
  forall a b c : conat, sim (min (min a b) c) (min a (min b c)).

Lemma max_assoc :
  forall a b c : conat, sim (max (max a b) c) (max a (max b c)).

Lemma min_comm :
  forall n m : conat, sim (min n m) (min m n).

Lemma max_comm :
  forall n m : conat, sim (max n m) (max m n).

Lemma min_add_l :
  forall a b c : conat,
    sim (min (add a b) (add a c)) (add a (min b c)).

Lemma min_add_r :
  forall a b c : conat,
    sim (min (add a c) (add b c)) (add (min a b) c).

Lemma max_add_l :
  forall a b c : conat,
    sim (max (add a b) (add a c)) (add a (max b c)).

Lemma max_add_r :
  forall a b c : conat,
    sim (max (add a c) (add b c)) (add (max a b) c).

Lemma min_le :
  forall n m : conat, le n m -> sim (min n m) n.

Lemma max_le :
  forall n m : conat, le n m -> sim (max n m) m.

Lemma min_diag :
  forall n : conat, sim (min n n) n.

Lemma max_diag :
  forall n : conat, sim (max n n) n.

Lemma sim_min_max :
  forall n m : conat,
    sim (min n m) (max n m) -> sim n m.

Lemma min_max :
  forall a b : conat, sim (min a (max a b)) a.

Lemma max_min :
  forall a b : conat, sim (max a (min a b)) a.

Lemma min_max_distr :
  forall a b c : conat,
    sim (min a (max b c)) (max (min a b) (min a c)).

Lemma max_min_distr :
  forall a b c : conat,
    sim (max a (min b c)) (min (max a b) (max a c)).

Dzielenie przez 2

Zdefiniuj funkcję div2, która dzieli liczbę konaturalną przez 2 (cokolwiek to znaczy). Udowodnij jej właściwości.

Lemma div2_zero :
  sim (div2 zero) zero.

Lemma div2_omega :
  sim (div2 omega) omega.

Lemma div2_succ :
  forall n : conat, sim (div2 (succ (succ n))) (succ (div2 n)).

Lemma div2_add :
  forall n : conat, sim (div2 (add n n)) n.

Lemma le_div2_l_aux :
  forall n m : conat, le n m -> le (div2 n) m.

Lemma le_div2_l :
  forall n : conat, le (div2 n) n.

Lemma le_div2 :
  forall n m : conat, le n m -> le (div2 n) (div2 m).

Skończoność i nieskończoność

Zdefiniuj predykaty Finite i Infinite, które wiadomo co znaczą. Pokaż, że omega jest liczbą nieskończoną i że nie jest skończona, oraz że każda liczba nieskończona jest bipodobna do omegi. Pokaż też, że żadna liczba nie może być jednocześnie skończona i nieskończona.

Lemma omega_not_Finite :
  ~ Finite omega.

Lemma Infinite_omega :
  Infinite omega.

Lemma Infinite_omega' :
  forall n : conat, Infinite n -> sim n omega.

Lemma Finite_Infinite :
  forall n : conat, Finite n -> Infinite n -> False.

Parzystość i nieparzystość

Zdefiniuj predykaty Even i Odd. Pokaż, że omega jest jednocześnie parzysta i nieparzysta. Pokaż, że jeżeli liczba jest jednocześnie parzysta i nieparzysta, to jest nieskończona. Wyciągnij z tego oczywisty wniosek. Pokaż, że każda liczba skończona jest parzysta albo nieparzysta.

Lemma Even_zero :
  Even zero.

Lemma Odd_zero :
  ~ Odd zero.

Lemma Even_Omega :
  Even omega.

Lemma Odd_Omega :
  Odd omega.

Lemma Even_Odd_Infinite :
  forall n : conat, Even n -> Odd n -> Infinite n.

Lemma Even_succ :
  forall n : conat, Odd n -> Even (succ n).

Lemma Odd_succ :
  forall n : conat, Even n -> Odd (succ n).

Lemma Even_succ_inv :
  forall n : conat, Odd (succ n) -> Even n.

Lemma Odd_succ_inv :
  forall n : conat, Even (succ n) -> Odd n.

Lemma Finite_Even_Odd :
  forall n : conat, Finite n -> Even n \/ Odd n.

Lemma Finite_not_both_Even_Odd :
  forall n : conat, Finite n -> ~ (Even n /\ Odd n).

Lemma Even_add_Odd :
  forall n m : conat, Odd n -> Odd m -> Even (add n m).

Lemma Even_add_Even :
  forall n m : conat, Even n -> Even m -> Even (add n m).

Lemma Odd_add_Even_Odd :
  forall n m : conat, Even n -> Odd m -> Odd (add n m).

Odejmowanie (TODO)

Było już o dodawaniu, przydałoby się powiedzieć też coś o odejmowaniu. Niestety, ale odejmowania liczb konaturalnych nie da się zdefiniować (a przynajmniej tak mi się wydaje). Nie jest to również coś, co można bezpośrednio udowodnić. Jest to fakt żyjący na metapoziomie, czyli mówiący coś o Coqu, a nie mówiący coś w Coqu. Jest jednak pewien wewnętrzny sposób by upewnić się, że odejmowanie faktycznie nie jest koszerne.

Definition Sub (n m r : conat) : Prop :=
sim (add r m) n.

W tym celu definiujemy relację Sub, która ma reprezentować wykres funkcji odejmującej, tzn. specyfikować, jaki jest związek argumentów funkcji z jej wynikiem.

Definition sub : Type :=
{f : conat -> conat -> conat |
forall n m r : conat, f n m = r <-> Sub n m r}.

Dzięki temu możemy napisać precyzyjny typ, który powinna mieć nasza funkcja - jest to funkcja biorąca dwie liczby konaturalne i zwracająca liczbę konaturalną, która jest poprawna i pełna względem wykresu.

Lemma Sub_nondet :
forall r : conat, Sub omega omega r.

Niestety mimo, że definicja relacji Sub jest tak oczywista, jak to tylko możliwe, relacja ta nie jest wykresem żadnej funkcji, gdyż jest niedeterministyczna.

Lemma sub_cant_exist :
sub -> False.

Problem polega na tym, że omega - omega może być dowolną liczbą konaturalną. Bardziej obrazowo:

Chcielibyśmy, żeby n - n = 0
Chcielibyśmy, żeby (n + 1) - n = 1
Jednak dla n = omega daje to omega - omega = 0 oraz omega - omega = 1, co prowadzi do sprzeczności

Dzięki temu możemy skonkludować, że typ sub jest pusty, a zatem pożądana przez nas funkcją odejmująca nie może istnieć.

Najbliższą odejmowaniu operacją, jaką możemy wykonać na liczbach konaturalnych, jest odejmowanie liczby naturalnej od liczby konaturalnej.

Mnożenie (TODO)

CoFixpoint mul' (n m acc : conat) : conat :=
{|
    pred :=
      match pred n, pred m with
          | None , _ => pred acc
          | _ , None => pred acc
          | Some n', Some m' => Some (mul' n' m' (add n' (add m' acc)))
      end
|}.

Definition mul (n m : conat) : conat :=
  mul' n m zero.

Lemma mul'_zero_l :
  forall c acc : conat,
    mul' zero c acc = acc.

Lemma mul'_zero_r :
  forall n m acc : conat,
    pred m = None -> mul' n m acc = acc.

Lemma mul'_comm :
  forall n m acc1 acc2 : conat,
    sim acc1 acc2 ->
      sim (mul' n m acc1) (mul' m n acc2).

Lemma mul'_one_l :
  forall c acc : conat,
    sim (mul' (succ zero) c acc) (add c acc).

Lemma mul'_one_r :
  forall c acc : conat,
    sim (mul' c (succ zero) acc) (add c acc).

Lemma mul'_omega_l :
  forall c acc : conat,
    pred c <> None ->
      sim (mul' omega c acc) omega.

Lemma mul'_omega_r :
  forall c acc : conat,
    pred c <> None ->
      sim (mul' c omega acc) omega.

Definition pred' (n : conat) : conat :=
match pred n with
    | None => zero
    | Some n' => n'
end.

(* Inductive Finite' : conat -> Prop :=
    | Finite'_zero :
        forall n : conat, pred n = None -> Finite' n
    | Finite'_succ :
        forall n n' : conat, pred n = Some n' -> Finite' n' -> Finite' n.
*)

(* Inductive Finite' : conat -> Prop :=
    | Finite'_zero :
        forall n : conat, pred n = None -> Finite' n
    | Finite'_succ :
        forall n : conat, Finite' (pred' n) -> Finite' n.

Hint Constructors Finite' : core.
*)

Lemma mul'_acc :
  forall n m acc1 acc2 : conat,
    sim (mul' n m (add acc1 acc2)) (add acc1 (mul' n m acc2)).

Lemma mul'_succ_l :
  forall n m acc : conat,
    sim (mul' (succ n) m acc) (add m (mul' n m acc)).

Lemma Finite_mul' :
  forall n m acc : conat,
    Finite n -> Finite m -> Finite acc ->
      Finite (mul' n m acc).

Lemma mul'_assoc :
  forall a b c acc1 acc1' acc2 acc2' : conat,
    sim acc1 acc1' -> sim acc2 acc2' ->
      sim (mul' a (mul' b c acc1) acc2) (mul' (mul' a b acc1') c acc2').

Koindukcja wzajemna (TODO)

Liczby naturalne i konaturalne

Zdefiniuj funkcję from_nat, która przekształca liczbę naturalną w odpowiadającą jej skończoną liczbę konaturalną.

Lemma Finite_from_nat :
forall n : nat, Finite (from_nat n).

Pokaż, że from_nat nie ma żadnej preodwrotności.

Lemma no_preinverse :
forall f : conat -> nat,
(forall c : conat, from_nat (f c) = c) -> False.

Pokaż, że jeżeli from_nat ma postodwrotność, to można rozstrzygać, czy liczba konaturalna jest skończona czy nie.

UWAGA: diabelsko trudne. Wymaga ruszenia wyobraźnią i wymyślenia kilku induktywnych definicji relacji oraz udowodnienia paru lematów na ich temat.

Lemma inverse_taboo :
  forall f : conat -> nat,
    (forall n : nat, f (from_nat n) = n) ->
      forall c : conat, Infinite c \/ Finite c.

Losowe ćwiczenia

Ćwiczenie

Pokaż, że niezaprzeczalnie każda liczba konaturalna jest skończona lub nieskończona.

Lemma Finite_or_Infinite :
forall c : conat, ~ ~ (Finite c \/ Infinite c).