testing.v

Require Import Reals Lra Equivalence Utf8.
Open Scope R.

Reserved Infix "~>" (at level 90, right associativity).
Reserved Infix "∘" (at level 40, left associativity).

Definition set A := A → Prop.
Axiom SetExtensionality: ∀ {A} (X Y: set A), (∀ a, X a ↔ Y a) ↔ X = Y.
Definition empty_set A: set A := λ x, False.
Definition full_set A: set A := λ x, True.
Definition union {A} (X Y: set A): set A := λ a, X a ∨ Y a.
Definition intersection {A} (X Y: set A): set A := λ a, X a ∧ Y a.
Definition difference {A} (X Y: set A): set A := λ a, X a ∧ ¬ Y a.

Structure function A B := {
  graph: set (A * B);
  function_property: ∀ x y1 y2, graph (x, y1) → graph (x, y2) → y1 = y2
}.
Arguments graph: default implicits.
Arguments function_property: default implicits.

Notation "a ~> b" := (function a b).

Definition domain {A B} (f: A ~> B): set A := λ x, ∃ y, graph f (x, y).
Definition range {A B} (f: A ~> B): set B := λ y, ∃ x, graph f (x, y).
Definition preimage {A B} (f: A ~> B) (y: B): set A := λ x, graph f (x, y).
Definition set_image {A B} (f: A ~> B) (X: set A) (*(H: subset X (domain f))*): set B :=
  λ y, (∃ x, X x ∧ graph f (x, y)).
Definition set_preimage {A B} (f: A ~> B) (Y: set B) (*(H: subset Y (full_set B))*): set A :=
  λ x, ∃ y, Y y ∧ graph f (x, y).

Definition function_equiv {A B} (f g: A ~> B) := ∀ x, graph f x ↔ graph g x.

Instance function_equiv_proof {A B} (f g: A ~> B): Equivalence (@function_equiv A B).
Proof.
  split.
  + unfold Reflexive. unfold function_equiv. tauto.
  + unfold Symmetric. unfold function_equiv. intros. rewrite H. auto. tauto.
  + unfold Transitive. unfold function_equiv. intros. rewrite H, H0. tauto.
Qed.

Definition arr {A B} (f: A → B): A ~> B.
Proof.
  exists (λ p, match p with (x, y) => y = f x end).
  congruence.
Defined.

Definition compose {A B C} (f: A ~> B) (g: B ~> C): A ~> C.
Proof.
  exists (λ p, match p with (x, z) => ∃ y, graph f (x, y) ∧ graph g (y, z) end).
  intros. destruct H as [t1 [H1 H2]], H0 as [t2 [H3 H4]].
  assert (t1 = t2). { eapply f; eauto. }
  subst. eapply g; eauto.
Defined.
Notation "f ∘ g" := (compose f g).

Definition first {A B C} (f: A ~> B): A * C ~> B * C.
Proof.
  exists (λ p, match p with ((x, z1), (y, z2)) => graph f (x, y) ∧ (z1 = z2) end).
  intros. destruct x, y1, y2. destruct H, H0. subst.
  pose proof (function_property f _ _ _ H H0). subst. auto.
Defined.

Definition second {A B C} (f: B ~> C): A * B ~> A * C.
Proof.
  exists (λ p, match p with ((x1, y), (x2, z)) => graph f (y, z) ∧ (x1 = x2) end).
  intros. destruct x, y1, y2. destruct H, H0. subst.
  pose proof (function_property f _ _ _ H H0). subst. auto.
Defined.

Definition split_and_combine {A B C D} (f: A ~> B) (g: C ~> D): A * C ~> B * D.
Proof.
  exists (λ p, match p with ((x1, x2), (y1, y2)) => graph f (x1, y1) ∧ graph g (x2, y2) end).
  intros. destruct x, y1, y2. destruct H, H0.
  pose proof (function_property f _ _ _ H H0). pose proof (function_property g _ _ _ H1 H2).
  subst. auto.
Defined.

Definition fanout {A B C} (f: A ~> B) (g: A ~> C): A ~> B * C.
Proof.
  exists (λ p, match p with (x, (y1, y2)) => graph f (x, y1) ∧ graph g (x, y2) end).
  intros. destruct y1, y2. destruct H, H0.
  pose proof (function_property f _ _ _ H H0). pose proof (function_property g _ _ _ H1 H2).
  subst. auto.
Defined.

(* Theorems about domains *)

Definition set_eq {A} (X Y: set A): Prop := ∀ x, X x ↔ Y x.

