Cvx.agda

module R where

open import Agda.Builtin.FromNat
open import Data.Unit using (tt)
open import Data.Rational as ℚ
open import Data.Rational.Properties
open import Data.Rational.Literals as ℚ
open import Data.Nat as ℕ using (ℕ)
import Data.Nat.Properties as ℕ
import Data.Integer as ℤ
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Function
open import Algebra.Definitions (_≡_ {A = ℚ})

infixr 1 _by⟨_⟩_
infixr 1 _by_

_by⟨_⟩_ : (A : Set) {B : Set} → (B → A) → B → A
A by⟨ f ⟩ x = f x

_by_ : (A : Set) → A → A
A by x = x

_Reflects_⟵_ : {A B : Set} → (A → B) → Rel A _ → Rel B _ → Set
f Reflects _~_ ⟵ _~~_ = ∀ {x y} → f x ~~ f y → x ~ y

module _ (a b c : ℕ) (a≤b : a ℕ.≤ b) (b<c : b ℕ.< c) where

  ofℕ : ℕ → ℚ
  ofℕ n = fromNat {{ℚ.number}} n {{tt}}

  x = ofℕ a
  y = ofℕ b
  z = ofℕ c

  fromℤ-< : fromℤ Preserves ℤ._<_ ⟶ _<_
  fromℤ-< z≤ = *<* ?

  x<z : x < z
  x<z = fromℤ-< (ℤ.+<+ (ℕ.<-transʳ a≤b b<c))

  minus-unfold : ∀ p q → p - q ≡ p + - q
  minus-unfold p@record{} q@record{} = refl

  neg-minus : ∀ p q → - (p - q) ≡ q - p
  neg-minus = ?

  +-minus-+ : ∀ p q → p - q + q ≡ p
  +-minus-+ p q = ?

  +-+-minus : ∀ p q → p + q + - q ≡ p
  +-+-minus p q = ?

  +-Reflects-<ʳ : (p : ℚ) → (_+ p) Reflects _<_ ⟵ _<_
  +-Reflects-<ʳ p {x} {y} xp< =
    x < y
    by⟨ subst id (cong₂ _<_ (+-+-minus x p) (+-+-minus y p)) ⟩
    x + p + - p < y + p + - p
    by⟨ +-monoˡ-< (- p) ⟩
    x + p < y + p
    by xp<

  open ≡-Reasoning

  instance
    NonZero-a-c : NonZero (z - x)
    NonZero-a-c = >-nonZero {p = z - x} (
      0ℚ < z - x
      by⟨ +-Reflects-<ʳ x ⟩
      0ℚ + x < z - x + x
      by⟨ subst id (sym (cong₂ _<_
        (+-identityˡ x)
        (+-minus-+ z x))) ⟩
      x < z
      by x<z)

  o : ℚ
  o = (z - y) ÷ (z - x)

  *-distribˡ-minus : _*_ DistributesOverˡ _-_
  *-distribˡ-minus x y z = ?

  ÷-*-invʳ : ∀ p q → .{{_ : NonZero q}} → (p ÷ q) * q ≡ p
  ÷-*-invʳ = ?

  u : o * x + (1ℚ - o) * z ≡ y
  u = o * x + (1ℚ - o) * z
      ≡⟨ cong (λ φ → o * x + φ * z) (minus-unfold 1ℚ o) ⟩
      o * x + (1ℚ + - o) * z
      ≡⟨ cong (o * x +_) (trans (*-distribʳ-+ z 1ℚ (- o)) (+-comm (1ℚ * z) ((- o) * z))) ⟩
      o * x + ((- o) * z + 1ℚ * z)
      ≡⟨ cong (λ φ → o * x + ((- o) * z + φ)) (*-identityˡ z) ⟩
      o * x + ((- o) * z + z)
      ≡⟨ sym (+-assoc (o * x) (- o * z) z) ⟩
      o * x + (- o) * z + z
      ≡⟨ cong (λ φ → o * x + φ + z) (sym (neg-distribˡ-* o z)) ⟩
      o * x + - (o * z) + z
      ≡⟨ cong (_+ z) (sym (minus-unfold (o * x) (o * z))) ⟩
      o * x - (o * z) + z
      ≡⟨ cong (_+ z) (sym (neg-minus (o * z) (o * x))) ⟩
      - (o * z - o * x) + z
      ≡⟨ cong (λ φ → - φ + z) (sym (*-distribˡ-minus o z x)) ⟩
      - (o * (z - x)) + z
      ≡⟨ cong (λ φ → - φ + z) (÷-*-invʳ (z - y) (z - x)) ⟩
      - (z - y) + z
      ≡⟨ ? ⟩
      y ∎