{-# OPTIONS --rewriting #-}
module Interval where
open import Decidable
open import Equality
open import EqualityRewriting
open import EquationalReasoning
open import Level
open import Order
open import Proposition
open import Sum
open import UIP
infixr 7 _∸_
postulate
𝕀 : Set
instance 𝕀order : Order 𝕀
O : 𝕀
O≤ : ∀ {i} → O ≤ i
I : 𝕀
≤I : ∀ {i} → i ≤ I
_∸_ : 𝕀 → 𝕀 → 𝕀
∸≤ : ∀ {i j} → j ≤ i → i ∸ j ≤ i
∸∸ : ∀ {i j} → j ≤ i → i ∸ (i ∸ j) ≡ j
∸δ : ∀ i → i ∸ i ≡ O
O≠I : ¬ (O ≡ I)
min : 𝕀 → 𝕀 → 𝕀
minl : ∀ {i j} → i ≤ j → min i j ≡ i
minr : ∀ {i j} → j ≤ i → min i j ≡ j
max : 𝕀 → 𝕀 → 𝕀
maxl : ∀ {i j} → j ≤ i → max i j ≡ i
maxr : ∀ {i j} → i ≤ j → max i j ≡ j
cvx : 𝕀 → 𝕀 → 𝕀 → 𝕀
cvxl : ∀ {i j k} → i ≤ k → cvx i j k ≡ min (max i j) k
cvxr : ∀ {i j k} → k ≤ i → cvx i j k ≡ min i (max (I ∸ j) k)
↑ : 𝕀 → 𝕀
↑l : ∀ {i} → i ≤ I ∸ i → ↑ i ≡ I ∸ ((I ∸ i) ∸ i)
↑r : ∀ {i} → I ∸ i ≤ i → ↑ i ≡ I
↓ : 𝕀 → 𝕀
↓l : ∀ {i} → i ≤ I ∸ i → ↓ i ≡ O
↓r : ∀ {i} → I ∸ i ≤ i → ↓ i ≡ i ∸ (I ∸ i)
∸O : ∀ {i} → i ∸ O ≡ i
∸O {i} =
proof:
i ∸ O
≡[ cong (i ∸_) (symm (∸δ i)) ]
i ∸ (i ∸ i)
≡[ ∸∸ (≤refl i) ]
i
qed
∸∸I : ∀ {i} → I ∸ (I ∸ i) ≡ i
∸∸I = ∸∸ ≤I
{-# REWRITE ∸δ ∸O ∸∸I #-}
Omin : ∀ {i} → min O i ≡ O
Omin = minl O≤
Imin : ∀ {i} → min I i ≡ i
Imin {i} = minr ≤I
{-# REWRITE Omin Imin #-}
cvxO : ∀ i j → cvx i O j ≡ i
cvxO i j =
≤ind (λ k → cvx i O k ≡ i) (λ _ → uip) i a b j
where
a : {k : 𝕀} → k ≤ i → cvx i O k ≡ i
a {k} u =
proof:
cvx i O k
≡[ cvxr u ]
min i (max (I ∸ O) k)
≡[ cong (λ j → min i (max j k)) ∸O ]
min i (max I k)
≡[ cong (min i) (maxl ≤I) ]
min i I
≡[ minl ≤I ]
i
qed
b : {k : 𝕀} → i ≤ k → cvx i O k ≡ i
b {k} v =
proof:
cvx i O k
≡[ cvxl v ]
min (max i O) k
≡[ cong (λ j → min j k) (maxl O≤) ]
min i k
≡[ minl v ]
i
qed
cvxI : ∀ i j → cvx i I j ≡ j
cvxI i j =
≤ind (λ k → cvx k I j ≡ j) (λ _ → uip) j a b i
where
a : {k : 𝕀} → k ≤ j → cvx k I j ≡ j
a {k} u =
proof:
cvx k I j
≡[ cvxl u ]
min (max k I) j
≡[ cong (λ i → min i j) (maxr ≤I) ]
min I j
≡[ minr ≤I ]
j
qed
b : {k : 𝕀} → j ≤ k → cvx k I j ≡ j
b {k} v =
proof:
cvx k I j
≡[ cvxr v ]
min k (max (I ∸ I) j)
≡[ cong (λ i → min k (max i j))(∸δ I) ]
min k (max O j)
≡[ cong (min k) (maxr O≤) ]
min k j
≡[ minr v ]
j
qed
cvxδ : ∀ i j → cvx i j i ≡ i
cvxδ i j =
proof:
cvx i j i
≡[ cvxl (≤refl i) ]
min (max i j) i
≡[ minr i≤maxij ]
i
qed
where
i≤maxij : i ≤ max i j
i≤maxij =
≤ind
(λ k → k ≤ max k j)
(λ k → ≤isProp {x = k} {max k j})
j
(λ {k} u → subst (k ≤_) (symm (maxr u)) u)
(λ {k} v → subst (k ≤_) (symm (maxl v)) (≤refl k))
i
cvxOI : ∀ i → cvx O i I ≡ i
cvxOI i =
proof:
cvx O i I
≡[ cvxl O≤ ]
min (max O i) I
≡[ minl ≤I ]
max O i
≡[ maxr O≤ ]
i
qed
{-# REWRITE cvxO cvxI cvxδ cvxOI #-}
↑O : ↑ O ≡ O
↑O = ↑l O≤
↑I : ↑ I ≡ I
↑I = ↑r ≤I
↓O : ↓ O ≡ O
↓O = ↓l O≤
↓I : ↓ I ≡ I
↓I = ↓r ≤I
{-# REWRITE ↑O ↑I ↓O ↓I #-}
↓or↑ : ∀ i → (↓ i ≡ O) or (↑ i ≡ I)
↓or↑ i =
orrec f g f' g' (λ _ _ → ∥∥isProp) (≤tot i (I ∸ i))
where
f : i ≤ I ∸ i → (↓ i ≡ O or ↑ i ≡ I)
f p = (inl (↓l p)) mod∇
f' : (p p' : i ≤ I ∸ i) → f p ≡ f p'
f' p p' = cong f (≤isProp {x = i} {y = I ∸ i} {x = p} {y = p'})
g : I ∸ i ≤ i → (↓ i ≡ O or ↑ i ≡ I)
g q = (inr (↑r q)) mod∇
g' : (q q' : I ∸ i ≤ i) → g q ≡ g q'
g' q q' = cong g (≤isProp {x = I ∸ i} {y = i} {x = q} {y = q'})
module _
{ℓ : Level}
(P : 𝕀 → Set ℓ)
(f : ∀ i → ↓ i ≡ O → P i)
(g : ∀ i → ↑ i ≡ I → P i)
(h : ∀ i → (u : ↓ i ≡ O)(v : ↑ i ≡ I) → f i u ≡ g i v)
where
𝕀ind : ∀ i → P i
𝕀ind i =
orrec
(f i)
(g i)
(λ _ _ → cong (f i) uip)
(λ _ _ → cong (g i) uip)
(h i)
(↓or↑ i)
𝕀ind↓ :
(i : 𝕀)
(u : ↓ i ≡ O)
→
𝕀ind i ≡ f i u
𝕀ind↓ i u =
let
f' = λ _ _ → cong (f i) uip
g' = λ _ _ → cong (g i) uip
p = orrec (f i) (g i) f' g' (h i)
in
proof:
p (↓or↑ i)
≡[ cong p (∥∥isProp {x = ↓or↑ i} {y = inl u mod∇}) ]
p (inl u mod∇)
≡[ orcompl (f i) (g i) f' g' (h i) u ]
f i u
qed
𝕀ind↑ :
(i : 𝕀)
(v : ↑ i ≡ I)
→
𝕀ind i ≡ g i v
𝕀ind↑ i v =
let
f' = λ _ _ → cong (f i) uip
g' = λ _ _ → cong (g i) uip
p = orrec (f i) (g i) f' g' (h i)
in
proof:
p (↓or↑ i)
≡[ cong p (∥∥isProp {x = ↓or↑ i} {y = inr v mod∇}) ]
p (inr v mod∇)
≡[ orcompr (f i) (g i) f' g' (h i) v ]
g i v
qed
rev : 𝕀 → 𝕀
rev i = cvx I i O