Theorem domain_of_arr {A B} (f: A → B): domain (arr f) = @full_set A.
Proof.
  unfold arr, domain, full_set. simpl. apply SetExtensionality. split; intros.
  + auto.
  + eauto.
Qed.

Theorem domain_of_composition {A B C} (f: A ~> B) (g: B ~> C):
  domain (f ∘ g) = intersection (domain f) (set_preimage f (domain g)).
Proof.
  unfold domain, compose, set_preimage, intersection, range.
  simpl. apply SetExtensionality. split; intros.
  + destruct H as [z [y [H H0]]]. split.
    - eauto.
    - eauto.
  + destruct H as [[y H] [y0 [[z H0] H1]]]. eauto.
Qed.

Theorem domain_of_first {A B C} (f: A ~> B):
  domain (@first _ _ C f) = λ p, domain f (fst p).
Proof.
  unfold first, domain. simpl. apply SetExtensionality. split; intros.
  + destruct a. simpl. destruct H as [[y z] [H0 H1]]. subst. eauto.
  + destruct a. simpl in *. destruct H as [y H]. exists (y, c). auto.
Qed.

Theorem domain_of_second {A B C} (f: B ~> C):
  domain (@second A _ _ f) = λ p, domain f (snd p).
Proof.
  unfold second, domain. simpl. apply SetExtensionality. split; intros.
  + destruct a. simpl. destruct H as [y H]. destruct y. destruct H. eauto.
  + destruct a, H as [y H]. simpl in *. exists (a, y). auto.
Qed.

Theorem domain_of_split_and_combine {A B C D} (f: A ~> B) (g: C ~> D):
  domain (split_and_combine f g) = λ p, match p with (x, y) => domain f x ∧ domain g y end.
Proof.
  unfold domain, split_and_combine. simpl. apply SetExtensionality. split; intros.
  + destruct a. destruct H as [[y w] [H H0]]. split; eauto.
  + destruct a. destruct H as [[y H] [w H0]]. exists (y, w). auto.
Qed.

Theorem domain_of_fanout {A B C} (f: A ~> B) (g: A ~> C):
  domain (fanout f g) = intersection (domain f) (domain g).
Proof.
  unfold domain, fanout, intersection. simpl. apply SetExtensionality. split; intros.
  + destruct H as [[y z] [H H0]]. eauto.
  + destruct H as [[y H] [z H0]]. exists (y, z). auto.
Qed.

Theorem range_of_fanout {A B C} (f: A ~> B) (g: A ~> C):
  range (fanout f g) = λ p, match p with (x, y) => range f x ∧ range g y end.
Proof.
  unfold range, fanout. simpl. apply SetExtensionality. split; intros.
  + destruct a. destruct H as [x [H H0]]. eauto.
  + destruct a. destruct H as [[x H] [x0 H0]].
Abort.


(* Experimenting *)

Definition Rplus': R * R ~> R := arr (λ p, match p with (x, y) => x + y end).

Definition test1: R ~> R.
Proof.
  exists (λ p, match p with (x, y) => x < 4 ∧ x = y end).
  intros. abstract lra.
Defined.

Definition test2: R ~> R.
Proof.
  exists (λ p, match p with (x, y) => x > - 4 ∧ x = y end).
  intros. abstract lra.
Defined.

Definition combination: R ~> R := (fanout test1 test2) ∘ Rplus'.

Definition domain_of_combination: domain combination = λ x, -4 < x < 4.
Proof.
  assert (domain test1 = λ x, x < 4).
  { unfold domain, test1. simpl. apply SetExtensionality. split; intros.
    + destruct H. tauto.
    + eauto. }
  assert (domain test2 = λ x, x > -4).
  { unfold domain, test2. simpl. apply SetExtensionality. split; intros.
    + destruct H0. tauto.
    + eauto. }
  unfold combination. rewrite domain_of_composition.
  unfold Rplus'. rewrite domain_of_arr. rewrite domain_of_fanout.
  assert (∀ A B (f: A ~> B), set_preimage f (@full_set _) = domain f).
  { intros. unfold full_set, set_preimage, domain. apply SetExtensionality. split; intros.
    + destruct H1 as [y [H1 H2]]. eauto.
    + destruct H1 as [y H1]. eauto. }
  rewrite H1. rewrite domain_of_fanout. rewrite H, H0.
  unfold intersection. apply SetExtensionality. split; intros.
  + tauto.
  + tauto.
Qed.