experiment00.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) = intersection (set_image f X) (range f).
Proof.
  unfold range, restriction, intersection, set_image. apply SetExtensionality. split; intros.
  + split.
    - destruct H. exists x0. destruct (dec x0).
      * split; auto. destruct (f x0); congruence.
      * destruct (f x0); congruence.
    - destruct H. exists x0. destruct (dec x0).
      * destruct (f x0); congruence.
      * destruct (f x0); congruence.
  + repeat destruct H. destruct H0. exists x0. rewrite H1. destruct (dec x0).
    - auto.
    - tauto.
Qed.

(* Experimenting *)

Inductive formula_of_one_variable :=
| variable: formula_of_one_variable
| number: R → formula_of_one_variable
| Rplus': formula_of_one_variable → formula_of_one_variable → formula_of_one_variable
| Rminus': formula_of_one_variable → formula_of_one_variable → formula_of_one_variable
| Rmult': formula_of_one_variable → formula_of_one_variable → formula_of_one_variable
| Rdiv': formula_of_one_variable → formula_of_one_variable → formula_of_one_variable.

Declare Scope R'.
Notation "[x]" := variable: R'.
Notation "[ a ]" := (number a): 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'.

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: formula_of_one_variable → R ~> R.
Proof.
  intros. induction H as [| |? f1 ? f2|? f1 ? f2|? f1 ? f2|? f1 ? f2].
  + exact (λ x, Some x).
  + exact (λ x, Some r).
  + exact (fanout f1 f2 ∘ Rplus'_function).
  + exact (fanout f1 f2 ∘ Rminus'_function).
  + exact (fanout f1 f2 ∘ Rmult'_function).
  + exact (fanout f1 f2 ∘ Rdiv'_function).
Defined.

Definition formula_eq (f1 f2: formula_of_one_variable) :=
  let fun1 := transform f1 in
  let fun2 := transform f2 in
  ∀ x, domain fun1 x → domain fun2 x → fun1 x = fun2 x.
(* Not an equivalence, because it isn't transitive. *)

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

Delimit Scope R' with R'.
Open Scope R'.

Definition test_formula_1: formula_of_one_variable := ([x] + [1]) * ([x] + [1]).
Print test_formula_1.
Eval compute in transform test_formula_1.

Definition test_formula_2: formula_of_one_variable := ([x] + [1]) / ([x] - [2]).
Print test_formula_2.
Eval compute in transform test_formula_2.

Definition test_formula_3: formula_of_one_variable := [x] + [x] + [x] + [x].
Print test_formula_3.
Eval compute in transform test_formula_3.

Theorem test: [x] / [x] == [1].
Proof.
  unfold formula_eq. intros. simpl in *.
  rewrite domain_of_composition in H. rewrite domain_of_fanout in H.
  assert (domain (λ x, Some x) = @full_set R).
  { unfold domain, full_set. apply SetExtensionality. split; intro; auto. eauto. }
  assert (domain Rdiv'_function = λ p, match p with (x, y) => y ≠ 0 end).
  { unfold domain, Rdiv'_function. apply SetExtensionality. split; intros.
    + destruct x0, H2 as [y H2]. destruct (Req_EM_T r0 0); congruence.
    + destruct x0. destruct (Req_EM_T r0 0); try congruence. eauto. }
  rewrite H1, H2 in H. unfold intersection, full_set, set_preimage, fanout in H.
  destruct H. destruct H3 as [[a b] [H3 H4]]. inversion H4. subst.
  unfold fanout, Rdiv'_function, compose. destruct (Req_EM_T b 0).
  + congruence.
  + f_equal. field. auto.
Qed.

Search "_ / _". (* finds theorem test (among many other things) *)
Search (?x / ?x). (* finds it, too *)
Search ([x] / [x]) % R'. (* finds it *)