F3: Liczby konaturalne [TODO]

Set Primitive Projections.

Set Warnings "+cannot-define-projection".
Set Warnings "+non-primitive-record".

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

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żywać taktyki rewrite do przepisywania sim tak samo jak =.

Require Import Setoid.

#[export]
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_out :
  forall n m : conat,
    n = succ m <-> out n = S 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_conv :
  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 m : conat,
    out n = Z -> add n m = m.

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

Lemma add_zero_r' :
  forall n m : conat,
    out m = Z -> sim (add n m) n.

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

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

Lemma sim_add_zero_r :
  forall n m : conat,
    sim (add n m) zero -> 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,
    add (succ n) m = succ (add n m).

Lemma add_succ_r' :
  forall n m m' : conat,
    out m = S m' -> sim (add n m) (succ (add n m')).
Proof.
  cofix CH.
  intros n m m' Hm.
  constructor; cbn.
  destruct (out n) as [| n'] eqn: Hn.
  - rewrite Hm.
    constructor.
    now rewrite add_zero_l.
  - constructor.
Abort.

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

Lemma eq_sim :
  forall n m : conat,
    n = m -> sim n m.

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

Variant sim2 (F : conat -> conat -> Prop) : NatF conat -> NatF conat -> Prop :=
| sim2_Z : sim2 F Z Z
| sim2_S : forall n1 n2 : conat, F n1 n2 -> sim2 F (S n1) (S n2)
(*| sim2_add : forall n1 n2 m1 m2 : conat,
    F n1 n2 -> F m1 m2 -> sim2 F (out (add n1 m1)) (out (add m2 n2)).*)
| sim2_add : forall n m : conat, sim2 F (out (add n m)) (out (add m n)).

CoInductive sim2' (n m : conat) : Prop :=
{
  sim2'_out : sim2 sim2' (out n) (out m);
}.

Lemma wut :
  forall n m : conat,
    sim2 sim2' (S n) (S m) -> sim2 sim2' (out n) (out m).
Proof.
  intros n m H; inversion H; subst.
  - now apply H2.
  - cbn in *.
    destruct (out n0), (out m0).
    + now congruence.
    + inversion H1; inversion H2; subst.
      admit.
    + inversion H1; inversion H2; subst.
Admitted.

Lemma wut' :
  forall n n' m m' : conat,
    out n = S n' -> out m = S m' ->
      sim2' n m -> sim2' n' m'.
Proof.
  cofix CH.
  intros n n' m m' Hn Hm [Hs].
  constructor.
  inversion Hs.
  - now congruence.
  - replace (out n') with (out n1) by congruence.
    replace (out m') with (out n2) by congruence.
    apply H1.
  - cbn in *.
    destruct (out n0), (out m0).
    + now congruence.
    +
Abort.

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

Lemma sim_add :
  forall n1 n2 m1 m2 : conat,
    sim n1 n2 -> sim m1 m2 -> sim (add n1 m1) (add n2 m2).

Lepsze dodawanie

CoFixpoint add' (n m : conat) : conat :=
{|
  out :=
    match out n with
    | Z => out m
    | S n' =>
      match out m with
      | Z => S n'
      | S m' => S {| out := S (add' n' m') |}
      end
    end
|}.

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

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

Lemma add'_zero_l :
  forall n m : conat,
    out n = Z -> sim (add' n m) m.

Lemma add'_zero_r :
  forall n m : conat,
    out m = Z -> sim (add' n m) n.

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

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 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'_S_l :
  forall n n' m : conat,
    out n = S n' -> sim (add' n m) (succ (add' n' m)).

Lemma add'_S_r :
  forall n m m' : conat,
    out m = S m' -> sim (add' n m) (succ (add' 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'_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).

#[global] Hint Constructors simF sim : core.

Lemma sim_add' :
  forall n1 n2 m1 m2 : conat,
    sim n1 n2 -> sim m1 m2 -> sim (add' n1 m1) (add' n2 m2).

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

Require Import SetoidClass.

#[export]
Instance sim_add'' :
  Proper (sim ==> sim ==> sim) add'.

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

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 -> sim 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 m' : conat,
    out m = S m' -> le n m' -> le n 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'_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).

#[export]
Instance Proper_le :
  Proper (sim ==> sim ==> iff) le.

#[export]
Instance Proper_le' :
  Proper (sim ==> sim ==> Basics.flip Basics.impl) le.

Lemma le_add_r' :
  forall n m : conat,
    le m (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,
    sim (min zero n) zero.

Lemma min_zero_r :
  forall n : conat,
    sim (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_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 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 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 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' :
  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 Finite_sim :
  forall n1 n2 : conat,
    sim n1 n2 -> Finite n1 -> Finite n2.

Lemma Finite_zero' :
  Finite zero.

Lemma Finite_Z :
  forall n : conat,
    out n = Z -> Finite n.

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.

Lemma sim_add_Finite :
  forall a b c : conat,
    Finite c -> sim (add a c) (add b c) -> sim a b.

Lemma sim_add'_Finite :
  forall a b c : conat,
    Finite c -> sim (add' a c) (add' b c) -> sim a b.

Lemma Finite_add :
  forall n m : conat,
    Finite n -> Finite m -> Finite (add n m).

Lemma Finite_add_inv_l :
  forall n m : conat,
    Finite (add n m) -> Finite n.

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_sim :
  forall n m : conat,
    sim n m -> Even n -> Even m.

Lemma Even_S :
  forall n n' : conat,
    out n = S n' -> Odd n' -> Even n.

Lemma Even_S_conv :
  forall n n' : conat,
    out n = S n' -> Even n -> Odd n'.

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

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

Lemma Odd_S :
  forall n n' : conat,
    out n = S n' -> Even n' -> Odd n.

Lemma Odd_S_conv :
  forall n n' : conat,
    out n = S n' -> Odd n -> Even n'.

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

Lemma Odd_succ_conv :
  forall n : conat,
    Odd (succ n) -> Even 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 :
  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 = (omega + 1) - 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)

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

Lemma mul'_zero_r :
  forall n m acc : conat,
    out m = Z -> 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,
    out c <> Z ->
      sim (mul' omega c acc) omega.

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

(* Inductive Finite' : conat -> Prop :=
| Finite'_zero :
    forall n : conat, out n = Z -> Finite' n
| Finite'_succ :
    forall n n' : conat, out n = S n' -> Finite' n' -> Finite' n.

[global] 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)

Module Even2_v2.

Inductive Even2F (n : conat) (P : conat -> Prop) : Prop :=
| Even2_Z :
    forall Hn : out n = Z, Even2F n P
| Even2_SS :
    forall (n' : conat) (Hn : out n = S n'),
      P n' -> Even2F n P.

Inductive Odd2F (n : conat) (P : conat -> Prop) : Prop :=
| Odd2_S :
    forall (n' : conat) (Hn : out n = S n') (HOdd : P n'), Odd2F n P.

CoInductive Even2' (n : conat) : Prop :=
{
  Even2'' : Even2F n Odd2'
}

with Odd2' (n : conat) : Prop :=
{
  Odd2'' : Odd2F n Even2'
}.

Lemma Even2_Even2' :
  forall n : conat, Even2 n -> Even2' n

with Odd2_Odd2' :
  forall n : conat, Odd2 n -> Odd2' n.

Lemma Even2'_Even2 :
  forall n : conat, Even2' n -> Even2 n

with Odd2'_Odd2 :
  forall n : conat, Odd2' n -> Odd2 n.

End Even2_v2.

Lemma Even2_add_Odd2 :
  forall n m : conat, Odd2 n -> Odd2 m -> Even2 (add n m)

with Even2_add_Odd2_Even2 :
  forall n m : conat, Even2 n -> Odd2 m -> Odd2 (add n m).

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