experiment01.v

Require Import Reals Lra Utf8.
Open Scope R.

Axiom FunctionalExtensionality: ∀ {A B} (f g: A → B), (∀ x, f x = g x) ↔ f = g.
Axiom PropositionalExtensionality: ∀ (P Q: Prop), (P ↔ Q) ↔ P = Q.

Definition set A := A → Prop.
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.

Lemma SetExtensionality: ∀ {A} (X Y: set A), (∀ x, X x ↔ Y x) ↔ X = Y.
Proof.
  intros. split; intros.
  + apply FunctionalExtensionality. intro. apply PropositionalExtensionality. auto.
  + subst. tauto.
Qed.

Definition function A B := A → option B.
Notation "a ~> b" := (function a b) (at level 90, right associativity).
Definition domain {A B} (f: A ~> B): set A := λ x, ∃ y, f x = Some y.
Definition range {A B} (f: A ~> B): set B := λ y, ∃ x, f x = Some y.
Definition preimage {A B} (f: A ~> B) (y: B): set A := λ x, f x = Some y.
Definition set_image {A B} (f: A ~> B) (X: set A): set B :=
  λ y, (∃ x, X x ∧ f x = Some y).
Definition set_preimage {A B} (f: A ~> B) (Y: set B): set A :=
  λ x, ∃ y, Y y ∧ f x = Some y.

Definition arr {A B} (f: A → B): A ~> B := λ x, Some (f x).

Definition compose {A B C} (f: A ~> B) (g: B ~> C): A ~> C :=
  λ x, match f x with
       | Some y => g y
       | None => None
       end.
Notation "f ∘ g" := (compose f g) (at level 40, left associativity).

Definition first {A B C} (f: A ~> B): A * C ~> B * C :=
  λ p, match p with (x, y) => match f x with
                              | Some x' => Some (x', y)
                              | None => None
                              end end.

Definition second {A B C} (f: B ~> C): A * B ~> A * C :=
  λ p, match p with (x, y) => match f y with
                              | Some y' => Some (x, y')
                              | None => None
                              end end.

Definition split_and_combine {A B C D} (f: A ~> B) (g: C ~> D): A * C ~> B * D :=
  λ p, match p with (x, y) => match f x, g y with
                              | Some x', Some y' => Some (x', y')
                              | _, _ => None
                              end end.

Definition fanout {A B C} (f: A ~> B) (g: A ~> C): A ~> B * C :=
  λ x, match f x, g x with
       | Some x', Some y' => Some (x', y')
       | _, _ => None
       end.

Definition restriction {A B} (f: A ~> B) {X: set A} (dec: ∀ x, {X x} + {¬ X x}) :=
  λ x, match f x with
       | Some x' => if dec x then Some x' else None
       | None => None
       end.

(* Theorems about domains *)

