{-# OPTIONS --cubical-compatible --safe #-}
module Data.Nat.Binary.Subtraction where
open import Algebra.Core using (Op₂)
open import Algebra.Bundles using (Magma)
open import Algebra.Consequences.Propositional using (comm∧distrˡ⇒distrʳ)
open import Algebra.Morphism.Consequences using (homomorphic₂-inv)
open import Data.Bool.Base using (true; false; if_then_else_)
open import Data.Nat as ℕ using (ℕ)
open import Data.Nat.Binary.Base using (ℕᵇ; 0ᵇ; 2[1+_]; 1+[2_]; double;
pred; toℕ; fromℕ; even<odd; odd<even; _≥_; _>_; _≤_; _<_; _+_; zero; suc; 1ᵇ;
_*_)
open import Data.Nat.Binary.Properties
import Data.Nat.Properties as ℕ
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Vec.Base using ([]; _∷_)
open import Function.Base using (_∘_; _$_)
open import Level using (0ℓ)
open import Relation.Binary
using (Tri; tri<; tri≈; tri>; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality.Algebra using (magma)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; cong; cong₂; sym; trans; subst; _≢_)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)
open import Relation.Nullary using (Dec; yes; no; does)
open import Relation.Nullary.Negation using (contradiction)
open import Algebra.Definitions {A = ℕᵇ} _≡_
open import Algebra.Properties.CommutativeSemigroup +-commutativeSemigroup
using (xy∙z≈y∙xz; x∙yz≈y∙xz)
open import Algebra.Solver.CommutativeMonoid +-0-commutativeMonoid
private
variable
x y : ℕᵇ
infixl 6 _∸_
_∸_ : Op₂ ℕᵇ
zero ∸ _ = 0ᵇ
x ∸ zero = x
2[1+ x ] ∸ 2[1+ y ] = double (x ∸ y)
1+[2 x ] ∸ 1+[2 y ] = double (x ∸ y)
2[1+ x ] ∸ 1+[2 y ] = if does (x <? y) then 0ᵇ else 1+[2 (x ∸ y) ]
1+[2 x ] ∸ 2[1+ y ] = if does (x ≤? y) then 0ᵇ else pred (double (x ∸ y))
∸-magma : Magma 0ℓ 0ℓ
∸-magma = magma _∸_
x∸0≡x : ∀ x → x ∸ 0ᵇ ≡ x
x∸0≡x zero = refl
x∸0≡x 2[1+ _ ] = refl
x∸0≡x 1+[2 _ ] = refl
x∸x≡0 : ∀ x → x ∸ x ≡ 0ᵇ
x∸x≡0 zero = refl
x∸x≡0 2[1+ x ] = x≡0⇒double[x]≡0 (x∸x≡0 x)
x∸x≡0 1+[2 x ] = x≡0⇒double[x]≡0 (x∸x≡0 x)
toℕ-homo-∸ : ∀ x y → toℕ (x ∸ y) ≡ (toℕ x) ℕ.∸ (toℕ y)
toℕ-homo-∸ zero zero = refl
toℕ-homo-∸ zero 2[1+ y ] = refl
toℕ-homo-∸ zero 1+[2 y ] = refl
toℕ-homo-∸ 2[1+ x ] zero = refl
toℕ-homo-∸ 2[1+ x ] 2[1+ y ] = begin
toℕ (double (x ∸ y)) ≡⟨ toℕ-double (x ∸ y) ⟩
2 ℕ.* toℕ (x ∸ y) ≡⟨ cong (2 ℕ.*_) (toℕ-homo-∸ x y) ⟩
2 ℕ.* (toℕ x ℕ.∸ toℕ y) ≡⟨ ℕ.*-distribˡ-∸ 2 (ℕ.suc (toℕ x)) (ℕ.suc (toℕ y)) ⟩
toℕ 2[1+ x ] ℕ.∸ toℕ 2[1+ y ] ∎
where open ≡-Reasoning
toℕ-homo-∸ 2[1+ x ] 1+[2 y ] with x <? y
... | yes x<y = sym (ℕ.m≤n⇒m∸n≡0 (toℕ-mono-≤ (inj₁ (even<odd x<y))))
... | no x≮y = begin
ℕ.suc (2 ℕ.* toℕ (x ∸ y)) ≡⟨ cong (ℕ.suc ∘ (2 ℕ.*_)) (toℕ-homo-∸ x y) ⟩
ℕ.suc (2 ℕ.* (toℕ x ℕ.∸ toℕ y)) ≡⟨ cong ℕ.suc (ℕ.*-distribˡ-∸ 2 (toℕ x) (toℕ y)) ⟩
ℕ.suc (2 ℕ.* toℕ x ℕ.∸ 2 ℕ.* toℕ y) ≡⟨ sym (ℕ.∸-suc (ℕ.*-monoʳ-≤ 2 (toℕ-mono-≤ (≮⇒≥ x≮y)))) ⟩
ℕ.suc (2 ℕ.* toℕ x) ℕ.∸ 2 ℕ.* toℕ y ≡⟨ sym (cong (ℕ._∸ 2 ℕ.* toℕ y) (ℕ.+-suc (toℕ x) (1 ℕ.* toℕ x))) ⟩
2 ℕ.* (ℕ.suc (toℕ x)) ℕ.∸ ℕ.suc (2 ℕ.* toℕ y) ∎
where open ≡-Reasoning
toℕ-homo-∸ 1+[2 x ] zero = refl
toℕ-homo-∸ 1+[2 x ] 2[1+ y ] with x ≤? y
... | yes x≤y = sym (ℕ.m≤n⇒m∸n≡0 (toℕ-mono-≤ (inj₁ (odd<even x≤y))))
... | no _ = begin
toℕ (pred (double (x ∸ y))) ≡⟨ toℕ-pred (double (x ∸ y)) ⟩
ℕ.pred (toℕ (double (x ∸ y))) ≡⟨ cong ℕ.pred (toℕ-double (x ∸ y)) ⟩
ℕ.pred (2 ℕ.* toℕ (x ∸ y)) ≡⟨ cong (ℕ.pred ∘ (2 ℕ.*_)) (toℕ-homo-∸ x y) ⟩
ℕ.pred (2 ℕ.* (toℕ x ℕ.∸ toℕ y)) ≡⟨ cong ℕ.pred (ℕ.*-distribˡ-∸ 2 (toℕ x) (toℕ y)) ⟩
ℕ.pred (2 ℕ.* toℕ x ℕ.∸ 2 ℕ.* toℕ y) ≡⟨ ℕ.pred[m∸n]≡m∸[1+n] (2 ℕ.* toℕ x) (2 ℕ.* toℕ y) ⟩
2 ℕ.* toℕ x ℕ.∸ ℕ.suc (2 ℕ.* toℕ y) ≡⟨ sym (cong (2 ℕ.* toℕ x ℕ.∸_) (ℕ.+-suc (toℕ y) (1 ℕ.* toℕ y))) ⟩
ℕ.suc (2 ℕ.* toℕ x) ℕ.∸ 2 ℕ.* (ℕ.suc (toℕ y)) ∎
where open ≡-Reasoning
toℕ-homo-∸ 1+[2 x ] 1+[2 y ] = begin
toℕ (double (x ∸ y)) ≡⟨ toℕ-double (x ∸ y) ⟩
2 ℕ.* toℕ (x ∸ y) ≡⟨ cong (2 ℕ.*_) (toℕ-homo-∸ x y) ⟩
2 ℕ.* (toℕ x ℕ.∸ toℕ y) ≡⟨ ℕ.*-distribˡ-∸ 2 (toℕ x) (toℕ y) ⟩
2 ℕ.* toℕ x ℕ.∸ 2 ℕ.* toℕ y ∎
where open ≡-Reasoning
fromℕ-homo-∸ : ∀ m n → fromℕ (m ℕ.∸ n) ≡ (fromℕ m) ∸ (fromℕ n)
fromℕ-homo-∸ = homomorphic₂-inv ∸-magma ℕ.∸-magma
(cong fromℕ) toℕ-inverseᵇ toℕ-homo-∸
even∸odd-for≥ : x ≥ y → 2[1+ x ] ∸ 1+[2 y ] ≡ 1+[2 (x ∸ y) ]
even∸odd-for≥ {x} {y} x≥y with x <? y
... | no _ = refl
... | yes x<y = contradiction x≥y (<⇒≱ x<y)
odd∸even-for> : x > y → 1+[2 x ] ∸ 2[1+ y ] ≡ pred (double (x ∸ y))
odd∸even-for> {x} {y} x>y with x ≤? y
... | no _ = refl
... | yes x≤y = contradiction x>y (≤⇒≯ x≤y)
x≤y⇒x∸y≡0 : x ≤ y → x ∸ y ≡ 0ᵇ
x≤y⇒x∸y≡0 {x} {y} = toℕ-injective ∘ trans (toℕ-homo-∸ x y) ∘ ℕ.m≤n⇒m∸n≡0 ∘ toℕ-mono-≤
x∸y≡0⇒x≤y : x ∸ y ≡ 0ᵇ → x ≤ y
x∸y≡0⇒x≤y {x} {y} = toℕ-cancel-≤ ∘ ℕ.m∸n≡0⇒m≤n ∘ trans (sym (toℕ-homo-∸ x y)) ∘ cong toℕ
x<y⇒y∸x>0 : x < y → y ∸ x > 0ᵇ
x<y⇒y∸x>0 {x} {y} = toℕ-cancel-< ∘ subst (ℕ._> 0) (sym (toℕ-homo-∸ y x)) ∘ ℕ.m<n⇒0<n∸m ∘ toℕ-mono-<
[x∸y]+y≡x : x ≥ y → (x ∸ y) + y ≡ x
[x∸y]+y≡x {x} {y} x≥y = toℕ-injective (begin
toℕ (x ∸ y + y) ≡⟨ toℕ-homo-+ (x ∸ y) y ⟩
toℕ (x ∸ y) ℕ.+ toℕ y ≡⟨ cong (ℕ._+ toℕ y) (toℕ-homo-∸ x y) ⟩
(toℕ x ℕ.∸ toℕ y) ℕ.+ toℕ y ≡⟨ ℕ.m∸n+n≡m (toℕ-mono-≤ x≥y) ⟩
toℕ x ∎)
where open ≡-Reasoning
x+y∸y≡x : ∀ x y → (x + y) ∸ y ≡ x
x+y∸y≡x x y = +-cancelʳ-≡ _ _ x ([x∸y]+y≡x (x≤y+x y x))
[x+y]∸x≡y : ∀ x y → (x + y) ∸ x ≡ y
[x+y]∸x≡y x y = trans (cong (_∸ x) (+-comm x y)) (x+y∸y≡x y x)
x+[y∸x]≡y : x ≤ y → x + (y ∸ x) ≡ y
x+[y∸x]≡y {x} {y} x≤y = begin-equality
x + (y ∸ x) ≡⟨ +-comm x _ ⟩
(y ∸ x) + x ≡⟨ [x∸y]+y≡x x≤y ⟩
y ∎
where open ≤-Reasoning
∸-+-assoc : ∀ x y z → (x ∸ y) ∸ z ≡ x ∸ (y + z)
∸-+-assoc x y z = toℕ-injective $ begin
toℕ ((x ∸ y) ∸ z) ≡⟨ toℕ-homo-∸ (x ∸ y) z ⟩
toℕ (x ∸ y) ℕ.∸ n ≡⟨ cong (ℕ._∸ n) (toℕ-homo-∸ x y) ⟩
(k ℕ.∸ m) ℕ.∸ n ≡⟨ ℕ.∸-+-assoc k m n ⟩
k ℕ.∸ (m ℕ.+ n) ≡⟨ cong (k ℕ.∸_) (sym (toℕ-homo-+ y z)) ⟩
k ℕ.∸ (toℕ (y + z)) ≡⟨ sym (toℕ-homo-∸ x (y + z)) ⟩
toℕ (x ∸ (y + z)) ∎
where open ≡-Reasoning; k = toℕ x; m = toℕ y; n = toℕ z
+-∸-assoc : ∀ x {y z} → z ≤ y → (x + y) ∸ z ≡ x + (y ∸ z)
+-∸-assoc x {y} {z} z≤y = toℕ-injective $ begin
toℕ ((x + y) ∸ z) ≡⟨ toℕ-homo-∸ (x + y) z ⟩
(toℕ (x + y)) ℕ.∸ n ≡⟨ cong (ℕ._∸ n) (toℕ-homo-+ x y) ⟩
(k ℕ.+ m) ℕ.∸ n ≡⟨ ℕ.+-∸-assoc k n≤m ⟩
k ℕ.+ (m ℕ.∸ n) ≡⟨ cong (k ℕ.+_) (sym (toℕ-homo-∸ y z)) ⟩
k ℕ.+ toℕ (y ∸ z) ≡⟨ sym (toℕ-homo-+ x (y ∸ z)) ⟩
toℕ (x + (y ∸ z)) ∎
where
open ≡-Reasoning; k = toℕ x; m = toℕ y; n = toℕ z; n≤m = toℕ-mono-≤ z≤y
x+y∸x+z≡y∸z : ∀ x y z → (x + y) ∸ (x + z) ≡ y ∸ z
x+y∸x+z≡y∸z x y z = begin-equality
(x + y) ∸ (x + z) ≡⟨ sym (∸-+-assoc (x + y) x z) ⟩
((x + y) ∸ x) ∸ z ≡⟨ cong (_∸ z) ([x+y]∸x≡y x y) ⟩
y ∸ z ∎
where open ≤-Reasoning
suc[x]∸suc[y] : ∀ x y → suc x ∸ suc y ≡ x ∸ y
suc[x]∸suc[y] x y = begin-equality
suc x ∸ suc y ≡⟨ cong₂ _∸_ (suc≗1+ x) (suc≗1+ y) ⟩
(1ᵇ + x) ∸ (1ᵇ + y) ≡⟨ x+y∸x+z≡y∸z 1ᵇ x y ⟩
x ∸ y ∎
where open ≤-Reasoning
∸-mono-≤ : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
∸-mono-≤ {x} {y} {u} {v} x≤y v≤u = toℕ-cancel-≤ (begin
toℕ (x ∸ u) ≡⟨ toℕ-homo-∸ x u ⟩
toℕ x ℕ.∸ toℕ u ≤⟨ ℕ.∸-mono (toℕ-mono-≤ x≤y) (toℕ-mono-≤ v≤u) ⟩
toℕ y ℕ.∸ toℕ v ≡⟨ sym (toℕ-homo-∸ y v) ⟩
toℕ (y ∸ v) ∎)
where open ℕ.≤-Reasoning
∸-monoˡ-≤ : (x : ℕᵇ) → (_∸ x) Preserves _≤_ ⟶ _≤_
∸-monoˡ-≤ x y≤z = ∸-mono-≤ y≤z (≤-refl {x})
∸-monoʳ-≤ : (x : ℕᵇ) → (x ∸_) Preserves _≥_ ⟶ _≤_
∸-monoʳ-≤ x y≥z = ∸-mono-≤ (≤-refl {x}) y≥z
x∸y≤x : ∀ x y → x ∸ y ≤ x
x∸y≤x x y = begin
x ∸ y ≤⟨ ∸-monoʳ-≤ x (0≤x y) ⟩
x ∸ 0ᵇ ≡⟨ x∸0≡x x ⟩
x ∎
where open ≤-Reasoning
x∸y<x : {x y : ℕᵇ} → x ≢ 0ᵇ → y ≢ 0ᵇ → x ∸ y < x
x∸y<x {x} {y} x≢0 y≢0 = begin-strict
x ∸ y ≡⟨ cong₂ _∸_ (sym (suc-pred x≢0)) (sym (suc-pred y≢0)) ⟩
suc px ∸ suc py ≡⟨ suc[x]∸suc[y] px py ⟩
px ∸ py ≤⟨ x∸y≤x px py ⟩
px <⟨ pred[x]<x x≢0 ⟩
x ∎
where open ≤-Reasoning; px = pred x; py = pred y
*-distribˡ-∸ : _*_ DistributesOverˡ _∸_
*-distribˡ-∸ x y z = toℕ-injective $ begin
toℕ (x * (y ∸ z)) ≡⟨ toℕ-homo-* x (y ∸ z) ⟩
k ℕ.* (toℕ (y ∸ z)) ≡⟨ cong (k ℕ.*_) (toℕ-homo-∸ y z) ⟩
k ℕ.* (m ℕ.∸ n) ≡⟨ ℕ.*-distribˡ-∸ k m n ⟩
(k ℕ.* m) ℕ.∸ (k ℕ.* n) ≡⟨ cong₂ ℕ._∸_ (sym (toℕ-homo-* x y)) (sym (toℕ-homo-* x z)) ⟩
toℕ (x * y) ℕ.∸ toℕ (x * z) ≡⟨ sym (toℕ-homo-∸ (x * y) (x * z)) ⟩
toℕ ((x * y) ∸ (x * z)) ∎
where open ≡-Reasoning; k = toℕ x; m = toℕ y; n = toℕ z
*-distribʳ-∸ : _*_ DistributesOverʳ _∸_
*-distribʳ-∸ = comm∧distrˡ⇒distrʳ *-comm *-distribˡ-∸
*-distrib-∸ : _*_ DistributesOver _∸_
*-distrib-∸ = *-distribˡ-∸ , *-distribʳ-∸