text:
(** * 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. *)

(* begin hide *)
Inductive NatF (X : Type) : Type :=
| Z : NatF X
| S : X -> NatF X.

Arguments Z {X}.
Arguments S {X} _.

CoInductive conat : Type :=
{
  out : NatF conat;
}.

Inductive simF (R : conat -> conat -> Prop) : NatF conat -> NatF conat -> Prop :=
| simF_Z : simF R Z Z
| simF_S : forall n1 n2 : conat, R n1 n2 -> simF R (S n1) (S n2).

CoInductive sim (n m : conat) : Prop :=
{
  sim' : simF sim (out n) (out m);
}.

Axiom sim_eq :
  forall {n m : conat}, (sim n m) = (n = m).

Lemma sim_gfp :
  forall (R : conat -> conat -> Prop),
    (forall n1 n2 : conat, R n1 n2 -> simF R (out n1) (out n2)) ->
      forall n1 n2 : conat, R n1 n2 -> sim n1 n2.
Proof.
  intros R Hgfp.
  cofix CH.
  constructor.
  apply Hgfp in H as []; constructor.
  now apply CH.
Qed.

Lemma sim_refl :
  forall n : conat, sim n n.
(* begin hide *)
Proof.
  cofix CH.
  constructor.
  destruct (out n) as [| n'].
  - now constructor.
  - constructor.
    now apply CH.
Qed.
(* end hide *)

Lemma sim_sym :
  forall n m : conat, sim n m -> sim m n.
(* begin hide *)
Proof.
  cofix CH.
  intros n m H; constructor.
  destruct H as [[]].
  - now constructor.
  - constructor.
    now apply CH.
Qed.
(* end hide *)

Lemma sim_trans :
  forall a b c : conat, sim a b -> sim b c -> sim a c.
(* begin hide *)
Proof.
  cofix CH.
  intros a b c ab bc.
  constructor.
  destruct ab as [ab], bc as [bc].
  inversion ab; inversion bc; [| congruence.. |].
  - now constructor.
  - constructor.
    now apply CH with n2; [| congruence].
Qed.
(* end hide *)

(** 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.
(* begin hide *)
Proof.
  esplit; red.
  - apply sim_refl.
  - apply sim_sym.
  - apply sim_trans.
Defined.
(* end hide *)

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

(* begin hide *)
Definition zero : conat :=
{|
  out := Z;
|}.

Definition succ (n : conat) : conat :=
{|
  out := S n;
|}.

CoFixpoint omega : conat :=
{|
  out := S omega;
|}.
(* end hide *)

Lemma succ_out :
  forall n m : conat,
    n = succ m <-> out n = S m.
(* begin hide *)
Proof.
  split.
  - now intros ->; cbn.
  - intros Heq.
    assert (out n = out (succ m)).
      now rewrite Heq; cbn.
Abort.
(* end hide *)

Lemma zero_not_omega :
  ~ sim zero omega.
(* begin hide *)
Proof.
  intros [Hsim]; inversion Hsim.
Qed.
(* end hide *)

Lemma sim_succ_omega :
  forall n : conat, sim n (succ n) -> sim n omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct H as [H]; cbn in H; inversion H; subst.
  constructor.
  apply CH.
  constructor; cbn.
  rewrite H0.
  now apply H2.
Qed.
(* end hide *)

Lemma succ_omega :
  omega = succ omega.
(* begin hide *)
Proof.
Abort.
(* end hide *)

Lemma sim_succ :
  forall n m : conat,
    sim n m -> sim (succ n) (succ m).
(* begin hide *)
Proof.
  now do 2 constructor.
Defined.
(* end hide *)

Lemma sim_succ_conv :
  forall n m : conat,
    sim (succ n) (succ m) -> sim n m.
(* begin hide *)
Proof.
  intros n m [H]; cbn in H.
  now inversion H.
Qed.
(* end hide *)

(** * Dodawanie *)

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

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

Lemma add_zero_l :
  forall n m : conat,
    out n = Z -> add n m = m.
(* begin hide *)
Proof.
  intros n m Heq.
  rewrite <- sim_eq.
  constructor; cbn.
  rewrite Heq.
  now apply sim_refl.
Qed.
(* end hide *)

Lemma add_zero_r :
  forall n : conat,
    sim (add n zero) n.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n'].
  - now constructor.
  - constructor.
    now apply CH.
Qed.
(* end hide *)

Lemma add_zero_r' :
  forall n m : conat,
    out m = Z -> sim (add n m) n.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n'].
  - now rewrite H; constructor.
  - constructor.
    now apply CH.
Qed.
(* end hide *)

Lemma sim_add_zero :
  forall n m : conat,
    sim (add n m) zero -> n = zero /\ m = zero.
(* begin hide *)
Proof.
  intros n m [H]; inversion H.
  rewrite <- !sim_eq.
  cbn in *.
  destruct (out n) eqn: Heq; [| now congruence].
  split; constructor; cbn.
  - now rewrite Heq; constructor.
  - now rewrite <- H1; constructor.
Qed.
(* end hide *)

Lemma sim_add_zero_l :
  forall n m : conat,
    sim (add n m) zero -> n = zero.
(* begin hide *)
Proof.
  now intros; apply sim_add_zero in H as [].
Qed.
(* end hide *)

Lemma sim_add_zero_r :
  forall n m : conat,
    sim (add n m) zero -> m = zero.
(* begin hide *)
Proof.
  now intros; apply sim_add_zero in H as [].
Qed.
(* end hide *)

Lemma add_omega_l :
  forall n : conat,
    sim (add omega n) omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma add_omega_r :
  forall n : conat,
    sim (add n omega) omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n).
  - now constructor.
  - constructor.
    now apply CH.
Qed.
(* end hide *)

Lemma add_succ_l :
  forall n m : conat,
    add (succ n) m = succ (add n m).
(* begin hide *)
Proof.
  intros n m.
  rewrite <- sim_eq.
  now constructor; cbn; constructor.
Qed.
(* end hide *)

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)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n'] eqn: Heq; constructor.
  - constructor; cbn.
    rewrite Heq.
    apply sim_refl.
  - constructor; cbn.
    rewrite Heq.
    apply (CH n' m).
Abort.
(* end hide *)

Lemma eq_sim :
  forall n m : conat,
    n = m -> sim n m.
(* begin hide *)
Proof.
  destruct 1.
  apply sim_refl.
Qed.
(* end hide *)

Lemma add_assoc :
  forall a b c : conat,
    sim (add (add a b) c) (add a (add b c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out a) as [| a'] eqn: Ha.
  - now apply (sim_refl (add b c)).
  - constructor.
    now apply CH.
Qed.
(* end hide *)

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).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n'] eqn: Hn, (out m) as [| m'] eqn: Hm.
  - now constructor.
  - constructor.
    now rewrite add_zero_r'.
  - constructor.
    now rewrite add_zero_r'.
  - constructor.
    rewrite (CH n' m).
Restart.
  intros n m.
  apply sim_gfp with sim2'; cycle 1.
  - constructor.
    constructor 3.
  - intros n1 n2 [H]; inversion H.
    + now constructor.
    + now constructor.
    + cbn in *.
      destruct (out n0), (out m0); constructor.
      * constructor.
        rewrite <- H1, <- H2 in H.
        now apply wut in H.
      * constructor.
        rewrite <- H1, <- H2 in H.
        now apply wut in H.
      * constructor.
        rewrite <- H1, <- H2 in H.
        now apply wut in H.
Qed.
(* end hide *)

Lemma sim_add :
  forall n1 n2 m1 m2 : conat,
    sim n1 n2 -> sim m1 m2 -> sim (add n1 m1) (add n2 m2).
(* begin hide *)
Proof.
  cofix CH.
  intros n1 n2 m1 m2 [Hn] [Hm].
  constructor; cbn.
  inversion Hn; inversion Hm; constructor; [easy | ..].
  - now rewrite !add_zero_r'.
  - now apply CH.
Qed.
(* end hide *)

(** * 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
|}.

(* begin hide *)
CoFixpoint add'' (n m : conat) : conat :=
match out n, out m with
| Z   , _    => m
| _   , Z    => n
| S n', S m' => succ (succ (add'' n' m'))
end.
(* end hide *)

Lemma sim_add_add' :
  forall n m : conat,
    sim (add n m) (add' n m).
(* begin hide *)
Proof.
  (* To raczej nie przejdzie *)
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n'].
  - now apply sim_refl.
  - destruct (out m) as [| m'] eqn: Heq.
    + constructor.
      now rewrite add_zero_r'.
    +
Abort.
(* end hide *)

Lemma add'_comm :
  forall n m : conat,
    sim (add' n m) (add' m n).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n'], (out m) as [| m']; constructor; [easy.. |].
  do 2 (constructor; cbn).
  apply CH.
Qed.
(* end hide *)

Lemma add'_zero_l :
  forall n m : conat,
    out n = Z -> sim (add' n m) m.
(* begin hide *)
Proof.
  intros n m Hn.
  constructor; cbn.
  rewrite Hn.
  now apply sim_refl.
Qed.
(* end hide *)

Lemma add'_zero_r :
  forall n m : conat,
    out m = Z -> sim (add' n m) n.
(* begin hide *)
Proof.
  intros.
  rewrite add'_comm.
  now apply add'_zero_l.
Qed.
(* end hide *)

Lemma sim_add'_zero :
  forall n m : conat,
    sim (add' n m) zero -> sim n zero /\ sim m zero.
(* begin hide *)
Proof.
  intros n m [H]; inversion H; cbn in *.
  destruct (out n) as [| n'] eqn: Hn,
           (out m) as [| m'] eqn: Hm;
    [| now congruence..].
  now split; constructor; cbn; rewrite ?Hn, ?Hm; constructor.
Qed.
(* end hide *)

Lemma sim_add'_zero_l :
  forall n m : conat,
    sim (add' n m) zero -> sim n zero.
(* begin hide *)
Proof.
  now intros n m [H _]%sim_add'_zero.
Qed.
(* end hide *)

Lemma sim_add'_zero_r :
  forall n m : conat,
    sim (add' n m) zero -> sim m zero.
(* begin hide *)
Proof.
  now intros n m [_ H]%sim_add'_zero.
Qed.
(* end hide *)

Lemma add'_omega_l :
  forall n : conat,
    sim (add' omega n) omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n'].
  - now constructor.
  - constructor; cbn.
    do 2 (constructor; cbn).
    now apply CH.
Qed.
(* end hide *)

Lemma add'_omega_r :
  forall n : conat,
    sim (add' n omega) omega.
(* begin hide *)
Proof.
  intros.
  rewrite add'_comm.
  now apply add'_omega_l.
Qed.
(* end hide *)

Lemma add'_S_l :
  forall n n' m : conat,
    out n = S n' -> sim (add' n m) (succ (add' n' m)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  rewrite H.
  destruct (out m) as [| m'] eqn: Hm; constructor.
  - now rewrite add'_zero_r.
  - constructor; cbn.
    rewrite Hm.
    destruct (out n') as [| n''] eqn: Hn'; constructor.
    + now rewrite add'_zero_l.
    + now apply CH.
Defined.
(* end hide *)

Lemma add'_S_r :
  forall n m m' : conat,
    out m = S m' -> sim (add' n m) (succ (add' n m')).
(* begin hide *)
Proof.
  intros.
  rewrite add'_comm.
  rewrite add'_S_l; [| eassumption].
  apply sim_succ.
  now rewrite add'_comm.
Qed.
(* end hide *)

Lemma add'_succ_l :
  forall n m : conat,
    sim (add' (succ n) m) (succ (add' n m)).
(* begin hide *)
Proof.
  now intros; rewrite add'_S_l.
Qed.
(* end hide *)

Lemma add'_succ_r :
  forall n m : conat,
    sim (add' n (succ m)) (succ (add' n m)).
(* begin hide *)
Proof.
  now intros; rewrite add'_S_r.
Defined.
(* end hide *)

Lemma add'_succ_l' :
  forall n m : conat,
    sim (add' (succ n) m) (add' n (succ m)).
(* begin hide *)
Proof.
  now intros; rewrite add'_succ_l, add'_succ_r.
Qed.
(* end hide *)

Lemma add'_succ_r' :
  forall n m : conat,
    sim (add' n (succ m)) (add' (succ n) m).
(* begin hide *)
Proof.
  now intros; rewrite add'_succ_l, add'_succ_r.
Qed.
(* end hide *)

#[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).
(* begin hide *)
Proof.
  cofix CH.
  intros n1 n2 m1 m2 [Hn] [Hm].
  constructor; cbn.
  inversion Hn; inversion Hm; constructor; [easy.. |].
  constructor; cbn; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma add'_comp :
  forall n m : conat,
    sim (add' (succ n) (succ m)) (succ (succ (add' n m))).
(* begin hide *)
Proof.
  now do 2 (constructor; cbn; constructor).
Qed.
(* end hide *)

Require Import SetoidClass.

#[export]
Instance sim_add'' :
  Proper (sim ==> sim ==> sim) add'.
(* begin hide *)
Proof.
  cofix CH.
  intros n1 n2 [Hn] m1 m2 [Hm].
  constructor; cbn.
  inversion Hn; inversion Hm; constructor; [easy.. |].
  constructor; cbn; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma add'_assoc :
  forall a b c : conat,
    sim (add' (add' a b) c) (add' a (add' b c)).
(* begin hide *)
Proof.
  cofix CH.
  intros a b c.
  destruct (out a) as [| n'] eqn: Heq.
  - now rewrite !(add'_zero_l a).
  - rewrite (add'_S_l a); [| eassumption].
    rewrite add'_succ_l.
    rewrite (add'_S_l a); [| eassumption].
    apply sim_succ.
    apply CH.
Restart.
  cofix CH.
  constructor; cbn.
  destruct (out a) as [| a'], (out b) as [| b'], (out c) as [| c']; constructor; [easy.. |].
  constructor; cbn; constructor.
  constructor; cbn.
  destruct (out a') as [| a''] eqn: Ha,
           (out c') as [| c''] eqn: Hc;
    constructor; cbn.
  - rewrite add'_zero_l by easy.
    rewrite add'_zero_r by easy.
    easy.
  - change {| out := _ |} with (succ (add' (add' a' b') c'')).
    rewrite <- add'_succ_r.
    apply sim_add'.
    + now rewrite add'_zero_l.
    + now constructor; cbn; rewrite Hc; constructor.
  - change {| out := _ |} with (succ (add' a'' (add' b' c'))).
    rewrite <- add'_succ_l.
    apply sim_add'.
    + now constructor; cbn; rewrite Ha; constructor.
    + now rewrite add'_zero_r.
  - constructor; cbn; constructor.
    constructor; cbn.
    rewrite Ha, Hc.
    destruct (out a'') as [| a'''], (out b') as [| b''], (out c'') as [| c'''].
      constructor.
Abort.
(* end hide *)

(** * Porządek *)

(** Zdefiniuj relację [<=] na liczbach konaturalnych i udowodnij jej
    podstawowe właściwości. *)

(* begin hide *)
Inductive leF (R : conat -> conat -> Prop) : NatF conat -> NatF conat -> Prop :=
| leF_Z : forall m : NatF conat, leF R Z m
| leF_S : forall n m : conat, R n m -> leF R (S n) (S m).

CoInductive le (n m : conat) : Prop :=
{
  le' : leF le (out n) (out m);
}.
(* end hide *)

Lemma le_0_l :
  forall n : conat,
    le zero n.
(* begin hide *)
Proof.
  now constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma le_0_r :
  forall n : conat,
    le n zero -> sim n zero.
(* begin hide *)
Proof.
  intros n [H].
  constructor; cbn.
  inversion H.
  now constructor.
Qed.
(* end hide *)

Lemma le_succ :
  forall n m : conat,
    le n m -> le (succ n) (succ m).
(* begin hide *)
Proof.
  now constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma le_succ_conv :
  forall n m : conat,
    le (succ n) (succ m) -> le n m.
(* begin hide *)
Proof.
  now intros n m [H]; inversion H.
Qed.
(* end hide *)

Lemma le_refl :
  forall n : conat,
    le n n.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n']; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma le_trans :
  forall a b c : conat,
    le a b -> le b c -> le a c.
(* begin hide *)
Proof.
  cofix CH.
  intros a b c [Hab] [Hbc].
  constructor.
  inversion Hab; inversion Hbc; subst;
    [| | congruence |]; constructor.
  now eapply CH; [eassumption | congruence].
Qed.
(* end hide *)

Lemma le_univalent :
  forall n m : conat,
    le n m -> le m n -> sim n m.
(* begin hide *)
Proof.
  cofix CH.
  intros n m [Hnm] [Hmn].
  constructor.
  inversion Hnm; inversion Hmn; subst;
    [constructor | congruence.. | constructor].
  now apply CH; [| congruence].
Qed.
(* end hide *)

Lemma le_sim :
  forall n1 n2 m1 m2 : conat,
    sim n1 n2 -> sim m1 m2 -> le n1 m1 -> le n2 m2.
(* begin hide *)
Proof.
  cofix CH.
  intros n1 n2 m1 m2 [Hn] [Hm] [Hnm].
  constructor.
  inversion Hn; inversion Hm; inversion Hnm; subst; try congruence.
  - now constructor.
  - constructor.
    apply (CH _ _ _ _ H1 H4).
    now congruence.
Qed.
(* end hide *)

Lemma le_omega_r :
  forall n : conat,
    le n omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n']; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma le_omega_l :
  forall n : conat,
    le omega n -> sim n omega.
(* begin hide *)
Proof.
  cofix CH.
  intros n [H].
  constructor; cbn.
  inversion H; cbn in *.
  constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma le_succ_r' :
  forall n m m' : conat,
    out m = S m' -> le n m' -> le n m.
(* begin hide *)
Proof.
  cofix CH.
  intros n m m' Hm [Hle].
  constructor; cbn.
  rewrite Hm.
  inversion Hle; constructor.
  now apply CH with m0.
Qed.

Lemma le_succ_r :
  forall n m : conat,
    le n m -> le n (succ m).
(* begin hide *)
Proof.
  now intros; eapply le_succ_r'.
Qed.
(* end hide *)

Lemma le_add_l :
  forall a b c : conat,
    le a b -> le a (add b c).
(* begin hide *)
Proof.
  cofix CH.
  intros a b c [H].
  constructor; cbn.
  inversion H; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma le_add_r :
  forall a b c : conat,
    le a c -> le a (add b c).
(* begin hide *)
Proof.
  cofix CH.
  intros a b c [H].
  constructor; cbn.
  inversion H; [now constructor |].
  destruct (out b) as [| b']; constructor; [easy |].
  apply CH.
  apply le_trans with m; [easy |].
Abort.
(* end hide *)

Lemma le_add'_r :
  forall a b c : conat,
    le a c -> le a (add' b c).
(* begin hide *)
Proof.
  cofix CH.
  intros a b c [H].
  constructor; cbn.
  inversion H; [now constructor |].
  destruct (out b) as [| b']; constructor; [easy |].
  constructor; cbn.
  destruct (out n) as [| n'] eqn: Hn; constructor.
  apply CH.
  apply le_trans with n; [| easy].
  eapply le_succ_r'; [eassumption |].
  apply le_refl.
Qed.
(* end hide *)

Lemma le_add :
  forall n1 n2 m1 m2 : conat,
    le n1 n2 -> le m1 m2 -> le (add n1 m1) (add n2 m2).
(* begin hide *)
Proof.
  cofix CH.
  intros n1 n2 m1 m2 [Hn] [Hm].
  constructor; cbn.
  inversion Hn; inversion Hm.
  - now constructor.
  - rewrite <- H1.
    destruct m; constructor; [easy |].
    apply le_add_l.
Admitted.
(* end hide *)

Lemma le_add_l' :
  forall n m : conat,
    le n (add n m).
(* begin hide *)
Proof.
  intros; apply le_add_l, le_refl.
Qed.
(* end hide *)

#[export]
Instance Proper_le :
  Proper (sim ==> sim ==> iff) le.
(* begin hide *)
Proof.
  now split; apply le_sim.
Qed.
(* end hide *)

#[export]
Instance Proper_le' :
  Proper (sim ==> sim ==> Basics.flip Basics.impl) le.
(* begin hide *)
Proof.
  intros n1 n2 Hn m1 m2 Hm Hle.
  now eapply le_sim; [symmetry.. | apply Hle].
Qed.
(* end hide *)

Lemma le_add_r' :
  forall n m : conat,
    le m (add n m).
(* begin hide *)
Proof.
  cofix CH.
  intros.
  destruct (out n) as [| n'] eqn: Heq.
  - now rewrite add_zero_l; [apply le_refl |].
  - constructor; cbn.
    rewrite Heq.
    destruct (out m) as [| m']; constructor.
Abort.
(* end hide *)

Lemma le_add'_r' :
  forall n m : conat,
    le m (add' n m).
(* begin hide *)
Proof.
  intros.
  apply le_add'_r, le_refl.
Qed.
(* end hide *)

Lemma le_add_l'' :
  forall n n' m : conat,
    le n n' -> le (add n m) (add n' m).
(* begin hide *)
Proof.
  now intros; apply le_add; [| apply le_refl].
Qed.
(* end hide *)

Lemma le_add_r'' :
  forall n m m' : conat,
    le m m' -> le (add n m) (add n m').
(* begin hide *)
Proof.
  now intros; apply le_add; [apply le_refl |].
Qed.
(* end hide *)

(** * Minimum i maksimum *)

(** Zdefiniuj funkcje [min] i [max] i udowodnij ich właściwości. *)

(* begin hide *)
CoFixpoint min (n m : conat) : conat :=
{|
  out :=
    match out n, out m with
    | Z, _ => Z
    | _, Z => Z
    | S n', S m' => S (min n' m')
    end;
|}.

CoFixpoint max (n m : conat) : conat :=
{|
  out :=
    match out n, out m with
    | Z, _ => out m
    | _, Z => out n
    | S n', S m' => S (max n' m')
    end;
|}.
(* end hide *)

Lemma min_zero_l :
  forall n : conat,
    sim (min zero n) zero.
(* begin hide *)
Proof.
  now constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma min_zero_r :
  forall n : conat,
    sim (min n zero) zero.
(* begin hide *)
Proof.
  constructor; cbn.
  now destruct (out n); constructor.
Qed.
(* end hide *)

Lemma min_omega_l :
  forall n : conat,
    sim (min omega n) n.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n']; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma min_omega_r :
  forall n : conat,
    sim (min n omega) n.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n']; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma min_succ :
  forall n m : conat,
    sim (min (succ n) (succ m)) (succ (min n m)).
(* begin hide *)
Proof.
  now constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma max_zero_l :
  forall n : conat,
    sim (max zero n) n.
(* begin hide *)
Proof.
  constructor; cbn.
  now apply sim_refl.
Qed.
(* end hide *)

Lemma max_zero_r :
  forall n : conat,
    sim (max n zero) n.
(* begin hide *)
Proof.
  constructor; cbn.
  now destruct (out n) as [| n']; constructor.
Qed.
(* end hide *)

Lemma max_omega_l :
  forall n : conat,
    sim (max omega n) omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n']; constructor; [easy |].
  now apply CH.
Qed.
(* end hide *)

Lemma max_omega_r :
  forall n : conat,
    sim (max n omega) omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n']; constructor; [easy |].
  now apply CH.
Qed.
(* end hide *)

Lemma max_succ :
  forall n m : conat,
    sim (max (succ n) (succ m)) (succ (max n m)).
(* begin hide *)
Proof.
  now constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma min_assoc :
  forall a b c : conat,
    sim (min (min a b) c) (min a (min b c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out a), (out b), (out c); constructor.
Qed.
(* end hide *)

Lemma max_assoc :
  forall a b c : conat,
    sim (max (max a b) c) (max a (max b c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out a), (out b), (out c); constructor.
Qed.
(* end hide *)

Lemma min_comm :
  forall n m : conat,
    sim (min n m) (min m n).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out n), (out m); constructor.
Qed.
(* end hide *)

Lemma max_comm :
  forall n m : conat,
    sim (max n m) (max m n).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out n), (out m); constructor.
Qed.
(* end hide *)

Lemma min_le :
  forall n m : conat,
    le n m -> sim (min n m) n.
(* begin hide *)
Proof.
  cofix CH.
  intros n m [Hle].
  constructor; cbn.
  inversion Hle; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma max_le :
  forall n m : conat, le n m -> sim (max n m) m.
(* begin hide *)
Proof.
  cofix CH.
  intros n m [Hle].
  constructor; cbn.
  inversion Hle.
  - now apply sim_refl.
  - constructor.
    now apply CH.
Qed.
(* end hide *)

Lemma min_diag :
  forall n : conat,
    sim (min n n) n.
(* begin hide *)
Proof.
  now intros; apply min_le, le_refl.
Qed.
(* end hide *)

Lemma max_diag :
  forall n : conat,
    sim (max n n) n.
(* begin hide *)
Proof.
  now intros; apply max_le, le_refl.
Qed.
(* end hide *)

Lemma min_add_l :
  forall a b c : conat,
    sim (min (add a b) (add a c)) (add a (min b c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out a), (out b), (out c); constructor.
Qed.
(* end hide *)

Lemma min_add_r :
  forall a b c : conat,
    sim (min (add a c) (add b c)) (add (min a b) c).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out a) as [| a'], (out b) as [| b'], (out c) as [| c']; constructor.
  - now apply min_diag.
  - admit.
  - admit.
  - easy.
  - easy.
Abort.
(* end hide *)

Lemma min_add'_l :
  forall a b c : conat,
    sim (min (add' a b) (add' a c)) (add' a (min b c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out a), (out b), (out c); constructor; [easy | ..].
  - apply min_diag.
Abort.
(* end hide *)

Lemma min_add'_r :
  forall a b c : conat,
    sim (min (add' a c) (add' b c)) (add' (min a b) c).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out a) as [| a'], (out b) as [| b'], (out c) as [| c']; constructor.
  - now apply min_diag.
  - admit.
  - admit.
  - easy.
Abort.
(* end hide *)

Lemma max_add_l :
  forall a b c : conat,
    sim (max (add a b) (add a c)) (add a (max b c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out a), (out b), (out c); constructor.
Qed.
(* end hide *)

Lemma max_add_r :
  forall a b c : conat,
    sim (max (add a c) (add b c)) (add (max a b) c).
(* begin hide *)
Proof.
  cofix CH.
  constructor.
  destruct (out a).
Abort.
(* end hide *)

Lemma sim_min_max :
  forall n m : conat,
    sim (min n m) (max n m) -> sim n m.
(* begin hide *)
Proof.
  cofix CH.
  intros n m [H]; cbn in H.
  constructor.
  destruct (out n) as [| n'], (out m) as [| m'];
    inversion H; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma min_max :
  forall a b : conat,
    sim (min a (max a b)) a.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out a), (out b); constructor.
  - apply min_diag.
  - apply CH.
Qed.
(* end hide *)

Lemma max_min :
  forall a b : conat,
    sim (max a (min a b)) a.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out a), (out b); constructor.
Qed.
(* end hide *)

Lemma min_max_distr :
  forall a b c : conat,
    sim (min a (max b c)) (max (min a b) (min a c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  now destruct (out a), (out b), (out c); constructor.
Qed.
(* end hide *)

Lemma max_min_distr :
  forall a b c : conat,
    sim (max a (min b c)) (min (max a b) (max a c)).
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out a), (out b), (out c); constructor; [try easy.. |].
  - now symmetry; apply min_diag.
  - now rewrite min_max.
  - now rewrite min_comm, min_max.
  - now apply CH.
Qed.
(* end hide *)

(** * Dzielenie przez 2 *)

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

(* begin hide *)
CoFixpoint div2 (n : conat) : conat :=
{|
  out :=
    match out n with
    | Z => Z
    | S n' =>
      match out n' with
      | Z => Z
      | S n'' => S (div2 n'')
      end
    end;
|}.
(* end hide *)

Lemma div2_zero :
  sim (div2 zero) zero.
(* begin hide *)
Proof.
  constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma div2_omega :
  sim (div2 omega) omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn; constructor.
  apply CH.
Qed.
(* end hide *)

Lemma div2_succ :
  forall n : conat,
    sim (div2 (succ (succ n))) (succ (div2 n)).
(* begin hide *)
Proof.
  now constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma div2_add' :
  forall n : conat,
    sim (div2 (add' n n)) n.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn.
  destruct (out n) as [| n']; cbn; constructor.
  apply CH.
Qed.
(* end hide *)

Lemma le_div2_l' :
  forall n m : conat,
    le n m -> le (div2 n) m.
(* begin hide *)
Proof.
  cofix CH.
  intros n m [H].
  constructor; cbn.
  inversion H as [| n' m' [H']]; [constructor |].
  inversion H'; constructor.
  apply CH.
  setoid_replace m' with (succ m0) using relation sim.
  - apply le_trans with m0; [easy |].
    apply le_succ_r, le_refl.
  - constructor; cbn.
    rewrite <- H3.
    now constructor.
Qed.
(* end hide *)

Lemma le_div2_l :
  forall n : conat,
    le (div2 n) n.
(* begin hide *)
Proof.
  intros; apply le_div2_l', le_refl.
Qed.
(* end hide *)

Lemma le_div2 :
  forall n m : conat,
    le n m -> le (div2 n) (div2 m).
(* begin hide *)
Proof.
  cofix CH.
  intros n m [H].
  constructor; cbn.
  inversion H as [| n' m' [H'] Hn Hm]; [constructor |].
  inversion H'; constructor.
  now apply CH.
Qed.
(* end hide *)

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

(* begin hide *)

Inductive Finite : conat -> Prop :=
| Finite_zero : Finite zero
| Finite_succ : forall n : conat, Finite n -> Finite (succ n).

Inductive FiniteF (P : conat -> Prop) : NatF conat -> Prop :=
| FiniteF_Z : FiniteF P Z
| FiniteF_S : forall n : conat, P n -> FiniteF P (S n).

Inductive Finite' (n : conat) : Prop :=
| Finite'' : FiniteF Finite' (out n) -> Finite' n.

Inductive InfiniteF (P : conat -> Prop) : NatF conat -> Prop :=
| InfiniteF' :
    forall (n : conat),
      P n -> InfiniteF P (S n).

CoInductive Infinite (n : conat) : Prop :=
{
  Infinite' : InfiniteF Infinite (out n);
}.
(* end hide *)

Lemma Finite_sim :
  forall n1 n2 : conat,
    sim n1 n2 -> Finite n1 -> Finite n2.
(* begin hide *)
Proof.
  intros n1 n2 Hs Hf; revert n2 Hs.
  induction Hf; intros n2 [Hs].
  - inversion Hs.
Admitted.
(* end hide *)

Lemma Finite_zero' :
  Finite zero.
(* begin hide *)
Proof.
  constructor.
Qed.
(* end hide *)

Lemma Finite_Z :
  forall n : conat,
    out n = Z -> Finite n.
(* begin hide *)
Proof.
  intros n Heq.
Admitted.
(* end hide *)

Lemma omega_not_Finite :
  ~ Finite omega.
(* begin hide *)
Proof.
  intros HF.
  remember omega as n; revert Heqn.
  induction HF; intros.
  - apply (f_equal out) in Heqn; inversion Heqn.
  - apply (f_equal out) in Heqn as [=]; cbn in H.
    now apply IHHF.
Qed.
(* end hide *)

Lemma Infinite_omega :
  Infinite omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma Infinite_omega' :
  forall n : conat,
    Infinite n -> sim n omega.
(* begin hide *)
Proof.
  cofix CH.
  intros n [H].
  constructor; cbn.
  inversion H; constructor.
  now apply CH.
Qed.
(* end hide *)

Lemma Finite_Infinite :
  forall n : conat,
    Finite n -> Infinite n -> False.
(* begin hide *)
Proof.
  induction 1; intros [HI]; inversion HI.
  now apply IHFinite.
Qed.
(* end hide *)

Lemma sim_add_Finite :
  forall a b c : conat,
    Finite c -> sim (add a c) (add b c) -> sim a b.
(* begin hide *)
Proof.
  intros a b c H; revert a b.
  induction H; cbn; intros.
  - now rewrite !add_zero_r in H.
  - apply IHFinite.
Admitted.
(* end hide *)

Lemma sim_add'_Finite :
  forall a b c : conat,
    Finite c -> sim (add' a c) (add' b c) -> sim a b.
(* begin hide *)
Proof.
  intros a b c H; revert a b.
  induction H; cbn; intros.
  - now rewrite !add'_zero_r in H.
  - apply IHFinite.
    apply sim_succ_conv.
    now rewrite <- !add'_succ_r.
Qed.
(* end hide *)

Lemma Finite_add :
  forall n m : conat,
    Finite n -> Finite m -> Finite (add n m).
(* begin hide *)
Proof.
  intros until 1. revert m.
  induction H; intros.
    rewrite add_zero_l.
      assumption.
      reflexivity.
    apply Finite_sim with (succ (add n m)).
      rewrite add_succ_l. reflexivity.
      constructor. apply IHFinite. assumption.
Qed.
(* end hide *)

Lemma Finite_add_inv_l :
  forall n m : conat,
    Finite (add n m) -> Finite n.
(* begin hide *)
Proof.
  intros.
  remember (add n m) as c. revert n m Heqc.
  induction H; intros.
  - symmetry in Heqc; apply eq_sim, sim_add_zero in Heqc as [-> _].
    constructor.
  - apply (f_equal out) in Heqc; cbn in Heqc.
    destruct (out n0) as [| n'] eqn: Heq.
    + admit.
    + inversion Heqc.
Admitted.
(* end hide *)

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

(* begin hide *)
Inductive EvenF (P : conat -> Prop) : NatF conat -> Prop :=
| EvenF_Z  : EvenF P Z
| EvenF_SS :
    forall (n n' : conat), out n = S n' -> P n' -> EvenF P (S n).

CoInductive Even (n : conat) : Prop :=
{
  Even' : EvenF Even (out n)
}.

Inductive OddF (P : conat -> Prop) : NatF conat -> Prop :=
| OddF_SZ :
    forall (n : conat), out n = Z -> OddF P (S n)
| OddF_SS :
    forall (n n' : conat), out n = S n' -> P n' -> OddF P (S n).

CoInductive Odd (n : conat) : Prop :=
{
  Odd' : OddF Odd (out n);
}.
(* end hide *)

Lemma Even_zero :
  Even zero.
(* begin hide *)
Proof.
  constructor; cbn; constructor.
Qed.
(* end hide *)

Lemma Odd_zero :
  ~ Odd zero.
(* begin hide *)
Proof.
  intros [H]; inversion H.
Qed.
(* end hide *)

Lemma Even_Omega :
  Even omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn; econstructor; [now cbn |].
  apply CH.
Qed.
(* end hide *)

Lemma Odd_Omega :
  Odd omega.
(* begin hide *)
Proof.
  cofix CH.
  constructor; cbn; econstructor 2; [now cbn |].
  apply CH.
Qed.
(* end hide *)

Lemma Even_Odd_Infinite :
  forall n : conat,
    Even n -> Odd n -> Infinite n.
(* begin hide *)
Proof.
  cofix CH.
  intros n [HE] [HO].
  constructor.
  inversion HO; constructor.
  - rewrite <- H in HE.
    inversion HE; congruence.
  - constructor; rewrite H0; constructor.
    apply CH; [| easy].
    inversion HE; congruence.
Qed.
(* end hide *)

Lemma Even_sim :
  forall n m : conat,
    sim n m -> Even n -> Even m.
(* begin hide *)
Proof.
  cofix CH.
  intros n m [Hs] [HE].
  constructor.
  inversion HE.
  - rewrite <- H0 in Hs.
    inversion Hs.
    constructor.
  -
Abort.
(* end hide *)

Lemma Even_S :
  forall n n' : conat,
    out n = S n' -> Odd n' -> Even n.
(* begin hide *)
Proof.
  cofix CH.
  intros n n' Heq [HO].
  constructor; cbn; rewrite Heq.
  inversion HO.
  - econstructor 2 with n0; [easy |].
    constructor; rewrite H0; constructor.
  - econstructor 2 with n0; [easy |].
    now eapply CH; [eassumption |].
Qed.
(* end hide *)

Lemma Even_S_conv :
  forall n n' : conat,
    out n = S n' -> Even n -> Odd n'.
(* begin hide *)
Proof.
  cofix CH.
  intros n n' Heq [HE].
  constructor.
  rewrite Heq in HE.
  inversion HE as [| ? n'' Heq' HE']; subst.
  rewrite Heq'.
  destruct (out n'') as [| n'''] eqn: Heq''.
  - now constructor.
  - econstructor 2 with n'''; [easy |].
    now eapply CH; [| apply HE'].
Qed.
(* end hide *)

Lemma Even_succ :
  forall n : conat,
    Odd n -> Even (succ n).
(* begin hide *)
Proof.
  now intros; eapply Even_S; cbn.
Qed.
(* end hide *)

Lemma Even_succ_conv :
  forall n : conat,
    Even (succ n) -> Odd n.
(* begin hide *)
Proof.
  now intros; eapply Even_S_conv; [| eassumption].
Qed.
(* end hide *)

Lemma Odd_S :
  forall n n' : conat,
    out n = S n' -> Even n' -> Odd n.
(* begin hide *)
Proof.
  cofix CH.
  intros n n' Heq [HE].
  constructor; cbn; rewrite Heq.
  inversion HE.
  - now constructor 1.
  - econstructor 2 with n0; [easy |].
    now eapply CH; [eassumption |].
Qed.
(* end hide *)

Lemma Odd_S_conv :
  forall n n' : conat,
    out n = S n' -> Odd n -> Even n'.
(* begin hide *)
Proof.
  cofix CH.
  intros n n' Heq [HO].
  constructor.
  rewrite Heq in HO.
  inversion HO as [| ? n'' Heq' HO']; subst.
  - rewrite H; constructor.
  - rewrite Heq'.
    destruct (out n'') as [| n'''] eqn: Heq''.
    + destruct HO' as [HO'']; inversion HO''; congruence.
    + econstructor 2 with n'''; [easy |].
      now eapply CH; [| eassumption].
Qed.
(* end hide *)

Lemma Odd_succ :
  forall n : conat,
    Even n -> Odd (succ n).
(* begin hide *)
Proof.
  now intros; eapply Odd_S.
Qed.
(* end hide *)

Lemma Odd_succ_conv :
  forall n : conat,
    Odd (succ n) -> Even n.
(* begin hide *)
Proof.
  now intros; eapply Odd_S_conv; [| eassumption].
Qed.
(* end hide *)

Lemma Finite_Even_Odd :
  forall n : conat,
    Finite n -> Even n \/ Odd n.
(* begin hide *)
Proof.
  induction 1.
  - left; do 2 constructor.
  - destruct IHFinite; [right | left].
    + now apply Odd_succ.
    + now apply Even_succ.
Qed.
(* end hide *)

Lemma Finite_not_both_Even_Odd :
  forall n : conat,
    Finite n -> ~ (Even n /\ Odd n).
(* begin hide *)
Proof.
  induction 1; intros [HE HO].
  - destruct HO as [HO']; inversion HO'.
  - apply IHFinite; split.
    + now apply Odd_succ_conv.
    + now apply Even_succ_conv.
Qed.
(* end hide *)

Lemma Even_add_Odd :
  forall n m : conat,
    Odd n -> Odd m -> Even (add n m).
(* begin hide *)
Proof.
  cofix CH.
  intros n m [Hn] [Hm].
  constructor; cbn.
  inversion Hn.
  - inversion Hm.
    + econstructor 2 with n1; cbn.
      * now rewrite H0.
      * apply Odd_succ_conv.
        constructor; cbn.
        congruence.
    + econstructor 2 with n1; cbn.
      * now rewrite H0.
      * apply Odd_succ_conv.
        constructor; cbn.
        congruence.
  - econstructor 2 with (add n' m); cbn.
    + now rewrite H0.
    + now apply CH.
Qed.
(* end hide *)

Lemma Even_add_Even :
  forall n m : conat,
    Even n -> Even m -> Even (add n m).
(* begin hide *)
Proof.
  cofix CH.
  intros n m [Hn] Hm.
  constructor; cbn.
  inversion Hn; [apply Hm |].
  econstructor 2 with (add n' m); cbn.
  - now rewrite H0.
  - now apply CH.
Qed.
(* end hide *)

Lemma Odd_add :
  forall n m : conat,
    Even n -> Odd m -> Odd (add n m).
(* begin hide *)
Proof.
  cofix CH.
  intros n m [Hn] Hm.
  constructor; cbn.
  inversion Hn; [apply Hm |].
  econstructor 2 with (add n' m); cbn.
  - now rewrite H0.
  - now apply CH.
Qed.
(* end hide *)

(** * 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.
(* begin hide *)
Proof.
  unfold Sub.
  apply add_omega_r.
Qed.
(* end hide *)

(** 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.
(* begin hide *)
Proof.
  intros [f H].
  cut (succ zero = zero); [now inversion 1 |].
  replace (succ zero) with (f omega omega) by apply H, Sub_nondet.
  replace zero with (f omega omega) by apply H, Sub_nondet.
  easy.
Qed.
(* end hide *)

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

(* begin hide *)
Fixpoint subn (n : conat) (m : nat) : conat :=
match out n, m with
| Z, _ => n
| _, 0 => n
| S n', Datatypes.S m' => subn n' m'
end.

Lemma Sub_Finite_sim :
  forall n m r1 r2 : conat,
    Finite n -> Sub n m r1 -> Sub n m r2 -> sim r1 r2.
Proof.
  unfold Sub; intros.
  eapply sim_add_Finite.
    2: { rewrite H0, H1. reflexivity. }
    eapply Finite_add_inv_l. eapply Finite_sim.
Admitted.
(*
      apply add_comm.
      eapply Finite_sim.
        symmetry. exact H0.
        assumption.
Qed.
*)

Definition sub' : Type :=
  {f : conat -> conat -> conat |
    forall n m r : conat, f n m = r -> Sub n m r}.
(* end hide *)

(** * Mnożenie (TODO) *)

(* begin hide *)
CoFixpoint mul' (n m acc : conat) : conat :=
{|
  out :=
    match out n, out m with
    | Z   , _       => out acc
    | _      , Z    => out acc
    | S n', S m' => S (mul' n' m' (add n' (add m' acc)))
    end
|}.

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

Lemma mul'_zero_l :
  forall c acc : conat,
    mul' zero c acc = acc.
(* begin hide *)
Proof.
Admitted.
(* end hide *)

Lemma mul'_zero_r :
  forall n m acc : conat,
    out m = Z -> mul' n m acc = acc.
(* begin hide *)
Proof.
Admitted.
(*
  intros. apply eq_out. cbn. rewrite H. destruct (out n); reflexivity.
Qed.
*)
(* end hide *)

Lemma mul'_comm :
  forall n m acc1 acc2 : conat,
    sim acc1 acc2 ->
      sim (mul' n m acc1) (mul' m n acc2).
(* begin hide *)
Proof.
  cofix CH.
  intros n m acc1 acc2 [Hs].
  constructor; cbn.
  inversion Hs.
  destruct (out n) as [| n'], (out m) as [| m']; only 1-3: now constructor.
  - constructor.
    apply CH.
Admitted.
(*
  - constructor.
  intros [[| n
  inversion ']] [[| m']] acc1 acc2 H.
    1-3: rewrite !mul'_zero_l, ?mul'_zero_r; cbn; auto.
    constructor. eright; cbn; try reflexivity. apply CH. rewrite <- !add_assoc. apply sim_add.
      apply add_comm.
      assumption.
Qed.
*)
(* end hide *)

Lemma mul'_one_l :
  forall c acc : conat,
    sim (mul' (succ zero) c acc) (add c acc).
(* begin hide *)
Proof.
Admitted.
(*
  destruct c as [[| c']]; constructor; cbn.
    destruct acc as [[| acc']]; cbn; eauto.
      eright; cbn; reflexivity.
    eright; cbn; try reflexivity. rewrite mul'_zero_l, add_zero_l; cbn; reflexivity.
Qed.
*)
(* end hide *)

Lemma mul'_one_r :
  forall c acc : conat,
    sim (mul' c (succ zero) acc) (add c acc).
(* begin hide *)
Proof.
  intros. rewrite mul'_comm.
    apply mul'_one_l.
    reflexivity.
Qed.
(* end hide *)

Lemma mul'_omega_l :
  forall c acc : conat,
    out c <> Z ->
      sim (mul' omega c acc) omega.
(* begin hide *)
Proof.
Admitted.
(*
  cofix CH.
  destruct c as [[| c']]; constructor; cbn in *.
    congruence.
    eright; cbn; try reflexivity. destruct c' as [[| c'']].
      rewrite mul'_zero_r, (add_zero_l _ acc).
        apply add_omega_l.
        1-2: reflexivity.
      apply CH. cbn. inversion 1.
Qed.
*)
(* end hide *)

Lemma mul'_omega_r :
  forall c acc : conat,
    out c <> Z ->
      sim (mul' c omega acc) omega.
(* begin hide *)
Proof.
  intros. rewrite mul'_comm.
    apply mul'_omega_l. assumption.
    reflexivity.
Qed.
(* end hide *)

(* 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)).
(* begin hide *)
Proof.
Admitted.
(* end hide *)

Lemma mul'_succ_l :
  forall n m acc : conat,
    sim (mul' (succ n) m acc) (add m (mul' n m acc)).
(* begin hide *)
Proof.
Admitted.
(*
  intros n [[| m']] acc.
    rewrite !mul'_zero_r, add_zero_l; reflexivity.
    constructor; eright; cbn; try reflexivity.
      rewrite !mul'_acc.
Admitted.
*)
(* end hide *)

Lemma Finite_mul' :
  forall n m acc : conat,
    Finite n -> Finite m -> Finite acc ->
      Finite (mul' n m acc).
(* begin hide *)
Proof.
  intros n m acc Hn Hm Hacc.
  revert m acc Hm Hacc.
  induction Hn as [| n' Hn IH]; intros.
    rewrite mul'_zero_l. assumption.
    eapply Finite_sim.
      symmetry. apply mul'_succ_l.
      apply Finite_add.
        assumption.
        apply IH; assumption.
Qed.
(* end hide *)

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').
(* begin hide *)
Proof.
Admitted.
(* end hide *)

(** * Koindukcja wzajemna (TODO) *)

(* begin hide *)
CoInductive Even2 (n : conat) : Prop :=
{
  Even2' :
    out n = Z \/
    exists n' : conat,
      out n = S n' /\ Odd2 n';
}

with Odd2 (n : conat) : Prop :=
{
  Odd2' :
    exists n' : conat,
      out n = S n' /\ Even2 n';
}.
(* end hide *)

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.
(* begin hide *)
Proof.
  intros n [[Hn | [n' [Hn HOdd]]]]; constructor.
    left. assumption.
    right with n'.
      assumption.
      apply Odd2_Odd2'. assumption.

  intros n [[n' [Hn HEven]]]. constructor. exists n'.
    assumption.
    apply Even2_Even2'. assumption.
Qed.
(* end hide *)

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

with Odd2'_Odd2 :
  forall n : conat, Odd2' n -> Odd2 n.
(* begin hide *)
Proof.
  intros n [[Hn | n' Hn HOdd]]; constructor.
    left. assumption.
    right. exists n'. split.
      assumption.
      apply Odd2'_Odd2. assumption.

  intros n [[n' Hn HEven]]. constructor. exists n'. split.
    assumption.
    apply Even2'_Even2. assumption.
Qed.
(* end hide *)

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).
(* begin hide *)
Proof.
  constructor. destruct H as [(n' & H1 & H2)].
    cbn. rewrite H1. right. eexists. intuition.
  constructor.
  destruct H as [[H | (n' & H1 & H2)]],
          H0 as [(m' & H1' & H2')]; subst; cbn.
    rewrite H. exists m'. intuition.
    rewrite H1. exists (add n' m). intuition. apply Even2_add_Odd2.
      assumption.
      constructor. exists m'. auto.
Qed.
(* end hide *)

(** * Liczby naturalne i konaturalne *)

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

(* begin hide *)
Fixpoint from_nat (n : nat) : conat :=
match n with
| 0 => zero
| Datatypes.S n' => succ (from_nat n')
end.
(* end hide *)

Lemma Finite_from_nat :
  forall n : nat, Finite (from_nat n).
(* begin hide *)
Proof.
  induction n as [| n']; cbn; constructor; assumption.
Qed.
(* end hide *)

(** Pokaż, że [from_nat] nie ma żadnej preodwrotności. *)

(* begin hide *)
(* TODO: wyjaśnić wcześniej pojęcie preodwrotności. *)
(* end hide *)

(* begin hide *)
Lemma no_preinverse_aux :
  forall f : conat -> nat,
    from_nat (f omega) <> omega.
Proof.
  intros f H.
  apply omega_not_Finite.
  rewrite <- H.
  apply Finite_from_nat.
Qed.
(* end hide *)

Lemma no_preinverse :
  forall f : conat -> nat,
    (forall c : conat, from_nat (f c) = c) -> False.
(* begin hide *)
Proof.
  intros f H.
  eapply no_preinverse_aux.
  apply H.
Qed.
(* end hide *)

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

(* begin hide *)
Inductive lec : conat -> nat -> Prop :=
| lec_0 : forall n : nat, lec zero n
| lec_S : forall (c : conat) (n : nat), lec c n -> lec (succ c) (Datatypes.S n).

Inductive gtc : conat -> nat -> Prop :=
| gtc_zero : forall c : conat, gtc (succ c) 0
| gtc_S : forall (c : conat) (n : nat), gtc c n -> gtc (succ c) (Datatypes.S n).

Lemma lec_spec :
  forall (n : nat) (c : conat),
    lec c n -> Finite c.
Proof.
  induction 1; constructor; assumption.
Qed.

Lemma gtc_omega :
  forall n : nat, gtc omega n.
Proof.
Admitted.
(*
  induction n as [| n'].
    rewrite sim_succ_omega. constructor.
    rewrite sim_succ_omega. constructor. assumption.
Qed.
*)

Lemma gtc_from_nat :
  forall n : nat, ~ gtc (from_nat n) n.
Proof.
  induction n as [| n']; cbn.
    inversion 1.
    intro. apply IHn'. inversion H. assumption.
Qed.

Lemma conat_nat_order :
  forall (n : nat) (c : conat),
    lec c n \/ gtc c n.
Proof.
Admitted.
(*
  induction n as [| n']; cbn; intro.
    destruct c as [[| c']].
      left. constructor.
      right. constructor.
    destruct c as [[| c']].
      left. constructor.
      destruct (IHn' c') as [IH | IH].
        left. constructor. assumption.
        right. constructor. assumption.
Qed.
*)

Lemma Infinite_not_from_nat :
  forall c : conat,
    (forall n : nat, c <> from_nat n) -> Infinite c.
Proof.
Admitted.
(*
  cofix CH.
  intros [[| c']] H.
    specialize (H 0). cbn in H. contradiction H. reflexivity.
    constructor. exists c'.
      cbn. reflexivity.
      apply CH. intros n H'. apply (H (Datatypes.S n)). subst. cbn. reflexivity.
Qed.
*)
(* end hide *)

Lemma inverse_taboo :
  forall f : conat -> nat,
    (forall n : nat, f (from_nat n) = n) ->
      forall c : conat, Infinite c \/ Finite c.
(* begin hide *)
Proof.
  intros.
  destruct (conat_nat_order (f c) c) as [Hlec | Hgtc].
    right. eapply lec_spec. eassumption.
    left.
    {
      apply Infinite_not_from_nat.
      intros n Heq.
      apply (gtc_from_nat (f c)).
      subst. rewrite H in *.
      assumption.
    }
Qed.
(* end hide *)

(** ** 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).
(* begin hide *)
Proof.
Admitted.
(*
  intros c H.
  apply H. right. revert c H. cofix CH.
  intros [[| c']] H.
    exfalso. apply H. left. constructor.
    constructor. exists c'.
      cbn. reflexivity.
      apply CH. intros [H' | H']; apply H.
        left. constructor. assumption.
        right. constructor. exists c'.
          cbn. reflexivity.
          assumption.
Qed.
*)
(* end hide *)

author: wkolowski

repo: Typonomikon

save_path: github-repos/coq/wkolowski-Typonomikon


text:
(* Full optimizer *)
(* Middle-end then backend *)
(* We use the information from the profiler to choose optimizations *)

Require Import RTL.
Require Import IR.
Require Import monad.
Require Import common.
Require Import Coqlib.
Require Import backend.
Require Import primitives.
Require Import profiler_types.
Require Import middle_end.

(** * The Full Backend Compiler  *)
(* If the profiler suggests a wrong function to optimize, we catch the error and do nothing *)
Definition backend_optimize (ps:profiler_state) (p:program): free unit :=
  match (backend_suggestion ps) with
  | Some fid =>
      do status <<- fprim(Prim_Check_Compiled fid);
      match status with
      | Installed _ => nothing     (* function has already been compiled *)
      | Not_compiled =>
          match ((prog_funlist p) # fid) with
          | Some func =>
              do current_ver <<- fret (current_version func);
              do params <<- fret (fn_params func);
              backend_and_install current_ver fid params (* catching errors that may happen during compilation *)
          | None => nothing            (* Can't find the function to optimize *)
          end
      end
  | None => nothing
  end.

(** * The Full Optimizer, Middle-end + Backend  *)
(* returns a program: the one that has been modified by the middle-end *)
(* but the native code are installed in the executable memory  *)
Definition optimize (ps:profiler_state) (p:program) : free program :=
  do newp <<- fret (safe_middle_end ps p);
  do _ <<- backend_optimize ps newp;
  fret (newp).

author: Aurele-Barriere

repo: JIThm

save_path: github-repos/coq/Aurele-Barriere-JIThm


(**
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/

Copyright (C) 2011-2015 Sylvie Boldo
#
#
Copyright (C) 2011-2015 Catherine Lelay
#
#
Copyright (C) 2011-2015 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.

---------------------------------------------------------------

This version modified to work without SSReflect,
or any other dependencies, as part of the QWIRE project
by Robert Rand and Jennifer Paykin (June 2017).

*)

Require Import Prelim.
Open Scope R_scope.

(******************************************)
(** Relevant lemmas from Rcomplements.v. **)
(******************************************)

Lemma Rle_minus_l : forall a b c,(a - c <= b <-> a <= b + c). Proof. intros. lra. Qed.
Lemma Rlt_minus_r : forall a b c,(a < b - c <-> a + c < b). Proof. intros. lra. Qed.
Lemma Rlt_minus_l : forall a b c,(a - c < b <-> a < b + c). Proof. intros. lra. Qed.
Lemma Rle_minus_r : forall a b c,(a <= b - c <-> a + c <= b). Proof. intros. lra. Qed.
Lemma Rminus_le_0 : forall a b, a <= b <-> 0 <= b - a. Proof. intros. lra. Qed.
Lemma Rminus_lt_0 : forall a b, a < b <-> 0 < b - a. Proof. intros. lra. Qed.

(* Automation *)

Lemma Rminus_unfold : forall r1 r2, (r1 - r2 = r1 + -r2). Proof. reflexivity. Qed.
Lemma Rdiv_unfold : forall r1 r2, (r1 / r2 = r1 */ r2). Proof. reflexivity. Qed.

Hint Rewrite Rminus_unfold Rdiv_unfold Ropp_0 Ropp_involutive Rplus_0_l Rplus_0_r
             Rmult_0_l Rmult_0_r Rmult_1_l Rmult_1_r : R_db.
Hint Rewrite <- Ropp_mult_distr_l Ropp_mult_distr_r : R_db.
Hint Rewrite Rinv_l Rinv_r sqrt_sqrt using lra : R_db.

(*********************)
(** Complex Numbers **)
(*********************)

(** This file defines complex numbers [C] as [R * R]. Operations are
given, and [C] is proved to be a field, a normed module, and a
complete space. *)

(** * The set of complex numbers *)

Definition C := (R * R)%type.

Definition RtoC (x : R) : C := (x,0).
Coercion RtoC : R >-> C.

Lemma RtoC_inj : forall (x y : R),
  RtoC x = RtoC y -> x = y.
Proof.
  intros x y H.
  now apply (f_equal (@fst R R)) in H.
Qed.

Lemma Ceq_dec (z1 z2 : C) : { z1 = z2 } + { z1 <> z2 }.
Proof.
  destruct z1 as [x1 y1].
  destruct z2 as [x2 y2].
  destruct (Req_EM_T x1 x2) as [Eqx | Neqx]; [| right; congruence].
  destruct (Req_EM_T y1 y2) as [Eqy | Neqy]; [subst; auto | right; congruence].
Qed.

(** ** Constants and usual functions *)

(** 0 and 1 for complex are defined as [RtoC 0] and [RtoC 1] *)
Definition Ci : C := (0,1).

(** *** Arithmetic operations *)

Definition Cplus (x y : C) : C := (fst x + fst y, snd x + snd y).
Definition Copp (x : C) : C := (-fst x, -snd x).
Definition Cminus (x y : C) : C := Cplus x (Copp y).
Definition Cmult (x y : C) : C := (fst x * fst y - snd x * snd y, fst x * snd y + snd x * fst y).
Definition Cinv (x : C) : C := (fst x / (fst x ^ 2 + snd x ^ 2), - snd x / (fst x ^ 2 + snd x ^ 2)).
Definition Cdiv (x y : C) : C := Cmult x (Cinv y).

Delimit Scope C_scope with C.
Local Open Scope C_scope.

Infix "+" := Cplus : C_scope.
Notation "- x" := (Copp x) : C_scope.
Infix "-" := Cminus : C_scope.
Infix "*" := Cmult : C_scope.
Notation "/ x" := (Cinv x) : C_scope.
Infix "/" := Cdiv : C_scope.

(* Added exponentiation *)
Fixpoint Cpow (c : C) (n : nat) : C :=
  match n with
  | 0%nat => 1
  | S n' => c * Cpow c n'
  end.

Infix "^" := Cpow : C_scope.

(** *** Other usual functions *)

Definition Re (z : C) : R := fst z.

Definition Im (z : C) : R := snd z.

Definition Cmod (x : C) : R := sqrt (fst x ^ 2 + snd x ^ 2).

Definition Cconj (x : C) : C := (fst x, (- snd x)%R).

Notation "a ^*" := (Cconj a) (at level 10).

Lemma Cmod_0 : Cmod 0 = R0.
Proof.
unfold Cmod.
simpl.
rewrite Rmult_0_l, Rplus_0_l.
apply sqrt_0.
Qed.
Lemma Cmod_1 : Cmod 1 = R1.
Proof.
unfold Cmod.
simpl.
rewrite Rmult_0_l, Rplus_0_r, 2!Rmult_1_l.
apply sqrt_1.
Qed.

Lemma Cmod_opp : forall x, Cmod (-x) = Cmod x.
Proof.
unfold Cmod.
simpl.
intros x.
apply f_equal.
ring.
Qed.

Lemma Cmod_triangle : forall x y, Cmod (x + y) <= Cmod x + Cmod y.
Proof.
  intros x y ; unfold Cmod.
  apply Rsqr_incr_0_var.
  apply Rminus_le_0.
  unfold Rsqr ; simpl ; ring_simplify.
  unfold pow.
  rewrite ?Rmult_1_r.
  rewrite ?sqrt_sqrt ; ring_simplify.
  replace (-2 * fst x * fst y - 2 * snd x * snd y)%R with (- (2 * (fst x * fst y + snd x * snd y)))%R by ring.
  rewrite Rmult_assoc, <- sqrt_mult.
  rewrite Rplus_comm.
  apply -> Rminus_le_0.
  apply Rmult_le_compat_l.
  apply Rlt_le, Rlt_0_2.
  apply Rsqr_incr_0_var.
  apply Rminus_le_0.
  unfold Rsqr; rewrite ?sqrt_sqrt ; ring_simplify.
  replace (fst x ^ 2 * snd y ^ 2 - 2 * fst x * snd x * fst y * snd y +
    snd x ^ 2 * fst y ^ 2)%R with ( (fst x * snd y - snd x * fst y)^2)%R
    by ring.
  apply pow2_ge_0.
  repeat apply Rplus_le_le_0_compat ; apply Rmult_le_pos ; apply pow2_ge_0.
  apply sqrt_pos.
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
  replace (fst x ^ 2 + 2 * fst x * fst y + fst y ^ 2 + snd x ^ 2 + 2 * snd x * snd y + snd y ^ 2)%R
    with ((fst x + fst y)^2 + (snd x + snd y)^2)%R by ring.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply sqrt_pos.
Qed.

Lemma Cmod_mult : forall x y, Cmod (x * y) = (Cmod x * Cmod y)%R.
Proof.
  intros x y.
  unfold Cmod.
  rewrite <- sqrt_mult.
  apply f_equal ; simpl ; ring.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
Qed.

Lemma Rmax_Cmod : forall x,
  Rmax (Rabs (fst x)) (Rabs (snd x)) <= Cmod x.
Proof.
  intros [x y]; simpl.
  rewrite <- !sqrt_Rsqr_abs.
  apply Rmax_case ; apply sqrt_le_1_alt, Rminus_le_0 ;
  unfold Rsqr; simpl ; ring_simplify ; try apply pow2_ge_0; auto.
Qed.
Lemma Cmod_2Rmax : forall x,
  Cmod x <= sqrt 2 * Rmax (Rabs (fst x)) (Rabs (snd x)).
Proof.
  intros [x y]; apply Rmax_case_strong; intros H0;
  rewrite <- !sqrt_Rsqr_abs ;
  rewrite <- ?sqrt_mult ;
  try (apply Rle_0_sqr; auto);
  try (apply Rlt_le, Rlt_0_2; auto) ;
  apply sqrt_le_1_alt ; simpl ; [ rewrite Rplus_comm | ] ;
  unfold Rsqr ; apply Rle_minus_r ; ring_simplify ;
  apply Rsqr_le_abs_1 in H0 ; unfold pow; rewrite !Rmult_1_r; auto.
Qed.

(** ** C is a field *)

Lemma RtoC_plus (x y : R) : RtoC (x + y) = RtoC x + RtoC y.
Proof.
  unfold RtoC, Cplus ; simpl.
  rewrite Rplus_0_r; auto.
Qed.

Lemma RtoC_opp (x : R) : RtoC (- x) = - RtoC x.
Proof.
  unfold RtoC, Copp ; simpl.
  rewrite Ropp_0; auto.
Qed.

Lemma RtoC_minus (x y : R) : RtoC (x - y) = RtoC x - RtoC y.
Proof. unfold Cminus; rewrite <- RtoC_opp, <- RtoC_plus; auto. Qed.

Lemma RtoC_mult (x y : R) : RtoC (x * y) = RtoC x * RtoC y.
Proof.
  unfold RtoC, Cmult ; simpl.
  apply injective_projections ; simpl ; ring.
Qed.

Lemma RtoC_inv (x : R) : (x <> 0)%R -> RtoC (/ x) = / RtoC x.
Proof. intros Hx. apply injective_projections ; simpl ; field ; auto. Qed.

Lemma RtoC_div (x y : R) : (y <> 0)%R -> RtoC (x / y) = RtoC x / RtoC y.
Proof. intros Hy. apply injective_projections ; simpl ; field ; auto. Qed.

Lemma Cplus_comm (x y : C) : x + y = y + x.
Proof. apply injective_projections ; simpl ; apply Rplus_comm. Qed.

Lemma Cplus_assoc (x y z : C) : x + (y + z) = (x + y) + z.
Proof. apply injective_projections ; simpl ; apply sym_eq, Rplus_assoc. Qed.

Lemma Cplus_0_r (x : C) : x + 0 = x.
Proof. apply injective_projections ; simpl ; apply Rplus_0_r. Qed.

Lemma Cplus_0_l (x : C) : 0 + x = x.
Proof. apply injective_projections ; simpl ; apply Rplus_0_l. Qed.

Lemma Cplus_opp_r (x : C) : x + -x = 0.
Proof. apply injective_projections ; simpl ; apply Rplus_opp_r. Qed.

Lemma Copp_plus_distr (z1 z2 : C) : - (z1 + z2) = (- z1 + - z2).
Proof. apply injective_projections ; apply Ropp_plus_distr; auto. Qed.

Lemma Copp_minus_distr (z1 z2 : C) : - (z1 - z2) = z2 - z1.
Proof. apply injective_projections ; apply Ropp_minus_distr; auto. Qed.

Lemma Cmult_comm (x y : C) : x * y = y * x.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_assoc (x y z : C) : x * (y * z) = (x * y) * z.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_0_r (x : C) : x * 0 = 0.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_0_l (x : C) : 0 * x = 0.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_1_r (x : C) : x * 1 = x.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_1_l (x : C) : 1 * x = x.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cinv_r (r : C) : r <> 0 -> r * /r = 1.
Proof.
  intros H.
  apply injective_projections ; simpl ; field.
  contradict H.
  apply Rplus_sqr_eq_0 in H.
  apply injective_projections ; simpl ; apply H.
  contradict H.
  apply Rplus_sqr_eq_0 in H.
  apply injective_projections ; simpl ; apply H.
Qed.

Lemma Cinv_l (r : C) : r <> 0 -> /r * r = 1.
Proof.
intros Zr.
rewrite Cmult_comm.
now apply Cinv_r.
Qed.

Lemma Cmult_plus_distr_l (x y z : C) : x * (y + z) = x * y + x * z.
Proof.
  apply injective_projections ; simpl ; ring.
Qed.

Lemma Cmult_plus_distr_r (x y z : C) : (x + y) * z = x * z + y * z.
Proof.
  apply injective_projections ; simpl ; ring.
Qed.

(* I'll be leaving out mixins and Canonical Structures :
Definition C_AbelianGroup_mixin :=
  AbelianGroup.Mixin _ _ _ _ Cplus_comm Cplus_assoc Cplus_0_r Cplus_opp_r.

Canonical C_AbelianGroup :=
  AbelianGroup.Pack C C_AbelianGroup_mixin C.
*)

Lemma Copp_0 : Copp 0 = 0.
Proof. apply injective_projections; simpl ; ring. Qed.

Lemma Cmod_m1 : Cmod (Copp 1) = 1.
Proof. rewrite Cmod_opp. apply Cmod_1. Qed.

Lemma Cmod_eq_0 : forall x, Cmod x = 0 -> x = 0.
Proof.
  intros x H.
  unfold Cmod, pow in H.
  rewrite 2!Rmult_1_r, <- sqrt_0 in H.
  apply sqrt_inj in H.
  apply Rplus_sqr_eq_0 in H.
  now apply injective_projections.
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
  apply Rle_refl.
Qed.

Lemma Cmod_ge_0 : forall x, 0 <= Cmod x.
Proof.
  intros x.
  apply sqrt_pos.
Qed.

Lemma Cmod_gt_0 :
  forall (x : C), x <> 0 <-> 0 < Cmod x.
Proof.
  intros x ; split; intro Hx.
  destruct (Cmod_ge_0 x); auto.
  apply sym_eq, Cmod_eq_0 in H. tauto.
  contradict Hx.
  apply Rle_not_lt, Req_le.
  rewrite Hx, Cmod_0; auto.
Qed.

Lemma Cmod_R : forall x : R, Cmod x = Rabs x.
Proof.
  intros x.
  unfold Cmod.
  simpl.
  rewrite Rmult_0_l, Rplus_0_r, Rmult_1_r.
  apply sqrt_Rsqr_abs.
Qed.

Lemma Cmod_inv : forall x : C, x <> 0 -> Cmod (/ x) = Rinv (Cmod x).
Proof.
  intros x Zx.
  apply Rmult_eq_reg_l with (Cmod x).
  rewrite <- Cmod_mult.
  rewrite Rinv_r.
  rewrite Cinv_r.
  rewrite Cmod_R.
  apply Rabs_R1.
  exact Zx.
  contradict Zx.
  now apply Cmod_eq_0.
  contradict Zx.
  now apply Cmod_eq_0.
Qed.

Lemma Cmod_div (x y : C) : y <> 0 -> Cmod (x / y) = Rdiv (Cmod x) (Cmod y).
Proof.
  intro Hy.
  unfold Cdiv.
  rewrite Cmod_mult.
  rewrite Cmod_inv; auto.
Qed.

Lemma Cmult_neq_0 (z1 z2 : C) : z1 <> 0 -> z2 <> 0 -> z1 * z2 <> 0.
Proof.
  intros Hz1 Hz2 Hz.
  assert (Cmod (z1 * z2) = 0).
  rewrite Hz, Cmod_0; auto.
  rewrite Cmod_mult in H.
  apply Rmult_integral in H ; destruct H.
  now apply Hz1, Cmod_eq_0.
  now apply Hz2, Cmod_eq_0.
Qed.

Lemma Cminus_eq_contra : forall r1 r2 : C, r1 <> r2 -> r1 - r2 <> 0.
Proof.
  intros ; contradict H ; apply injective_projections ;
  apply Rminus_diag_uniq.
  now apply (f_equal (@fst R R)) in H.
  now apply (f_equal (@snd R R)) in H.
Qed.

Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.
Proof.
constructor.
constructor.
exact Cplus_0_l.
exact Cplus_comm.
exact Cplus_assoc.
exact Cmult_1_l.
exact Cmult_comm.
exact Cmult_assoc.
exact Cmult_plus_distr_r.
easy.
exact Cplus_opp_r.
intros H.
injection H.
exact R1_neq_R0.
easy.
apply Cinv_l.
Qed.

Add Field C_field_field : C_field_theory.

(** Added Lemmas for QWIRE *)

(** Notations *)

Notation C0 := (RtoC 0).
Notation C1 := (RtoC 1).
Notation C2 := (RtoC 2).
Notation "√ n" := (sqrt n) (at level 20).

Lemma RtoC_pow : forall r n, (RtoC r) ^ n = RtoC (r ^ n).
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl.
    rewrite IHn.
    rewrite RtoC_mult.
    reflexivity.
Qed.

Lemma c_proj_eq : forall (c1 c2 : C), fst c1 = fst c2 -> snd c1 = snd c2 -> c1 = c2.
Proof. intros c1 c2 H1 H2. destruct c1, c2. simpl in *. subst. reflexivity. Qed.

Ltac clra := eapply c_proj_eq; simpl; lra.

Lemma Ci2 : Ci * Ci = -C1. Proof. clra. Qed.
Lemma Copp_mult_distr_r : forall c1 c2 : C, - (c1 * c2) = c1 * - c2.
Proof. intros; clra. Qed.
Lemma Copp_mult_distr_l : forall c1 c2 : C, - (c1 * c2) = - c1 * c2.
Proof. intros; clra. Qed.
Lemma Cplus_opp_l : forall c : C, - c + c = 0. Proof. intros; clra. Qed.
Lemma Cdouble : forall c : C, 2 * c = c + c. Proof. intros; clra. Qed.
Lemma Copp_involutive: forall c : C, - - c = c. Proof. intros; clra. Qed.

Lemma C0_imp : forall c : C, c <> 0 -> (fst c <> 0 \/ snd c <> 0)%R.
Proof. intros c H. destruct c. simpl.
       destruct (Req_EM_T r 0), (Req_EM_T r0 0); subst; intuition. Qed.
Lemma C0_fst : forall (c : C), fst c <> 0 -> c <> 0.
Proof. intros c. intros N E. apply N. rewrite E. reflexivity. Qed.
Lemma C0_snd : forall (c : C), snd c <> 0 -> c <> 0.
Proof. intros c. intros N E. apply N. rewrite E. reflexivity. Qed.

Lemma Rmult_div : forall r1 r2 r3 r4 : R, r2 <> 0 -> r4 <> 0 ->
                                     (r1 / r2 * (r3 / r4) = r1 * r3 / (r2 * r4))%R.
Proof. intros. unfold Rdiv. rewrite Rinv_mult_distr; trivial. lra. Qed.

Lemma Rdiv_cancel :  forall r r1 r2 : R, (r1 = r2 -> r / r1 = r / r2)%R.
Proof. intros. rewrite H. reflexivity. Qed.

Lemma Rsum_nonzero : forall r1 r2 : R, (r1 <> 0 \/ r2 <> 0 -> r1 * r1 + r2 * r2 <> 0)%R.
Proof.
  intros.
  replace (r1 * r1)%R with (r1 ^ 2)%R by lra.
  replace (r2 * r2)%R with (r2 ^ 2)%R by lra.
  specialize (pow2_ge_0 (r1)). intros GZ1.
  specialize (pow2_ge_0 (r2)). intros GZ2.
  destruct H.
  - specialize (pow_nonzero r1 2 H). intros NZ. lra.
  - specialize (pow_nonzero r2 2 H). intros NZ. lra.
Qed.

Lemma Cinv_mult_distr : forall c1 c2 : C, c1 <> 0 -> c2 <> 0 -> / (c1 * c2) = / c1 * / c2.
Proof.
  intros.
  apply c_proj_eq.
  - simpl.
    repeat rewrite Rmult_1_r.
    rewrite Rmult_div.
    rewrite Rmult_div.
    rewrite Rmult_opp_opp.
    unfold Rminus.
    rewrite <- RIneq.Ropp_div.
    rewrite <- Rdiv_plus_distr.
    rewrite Rmult_plus_distr_r.
    rewrite Rmult_plus_distr_l.
    apply Rdiv_cancel.
    lra.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
  - simpl.
    repeat rewrite Rmult_1_r.
    rewrite Rmult_div.
    rewrite Rmult_div.
    unfold Rminus.
    rewrite <- Rdiv_plus_distr.
    repeat rewrite Rmult_plus_distr_r.
    repeat rewrite Rmult_plus_distr_l.
    repeat rewrite <- Ropp_mult_distr_r.
    repeat rewrite <- Ropp_mult_distr_l.
    repeat rewrite <- Ropp_plus_distr.
    apply Rdiv_cancel.
    lra.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
Qed.

Lemma Csqrt_sqrt : forall x : R, 0 <= x -> ((RtoC (√ x)) * (RtoC (√ x)) = (RtoC x))%C.
Proof. intros. eapply c_proj_eq; simpl; try rewrite sqrt_sqrt; lra. Qed.

(* Lemmas about Conjugates *)

Lemma Cconj_R : forall r : R, r^* = r.         Proof. intros; clra. Qed.
Lemma Cconj_0 : 0^* = 0.                  Proof. clra. Qed.
Lemma Cconj_opp : forall C, (- C)^* = - (C^*). Proof. reflexivity. Qed.
Lemma Cconj_rad2 : (/ √2)^* = / √2.       Proof. clra. Qed.
Lemma Cplus_div2 : /2 + /2 = 1.           Proof. clra. Qed.
Lemma Cconj_involutive : forall c, (c^*)^* = c. Proof. intros; clra. Qed.
Lemma Cconj_plus_distr : forall (x y : C), (x + y)^* = x^* + y^*. Proof. intros; clra. Qed.
Lemma Cconj_mult_distr : forall (x y : C), (x * y)^* = x^* * y^*. Proof. intros; clra. Qed.

Lemma Cmult_conj_real : forall (c : C), snd (c * c^*) = 0.
Proof.
  intros c.
  unfold Cconj.
  unfold Cmult.
  simpl.
  rewrite <- Ropp_mult_distr_r.
  rewrite Rmult_comm.
  rewrite Rplus_opp_l.
  reflexivity.
Qed.

Lemma square_rad2 : /√2 * /√2 = /2.
Proof.
  eapply c_proj_eq; simpl; try lra.
  autorewrite with R_db.
  rewrite Rmult_assoc.
  rewrite (Rmult_comm (/2) _).
  repeat rewrite <- Rmult_assoc.
  rewrite sqrt_def; lra.
Qed.

Lemma Cpow_nonzero : forall (r : R) (n : nat), (r <> 0 -> r ^ n <> C0)%C.
Proof.
  intros.
  rewrite RtoC_pow.
  apply C0_fst.
  apply pow_nonzero.
  lra.
Qed.

(* e^(iθ) *)
Definition Cexp (θ : R) : C := (cos θ, sin θ).

Lemma eulers_identity : Cexp PI = -1.
Proof. unfold Cexp. rewrite cos_PI, sin_PI. easy. Qed.

Lemma eulers_identity2 : Cexp (PI/2) = Ci.
Proof. unfold Cexp. rewrite cos_PI2, sin_PI2. easy. Qed.

(*
Definition Cexp' (θ : R) : C := cos θ + Ci * (sin θ).
Lemma Cexp_eq : forall θ, Cexp θ = Cexp' θ. Proof. intros. clra. Qed.
*)

(**************)
(* Automation *)
(**************)

Lemma Cminus_unfold : forall c1 c2, (c1 - c2 = c1 + -c2)%C. Proof. reflexivity. Qed.
Lemma Cdiv_unfold : forall c1 c2, (c1 / c2 = c1 */ c2)%C. Proof. reflexivity. Qed.

(* Intentionally very limited tactic. Could have it call Cpow_nonzero
   and similar lemmas if we wanted to make it stronger *)
Ltac nonzero := apply C0_fst; specialize Rlt_sqrt2_0; intros; simpl; Psatz.lra.

Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2
     square_rad2 Cplus_div2
     Cplus_0_l Cplus_0_r Cplus_opp_r Cplus_opp_l Copp_0  Copp_involutive
     Cmult_0_l Cmult_0_r Cmult_1_l Cmult_1_r : C_db.

Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db.
Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db.
Hint Rewrite Cinv_l Cinv_r using nonzero : C_db.
(* Previously in the other direction *)
Hint Rewrite Cinv_mult_distr using nonzero : C_db.

(* Light rewriting db *)
Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0
             Cconj_R Cmult_1_l Cmult_1_r : C_db_light.

(* Distributing db *)
Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l Copp_involutive : Cdist_db.

Ltac Csimpl :=
  repeat match goal with
  | _ => rewrite Cmult_0_l
  | _ => rewrite Cmult_0_r
  | _ => rewrite Cplus_0_l
  | _ => rewrite Cplus_0_r
  | _ => rewrite Cmult_1_l
  | _ => rewrite Cmult_1_r
  | _ => rewrite Cconj_R
  end.

(* We might want these back at some point
Ltac Rsimpl :=
  simpl;
  unfold Rminus;
  unfold Rdiv;
  repeat (
    try rewrite Ropp_0;
    try rewrite Ropp_involutive;
    try rewrite Rplus_0_l;
    try rewrite Rplus_0_r;
    try rewrite Rmult_0_l;
    try rewrite Rmult_0_r;
    try rewrite Rmult_1_l;
    try rewrite Rmult_1_r;
    try rewrite <- Ropp_mult_distr_l;
    try rewrite <- Ropp_mult_distr_r;
    try (rewrite Rinv_l; [|lra]);
    try (rewrite Rinv_r; [|lra]);
    try (rewrite sqrt_sqrt; [|lra])).

Ltac Rsolve := repeat (Rsimpl; try group_radicals); lra.

Ltac Csolve := eapply c_proj_eq; simpl; Rsolve.
*)

(* Seems like this could loop forever *)
Ltac group_radicals :=
  repeat (
  match goal with
    | [ |- context[(?r1 * √ ?r2)%R] ] => rewrite (Rmult_comm r1 (√r2))
    | [ |- context[(?r1 * (√ ?r2 * ?r3))%R] ] => rewrite <- (Rmult_assoc _ (√ r2) _)
    | [ |- context[((√?r * ?r1) + (√?r * ?r2))%R ] ] =>
        rewrite <- (Rmult_plus_distr_l r r1 r2)
  end).


text:
From CertiCoq.Plugin Require Import CertiCoq.
Require Import String.

Require Import sha256.

Definition text := "Hallo Welt."%string.
Definition test_sha := sha256.SHA_256' (sha256.str_to_bytes text).

From CertiCoq.Plugin Require Import CertiCoq.
CertiCoq Show IR -file "sha" test_sha.
CertiCoq Generate WASM -file "sha" test_sha.

author: womeier

repo: certicoqwasm-testing


text:
Require Export Ascii String.

Require Import QArith.
Require Export DTimeQ.

Require Export MinBFT.
Require Export RunSM.

Section MinBFTinstance.

  (* ================== MINBFT CONTEXT ================== *)

  Definition minbft_digest : Set := list nat.

  Definition minbft_digest_def : minbft_digest := [].

  Lemma minbft_digest_deq : Deq minbft_digest.
  Proof.
    introv; apply list_eq_dec.
    apply deq_nat.
  Defined.

  Inductive sending_key_stub : Set :=
  | minbft_sending_key_stub.

  Inductive receiving_key_stub : Set :=
  | minbft_receiving_key_stub.

  Definition minbft_sending_key   : Set := sending_key_stub.
  Definition minbft_receiving_key : Set := receiving_key_stub.

  (*Definition F : nat := 1.*)
  Definition nreps (F : nat) : nat := 2 * F + 1.

  Definition replica (F : nat) : Set := nat_n (nreps F).

  Lemma replica_deq (F : nat) : Deq (replica F).
  Proof.
    apply nat_n_deq.
  Defined.

  Definition reps2nat (F : nat) : replica F -> nat_n (nreps F) := fun n => n.

  Lemma bijective_reps2nat (F : nat) : bijective (reps2nat F).
  Proof.
    exists (fun n : nat_n (nreps F) => n); introv; unfold reps2nat; auto.
  Defined.

  Definition replica0 (F : nat) : replica F.
  Proof.
    exists 0.
    apply leb_correct.
    unfold nreps.
    omega.
  Defined.

  Definition replica1 : replica 1.
  Proof.
    exists 1.
    apply leb_correct.
    unfold nreps.
    omega.
  Defined.

  Definition replica2 : replica 1.
  Proof.
    exists 2.
    apply leb_correct.
    unfold nreps.
    omega.
  Defined.

  Definition nclients (C : nat) : nat := S C.

  Definition client (C : nat) : Set := nat_n (nclients C).

  Definition client0 (C : nat) : client C.
  Proof.
    exists 0.
    apply leb_correct.
    unfold nclients.
    omega.
  Defined.

  Lemma client_deq (C : nat) : Deq (client C).
  Proof.
    apply nat_n_deq.
  Defined.

  Definition clients2nat (C : nat) : client C -> nat_n (nclients C) := fun n => n.

  Lemma bijective_clients2nat (C : nat) : bijective (clients2nat C).
  Proof.
    exists (fun n : nat_n (nclients C) => n); introv; unfold clients2nat; auto.
  Defined.

  Inductive minbft_data_message :=
  | minbft_data_message_plus (n : nat)
  | minbft_data_message_minus (n : nat).

  Lemma minbft_data_message_deq : Deq minbft_data_message.
  Proof.
    introv; destruct x as [x|x], y as [y|y];
      destruct (deq_nat x y); prove_dec.
  Defined.

  Definition minbft_result := nat.

  Lemma minbft_result_deq : Deq minbft_result.
  Proof.
    introv; apply deq_nat.
  Defined.

  Definition minbft_sm_state := nat.

  Definition minbft_sm_initial_state : minbft_sm_state := 0.

  Definition minbft_sm_update
             (C : nat)
             (c : client C)
             (s : minbft_sm_state)
             (m : minbft_data_message) : minbft_result * minbft_sm_state :=
    match m with
    | minbft_data_message_plus  n => let x := s + n in (x,x)
    | minbft_data_message_minus n => let x := s - n in (x,x)
    end.

  Definition F := 1.
  Definition C := 0.

  Global Instance MinBFT_I_context : MinBFT_context :=
    Build_MinBFT_context
      minbft_digest
      minbft_digest_deq
      minbft_sending_key
      minbft_receiving_key
      F
      (replica F)
      (replica_deq F)
      (reps2nat F)
      (bijective_reps2nat F)
      (nclients C)
      (client C)
      (client_deq C)
      (clients2nat C)
      (bijective_clients2nat C)
      minbft_data_message
      minbft_data_message_deq
      minbft_result
      minbft_result_deq
      minbft_sm_state
      minbft_sm_initial_state
      (minbft_sm_update C).

  (* ================== SIGNATURE ================== *)
(*
  Inductive MinBFTtoken_stub : Set :=
  | minbft_token_stub.

  Definition minbft_token : Set := MinBFTtoken_stub.

  Lemma minbft_token_deq : Deq minbft_token.
  Proof.
    introv; destruct x, y; simpl; prove_dec.
  Defined.

*)

  Definition minbft_create_signature
             (m  : MinBFT_Bare_Msg)
             (ks : sending_keys) : list MinBFT_digest := [minbft_digest_def].

  Definition minbft_verify_signature
             (m : MinBFT_Bare_Msg)
             (n : name)
             (k : receiving_key)
             (a : MinBFT_digest) : bool := true.

  Global Instance MinBFT_I_auth : MinBFT_auth :=
    MkMinBFT_auth minbft_create_signature minbft_verify_signature.

  Definition minbft_lookup_replica_sending_key   (src : Rep)    : minbft_sending_key   := minbft_sending_key_stub.
  Definition minbft_lookup_replica_receiving_key (dst : Rep)    : minbft_receiving_key := minbft_receiving_key_stub.
  Definition minbft_lookup_client_sending_key    (c   : Client) : minbft_sending_key   := minbft_sending_key_stub.
  Definition minbft_lookup_client_receiving_key  (c   : Client) : minbft_receiving_key := minbft_receiving_key_stub.

  Definition initial_minbft_local_key_map_replicas (src : name) : local_key_map :=
    match src with
    | MinBFT_replica i =>
      MkLocalKeyMap
        (map (fun c => MkDSKey [MinBFT_client c] (minbft_lookup_client_sending_key c)) clients)
        (map (fun c => MkDRKey [MinBFT_client c] (minbft_lookup_client_receiving_key c)) clients)
    | MinBFT_client _ => MkLocalKeyMap [] []
    end.

  Global Instance MinBFT_I_keys : MinBFT_initial_keys :=
    MkMinBFT_initial_keys initial_minbft_local_key_map_replicas.

  (* ================== USIG HASH ================== *)

  Definition minbft_create_hash_usig
             (hd : HashData)
             (lk : local_key_map) : MinBFT_digest := [].

  Definition minbft_verify_hash_usig
             (hd : HashData)
             (d  : MinBFT_digest)
             (lk : local_key_map) : bool := true.

  Lemma minbft_verify_create_hash_usig :
    forall (hd : HashData) (keys : local_key_map),
      minbft_verify_hash_usig hd (minbft_create_hash_usig hd keys) keys = true.
  Proof.
    tcsp.
  Qed.

  Global Instance MinBFT_I_usig_hash : USIG_hash :=
    MkMinBFThash
      minbft_create_hash_usig
      minbft_verify_hash_usig
      minbft_verify_create_hash_usig.

  (* ================== TIME ================== *)

  Definition time_I_type : Set := unit.

  Definition time_I_get_time : unit -> time_I_type := fun _ => tt.

  Definition time_I_sub : time_I_type -> time_I_type -> time_I_type := fun _ _ => tt.

  Definition time_I_2string : time_I_type -> string := fun _ => "".

  Global Instance TIME_I : Time.
  Proof.
    exists time_I_type.
    { exact time_I_get_time. }
    { exact time_I_sub. }
    { exact time_I_2string. }
  Defined.

  (* ================== PRETTY PRINTING ================== *)

  Definition print_endline : string -> unit := fun _ => tt.
  Definition nat2string (n : nat) : string := "-".

  Definition CR : string := String (ascii_of_nat 13) "".

  (* Fix: to finish *)
  Definition tokens2string (toks : Tokens) : string := "-".

  (* Fix: to finish *)
  Definition minbft_digest2string (d : minbft_digest) : string := "-".

  (* Fix: to finish *)
  Definition minbft_result2string (r : minbft_result) : string := nat2string r.

  (* Fix: there's only one client anyway *)
  Definition client2string (c : client C) : string := "-".

  Definition timestamp2string (ts : Timestamp) : string :=
    match ts with
    | time_stamp n => nat2string n
    end.

  Definition view2string (v : View) : string :=
    match v with
    | view n => nat2string n
    end.

  Definition seq2string (s : SeqNum) : string :=
    match s with
    | seq_num n => nat2string n
    end.

  Fixpoint str_concat (l : list String.string) : String.string :=
    match l with
    | [] => ""
    | s :: ss => String.append s (str_concat ss)
    end.

  Definition minbft_data_message2string (opr : minbft_data_message) : string :=
    match opr with
    | minbft_data_message_plus  n => str_concat ["+", nat2string n]
    | minbft_data_message_minus n => str_concat ["-", nat2string n]
    end.

  Definition nat_n2string {m} (n : nat_n m) : string := nat2string (proj1_sig n).

  Definition replica2string (r : replica F) : string := nat_n2string r.

  Definition bare_request2string (br : Bare_Request) : string :=
    match br with
    | bare_request c ts m =>
      str_concat [client2string c,
                  ",",
                  timestamp2string ts,
                  ",",
                  minbft_data_message2string m]
    end.

  Definition request2string (r : Request) : string :=
    match r with
    | request br a => str_concat ["REQUEST(", bare_request2string br, ",", tokens2string a, ")"]
    end.

  Definition bare_prepare2string (bp : Bare_Prepare) : string :=
    match bp with
    | bare_prepare v m =>
      str_concat [view2string v,
                  ",",
                  request2string m]
    end.

  Definition pre_ui2string (pui : preUI) : string :=
    match pui with
    | Build_preUI id counter =>
      str_concat [replica2string id,
                  ",",
                  nat2string counter]
    end.

  Definition ui2string (ui : UI) : string :=
    match ui with
    | Build_UI pui d =>
      str_concat [pre_ui2string pui,
                  ",",
                  minbft_digest2string d]
    end.

  Definition bare_commit2string (bc : Bare_Commit) : string :=
    match bc with
    | bare_commit v m ui =>
      str_concat [view2string v,
                  ",",
                  request2string m,
                  ",",
                  ui2string ui]
    end.

  Definition prepare2string (p : Prepare) : string :=
    match p with
    | prepare bp a => str_concat ["PREPARE(", bare_prepare2string bp, ",", ui2string a, ")"]
    end.

  Definition commit2string (c : Commit) : string :=
    match c with
    | commit bc a => str_concat ["COMMIT(", bare_commit2string bc, ",", ui2string a, ")"]
    end.

  Definition accept2string (r : Accept) : string :=
    match r with
    | accept r c => str_concat ["ACCEPT(", request2string r, ",", nat2string c, ")"]
    end.

  Definition bare_reply2string (br : Bare_Reply) : string :=
    match br with
    | bare_reply req res i v => str_concat [request2string req, ",", nat2string res, ",", replica2string i]
    end.

  Definition reply2string (r : Reply) : string :=
    match r with
    | reply br a => str_concat ["REPLY(", bare_reply2string br, ",", tokens2string a, ")"]
    end.

  Definition msg2string (m : MinBFT_msg) : string :=
    match m with
    | MinBFT_request r => request2string r
    | MinBFT_reply r   => reply2string r
    | MinBFT_prepare p => prepare2string p
    | MinBFT_commit  c => commit2string  c
    | MinBFT_accept  a => accept2string  a
    | MinBFT_debug   s => s
    end.

  Definition name2string (n : name) : string :=
    match n with
    | MinBFT_replica r => replica2string r
    | MinBFT_client c => client2string c
    end.

  Fixpoint names2string (l : list name) : string :=
    match l with
    | [] => ""
    | [n] => name2string n
    | n :: ns => str_concat [name2string n, ",", names2string ns]
    end.

  Definition delay2string (delay : nat) : string := nat2string delay.

  Definition z2string (z : Z) : string := "".
  Definition pos2string (p : positive) : string := "".

  Definition q2string (q : Q) : string :=
    str_concat ["(" ,
                z2string (Qnum q),
                "/",
                pos2string (Qden q),
                ")"].

  Definition posdtime2string (p : PosDTime) : string :=
    q2string (pos_dt_t p).

  Definition DirectedMsg2string (dm : DirectedMsg) : string :=
    match dm with
    | MkDMsg msg dst delay =>
      str_concat [msg2string msg, ":", "[", names2string dst, "]", ":", posdtime2string delay]
    end.

  Fixpoint DirectedMsgs2string (l : DirectedMsgs) : string :=
    match l with
    | [] => ""
    | [dm] => DirectedMsg2string dm
    | dm :: dmsgs => str_concat [DirectedMsg2string dm, CR, DirectedMsgs2string dmsgs]
    end.

  Definition TimedDirectedMsg2string (m : TimedDirectedMsg) : string :=
    match m with
    | MkTimedDMsg dm time => str_concat [DirectedMsg2string dm, ":", time_I_2string time]
    end.

  Fixpoint TimedDirectedMsgs2string (l : TimedDirectedMsgs) : string :=
    match l with
    | [] => ""
    | [dm] => TimedDirectedMsg2string dm
    | dm :: dmsgs => str_concat [TimedDirectedMsg2string dm, CR, TimedDirectedMsgs2string dmsgs]
    end.

  Definition SimState2string (s : SimState) : string :=
    match s with
    | MkSimState fls sys step out_inflight in_inflight delivered =>
      str_concat
        [CR,
         "====== STEP ======",
         CR,
         nat2string step,
         CR,
         "====== IN FLIGHT (from outside the system) ======",
         CR,
         DirectedMsgs2string out_inflight,
         CR,
         "====== IN FLIGHT (from inside the system) ======",
         CR,
         DirectedMsgs2string in_inflight,
         CR,
         "====== DELIVERED ======",
         CR,
         TimedDirectedMsgs2string delivered,
         CR]
    end.

  (* ================== SYSTEM ================== *)

  (* FIX: do we need this one? *)
  Definition dummy_usig_initial_state : USIG_state :=
    Build_USIG
      replica1
      0
      (MkLocalKeyMap [] []).

  (* do we need this one? *)
  Definition dummy_log_initial_state : LOG_state := [].

  (* do we need this one? *)
  Definition dummy_initial_state : MAIN_state :=
    Build_State
      (MkLocalKeyMap [] [])
      initial_view
      MinBFT_sm_initial_state
      initial_latest_executed_counter
      initial_latest_executed_request
      initial_highest_received_counter_value
      None.

  Definition dummy_LocalSystem : MLocalSystem 0 1 :=
    MkLocalSystem
      (MP_haltedSM munit_comp_name 0 tt)
      [].

  Definition MinBFT_instance_sys : M_USystem MinBFTfunLevelSpace :=
    fun name =>
      match name with
      | MinBFT_replica n => MinBFTlocalSys n
      | _ =>  MkLocalSystem (MP_haltedSM munit_comp_name 0 tt) []
      end.

(* this def + def below same as send_request (see below); the only difference is the client is not parameter *)
   Definition mk_request_to (rep : Rep) (ts : nat) (m : MinBFT_data_message) : DirectedMsg :=
    let ts   := time_stamp ts in
    let breq := bare_request (client0 C)  ts m in
    let dst  := MinBFT_replica rep in (* the leader *)
    let toks := [ minbft_digest_def ] in (* we just send empty lists here to authenticate messages *)
    let req  := request breq toks in
    let msg  := MinBFT_request req in
    MkDMsg msg [dst] (nat2pdt 0).

  Definition mk_request (ts : nat) (opr : MinBFT_data_message) : DirectedMsg :=
     mk_request_to (MinBFTprimary initial_view) ts opr.

  (* n request starting with number start *)
  Fixpoint mk_requests_start (n start : nat) (opr : MinBFT_data_message) : DirectedMsgs :=
    match n with
    | 0 => []
    | S m => List.app (mk_requests_start m start opr) [mk_request (n + start) opr]
    end.

  Definition mk_requests (n : nat) (opr : MinBFT_data_message) : DirectedMsgs :=
    mk_requests_start n 0 opr.

  Record InitRequests :=
    MkInitRequests
      {
        num_requests     : nat;
        starting_seq_num : nat;
        req_operation    : MinBFT_data_message;
      }.

  (* same as  minbft_init_sim_state (see below) *)
  Definition MinBFT_init_msgs (msgs : DirectedMsgs) : SimState :=
    MkInitSimState MinBFT_instance_sys msgs.

  Definition MinBFT_init (init : InitRequests) : SimState :=
    MinBFT_init_msgs
      (mk_requests_start
         (num_requests init)
         (starting_seq_num init)
         (req_operation init)).

  Definition MinBFT_simul_list (init : InitRequests) (L : list nat) : SimState :=
    run_n_steps L (MinBFT_init init).

  Definition MinBFT_simul_list_msgs (msgs : DirectedMsgs) (L : list nat) : SimState :=
    run_n_steps L (MinBFT_init_msgs msgs).

  (* [switch] is the list of steps at which we want to switch to sending messages
   coming from the outside (from clients) instead of keeping on sending messages
   coming from the inside (from replicas). *)
  Definition MinBFT_simul_n
             (init     : InitRequests) (* This is to generate an initial list of requests *)
             (rounds   : Rounds)
             (switches : Switches) : SimState :=
    iterate_n_steps rounds switches (MinBFT_init init).

  Definition MinBFT_simul_n_msgs
             (msgs     : DirectedMsgs)
             (rounds   : Rounds)
             (switches : Switches) : SimState :=
    iterate_n_steps rounds switches (MinBFT_init_msgs msgs).

(*
  (* ================== STATE ================== *)

 (* same as mk_request_to
  Definition send_request
             (c  : Client)
             (ts : Timestamp)
             (m  : MinBFT_data_message) :=
    MkDMsg
      (MinBFT_request (request (bare_request c ts m) [minbft_digest_def]))
      [MinBFT_replica (MinBFTprimary (view 0))]
      ('0).
 *)

(* same as MinBFT_init_msgs
  Definition minbft_init_sim_state : SimState :=
    let c  := client0 C in
    let ts := time_stamp 0 in
    let m  := minbft_data_message_plus 17 in
    MkInitSimState
      MinBFTsys
      [send_request c ts m]. *)

(* similar to  MinBFT_simul_list_msgs (no parameters required here *)
  Definition minbft_sim_state1 : SimState :=
    run_n_steps [0,0] minbft_init_sim_state.

  Eval compute in (let p0  := replica0 F in
                   let km  := initial_minbft_local_key_map_replicas (MinBFT_replica p0) in
                   let c   := client0 C in
                   let ts  := time_stamp 0 in
                   let m   := minbft_data_message_plus 17 in
                   let r   := request (bare_request c ts m) [minbft_digest_def] in
                   let s   := initial_state p0 in
                   valid_request p0 km r s).

  Eval compute in (let v   := view 0 in
                   let p0  := replica0 F in
                   let p1  := replica1 in
                   let km  := initial_minbft_local_key_map_replicas (MinBFT_replica p1) in
                   let c   := client0 C in
                   let ts  := time_stamp 0 in
                   let m   := minbft_data_message_plus 17 in
                   let r   := request (bare_request c ts m) [minbft_digest_def] in
                   let ui  := snd (create_UI v r (USIG_initial p0)) in
                   let p   := prepare (bare_prepare v r) ui in
                   let s   := initial_state p1 in
                   valid_prepare p1 km v p s).
 *)

End MinBFTinstance.

(* ================== EXTRACTION ================== *)

Extraction Language Ocaml.

(* printing stuff *)
Extract Inlined Constant print_endline => "Prelude.print_coq_endline".
Extract Inlined Constant nat2string    => "Prelude.char_list_of_int".
Extract Inlined Constant CR            => "['\n']".

(* numbers *)
Extract Inlined Constant Nat.modulo    => "(mod)".

(* lists *)
Extract Inlined Constant forallb => "List.for_all".
Extract Inlined Constant existsb => "List.exists".
Extract Inlined Constant length  => "List.length".
Extract Inlined Constant app     => "List.append".
Extract Inlined Constant map     => "List.map".
Extract Inlined Constant filter  => "List.filter".

(* timing stuff *)
Extract Inlined Constant time_I_type     => "float".
Extract Inlined Constant time_I_get_time => "Prelude.Time.get_time".
Extract Inlined Constant time_I_sub      => "Prelude.Time.sub_time".
Extract Inlined Constant time_I_2string  => "Prelude.Time.time2string".

(* == crypto stuff ==
(* === COMMENT OUT THIS PART IF YOU DON'T WANT TO USE KEYS ===*)

Extract Inlined Constant minbft_sending_key   => "Nocrypto.Rsa.priv".
Extract Inlined Constant minbft_receiving_key => "Nocrypto.Rsa.pub".
Extract Inlined Constant minbft_lookup_replica_sending_key   => "RsaKeyFun.lookup_replica_sending_key".
Extract Inlined Constant minbft_lookup_replica_receiving_key => "RsaKeyFun.lookup_replica_receiving_key".
Extract Inlined Constant minbft_lookup_client_receiving_key  => "RsaKeyFun.lookup_client_receiving_key".
Extract Inlined Constant minbft_lookup_client_sending_key  => "RsaKeyFun.lookup_client_sending_key".

Extract Inlined Constant minbft_create_signature => "RsaKeyFun.sign_list".
Extract Inlined Constant minbft_verify_signature => "RsaKeyFun.verify_one".

Extract Inlined Constant minbft_digest => "Cstruct.t".
Extract Inlined Constant minbft_digest_deq => "(=)".
(* === --- === *)

(* == hashing stuff == *)
Extract Inlined Constant minbft_create_hash_usig => "Obj.magic (Hash.create_hash_objects)".
Extract Inlined Constant minbft_verify_hash_usig => "Obj.magic (Hash.verify_hash_objects)".
(* === --- === *)

(* Cstruct.t is the most logical choice *)
Extract Inlined Constant minbft_digest_def => "Cstruct.empty".
*)

Require Export ExtrOcamlBasic.
Require Export ExtrOcamlNatInt.
Require Export ExtrOcamlString.

Definition local_system:=
  @MinBFTlocalSys.

(*
Extraction "MinbftReplica.ml" (* minbft_state2string *) run_sm SimState2string dummy_LocalSystem local_system.
*)

Definition MinBFT_simul : SimState :=
  let num_requests     := 2  in
  let starting_seq_num := 0  in
  let req_operation    := minbft_data_message_plus 17 in
  let rounds   := [MkRound 0(*pos*) 22(*num steps*)(*, MkRound 3 25, MkRound 0 36*)] in
  let switches := [(*MkSwitch 1 0*)] in
  MinBFT_simul_n
    (MkInitRequests num_requests starting_seq_num req_operation)
    rounds
    switches.

Definition MinBFT_simul_pp : unit :=
  print_endline (SimState2string MinBFT_simul).

Extraction "minbft_simul.ml" MinBFT_simul_pp.

author: veri-fit

repo: Asphalion

save_path: github-repos/coq/veri-fit-Asphalion