Theorem domain_of_arr {A B} (f: A → B): domain (arr f) = @full_set A.
Proof.
  unfold arr, domain, full_set. 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.
  apply SetExtensionality. split; intros.
  + destruct H as [z H], (f x); split; try congruence; eauto.
  + destruct H as [[y H] [y' [[z H0] H1]]]. rewrite 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. apply SetExtensionality. split; intros.
  + destruct x, H as [[y z] H]. simpl. destruct (f a); try congruence; eauto.
  + destruct x, H as [y H]. simpl in *. rewrite H. eauto.
Qed.

Theorem domain_of_second {A B C} (f: B ~> C):
  domain (@second A _ _ f) = λ p, domain f (snd p).
Proof.
  unfold second, domain. apply SetExtensionality. split; intros.
  + destruct x, H as [[x z] H]. simpl. destruct (f b); try congruence; eauto.
  + destruct x, H as [y H]. simpl in *. rewrite H. eauto.
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. apply SetExtensionality. split; intros.
  + destruct x, H as [[y w] H], (f a), (g c); try congruence; split; eauto.
  + destruct x, H as [[y H] [w H0]]. rewrite H, H0. eauto.
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. apply SetExtensionality. split; intros.
  + destruct H as [[y z] H], (f x), (g x); try congruence; split; eauto.
  + destruct H as [[y H] [z H0]]. rewrite H, H0. eauto.
Qed.

Theorem domain_of_restriction {A B} (f: A ~> B) {X} (dec: ∀ x, {X x} + {¬ X x}):
  domain (restriction f dec) = intersection X (domain f).
Proof.
  unfold domain, restriction, intersection. apply SetExtensionality. split; intros.
  + destruct H as [y H], (f x), (dec x); try congruence; eauto.
  + destruct H as [H [y H0]]. rewrite H0. destruct (dec x).
    - eauto.
    - tauto.
Qed.

(* Theorems about range *)

Theorem range_of_arr {A B} (f: A → B): range (arr f) = λ y, ∃ x, f x = y.
Proof.
  unfold arr, range. apply SetExtensionality. split; intros.
  + destruct H. inversion H. eauto.
  + destruct H. subst. eauto.
Qed.

Theorem range_of_composition {A B C} (f: A ~> B) (g: B ~> C):
  range (f ∘ g) = set_image g (intersection (range f) (domain g)).
Proof.
  unfold range, domain, compose, set_image, intersection, range.
  apply SetExtensionality. split; intros.
  + destruct H. remember (f x0) as W. destruct W.
    - exists b. split; auto. split; eauto.
    - congruence.
  + destruct H as [b [[[x0 H] [z H0]] H1]]. exists x0. rewrite H. auto.
Qed.

Theorem range_of_first {A B C} (f: A ~> B):
  range (@first _ _ C f) = λ p, match p with (x, y) => range f x end.
Proof.
  unfold first, range. apply SetExtensionality. split; intros.
  + destruct x, H as [[y z] H]. exists y. destruct (f y); congruence.
  + destruct x, H as [x H]. exists (x, c). rewrite H. auto.
Qed.

Theorem range_of_second {A B C} (f: B ~> C):
  range (@second A _ _ f) = λ p, match p with (x, y) => range f y end.
Proof.
  unfold second, range. apply SetExtensionality. split; intros.
  + destruct x, H as [[x z] H]. exists z. destruct (f z); congruence.
  + destruct x, H as [y H]. exists (a, y). rewrite H. auto.
Qed.

Theorem range_of_split_and_combine {A B C D} (f: A ~> B) (g: C ~> D):
  range (split_and_combine f g) = λ p, match p with (x, y) => range f x ∧ range g y end.
Proof.
  unfold range, split_and_combine. apply SetExtensionality. split; intros.
  + destruct x, H as [[y w] H]. split.
    - exists y. destruct (f y); try congruence. destruct (g w); congruence.
    - exists w. destruct (f y); try congruence. destruct (g w); congruence.
  + destruct x, H as [[x0 H] [z H0]]. exists (x0, z). rewrite H, H0. auto.
Qed.

Theorem fanout_aux {A B C} (f: A ~> B) (g: A ~> C):
  fanout f g = (λ x, Some (x, x)) ∘ first f ∘ second g.
Proof.
  apply FunctionalExtensionality. intros.
  unfold fanout, first, second, compose. destruct (f x); 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) => ∃ i, f i = Some x ∧ g i = Some y end.
Proof.
  unfold range. unfold fanout. apply SetExtensionality. split; intro.
  + destruct x, H. remember (f x) as F. remember (g x) as G.
    destruct F, G.
    - inversion H. subst. eauto.
    - congruence.
    - congruence.
    - congruence.
  + destruct x, H as [i [H H0]]. exists i. rewrite H, H0. auto.
Qed.

Theorem range_of_restriction {A B} (f: A ~> B) {X} (dec: ∀ x, {X x} + {¬ X x}):
  range (restriction f dec) = set_image f (intersection X (domain f)).
Proof.
  unfold range, restriction, intersection, domain, set_image. apply SetExtensionality. split; intros.
  + destruct H. exists x0. destruct (f x0).
    - destruct (dec x0).
      * split; auto. split; auto. eauto.
      * congruence.
    - congruence.
  + destruct H. destruct H. exists x0. rewrite H0. destruct H.
    destruct (dec x0); tauto.
Qed.

(* Experimenting *)

Inductive formula (n: nat) :=
| var: nat → formula n
| num: R → formula n
| Rplus': formula n → formula n → formula n
| Rminus': formula n → formula n → formula n
| Rmult': formula n → formula n → formula n
| Rdiv': formula n → formula n → formula n.

Declare Scope R'.
Delimit Scope R' with R'.
Notation "x + y" := (Rplus' _ x y) (at level 50, left associativity): R'.
Notation "x - y" := (Rminus' _ x y) (at level 50, left associativity): R'.
Notation "x * y" := (Rmult' _ x y) (at level 40, left associativity): R'.
Notation "x / y" := (Rdiv' _ x y) (at level 40, left associativity): R'.

Fixpoint tuple (n: nat) :=
  match n with
  | O => R
  | S m => prod (tuple m) R
  end.

Definition tuple_head {n: nat} (t: tuple n): R.
Proof.
  induction n.
  + exact t.
  + destruct t. exact (IHn t).
Defined.

Definition tuple_tail {n: nat} (t: tuple (S n)): tuple n.
Proof.
  induction n.
  + destruct t. exact r.
  + destruct t. simpl. exact (pair (IHn t) r).
Defined.

Fixpoint nth_of_tuple (n i: nat) : forall (t: tuple n), option R :=
  match n, i with
  | _, O => fun t => Some (tuple_head t)
  | O, _ => fun t => None
  | S n', S i' => fun t => nth_of_tuple n' i' (tuple_tail t)
  end.


Definition Rplus'_function := λ p, match p with (x, y) => Some (x + y) end.
Definition Rminus'_function := λ p, match p with (x, y) => Some (x - y) end.
Definition Rmult'_function := λ p, match p with (x, y) => Some (x * y) end.
Definition Rdiv'_function := λ p, match p with (x, y) => if Req_EM_T y 0 then None else Some (x / y) end.

Definition transform {n} (f: formula n): tuple n ~> R.
Proof.
  induction f.
  + exact (nth_of_tuple n n0).
  + exact (λ (x: tuple n), Some r).
  + exact (fanout IHf1 IHf2 ∘ Rplus'_function).
  + exact (fanout IHf1 IHf2 ∘ Rminus'_function).
  + exact (fanout IHf1 IHf2 ∘ Rmult'_function).
  + exact (fanout IHf1 IHf2 ∘ Rdiv'_function).
Defined.

Definition formula_eq {n} (f1 f2: formula n) :=
  let fun1 := transform f1 in
  let fun2 := transform f2 in
  ∀ x, domain fun1 x → domain fun2 x → fun1 x = fun2 x.

Infix "==" := formula_eq (at level 70): R'.

Open Scope R'.

Definition test_formula_1: formula 2 := (var _ 1 + num _ 1) * (var _ 1 + num _ 1).
Print test_formula_1.
Eval compute in transform test_formula_1.

Theorem test: (var 1 0 + var _ 1) * (var _ 0 - var _ 1) / (var _ 0 + var _ 1) ==
              var _ 0 - var _ 1.
Proof.
  unfold formula_eq. intros. simpl in *.
  destruct x as [x y]. compute in *.
  destruct H, H0. destruct (Req_EM_T (x + y) R0).
  + congruence.
  + f_equal. field. auto.
Qed.

Search "_ / _". (* finds theorem test (among many other things) *)
Search (?x / ?y). (* finds it, too *)