{-
Agda code accompanying the draft "A greedy algorithm for dropping digits",
by Richard Bird and Shin-Cheng Mu, submitted to Journal of Functional Programming.
-}
module DelsProofs where
open import Data.Empty
open import Data.Unit hiding (_≟_; _≤_)
open import Data.Bool hiding (_≤_; _<_; _≟_)
open import Data.Product
open import Data.Nat
open import Data.Nat.Properties using (≤-trans; ≤∧≢⇒<; <-cmp)
open import Data.Fin hiding (_≤_; _<_; _≟_; _+_)
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
{-
Problem: remove k digits from a number, such that the
resulting number is maximum.
7 6 4 3 6 5 2 3
6 4 3 6 5 2 3
7 4 3 6 5 2 3
-}
data _⊴_ : List ℕ → List ℕ → Set where
[]⊴ : ∀ {xs} → [] ⊴ xs
<⊴ : ∀ {x y xs ys} → x < y → (x ∷ xs) ⊴ (y ∷ ys)
≡⊴ : ∀ {x xs ys} → xs ⊴ ys → (x ∷ xs) ⊴ (x ∷ ys)
⊴-refl : ∀ {xs} → xs ⊴ xs
⊴-refl {[]} = []⊴
⊴-refl {x ∷ xs} = ≡⊴ ⊴-refl
≤≡⊴ : ∀ {x y xs} → x ≤ y → (x ∷ xs) ⊴ (y ∷ xs)
≤≡⊴ {x} {y} x≤y with x ≟ y
... | no x≠y = <⊴ (≤∧≢⇒< x≤y (λ x≡y → x≠y x≡y))
... | yes refl = ⊴-refl
{-
Task1 : construct gstep : List ℕ → List ℕ, such that mdel xs
removes one digits from xs, and gstep xs is maximum w.r.t (⊴).
In the paper gstep was calculated by equational reasoning.
We can also construct gstep in Agda.
Task2 : construct a way to remove n elements from gstep xs, such that
n+1
xs ------> zs
| 1 | ys ⊴ zs
V V
gstep xs ---> ys
n
-}
-- Task 1.
-- rather than let gstep return a list, we let it return an index.
-- del1 xs i deletes the ith element in xs.
del1 : {A : Set} → (xs : List A) → Fin (length xs) → List A
del1 (x ∷ xs) zero = xs
del1 (x ∷ xs) (suc n) = x ∷ del1 xs n
-- try constructing mdel and its correctness proof maxdel together.
-- Note: For some reason Agda cannot see that the gstep we are about
-- to construct is terminating. Thus I need this TERMINATING pragma.
{-# TERMINATING #-}
gstep : (xs : List ℕ) → 0 < length xs → Fin (length xs)
gstep (x ∷ []) _ = zero
gstep (x ∷ y ∷ xs) p with <-cmp x y
... | tri< _ _ _ = zero
... | tri≈ _ _ _ = suc (gstep (y ∷ xs) (s≤s z≤n))
... | tri> _ _ _ = suc (gstep (y ∷ xs) (s≤s z≤n))
maxdel : (xs : List ℕ) → (p : 0 < length xs)
→ ∀ k → del1 xs k ⊴ del1 xs (gstep xs p)
maxdel (x ∷ []) p zero = []⊴
maxdel (x ∷ y ∷ xs) p k with <-cmp x y
maxdel (x ∷ y ∷ xs) p zero | tri< _ _ _ = ⊴-refl
maxdel (x ∷ y ∷ xs) p (suc k) | tri< x ¬a ¬b x>y = <⊴ x>y
maxdel (x ∷ y ∷ xs) p (suc k) | tri> ¬a ¬b x>y = ≡⊴ (maxdel (y ∷ xs) (s≤s z≤n) k)
{-
-- would it be nicer if we combine the code and its proof?
∃gstep : (xs : List ℕ) → 0 < length xs →
∃ (λ i → ∀ k → del1 xs k ⊴ del1 xs i)
∃gstep xs p = {! !}
-}
-- Task 2.
-- Foot records decisions gstep makes.
-- gstep xs = i iff HFoot i xs.
-- It's called Foot, referring to "foot of a hill".
data HFoot : ℕ → List ℕ → Set where
last : ∀ {x} → HFoot zero (x ∷ [])
this : ∀ {x y xs}
→ (x zs arrow is represented by
-- some ds : Dels (suc n) xs.
-- We try to construct a function "alter" that takes ds and
-- and produce another Dels (suc n) xs, which represents
-- the two arrows from xs, through gstep xs, to ys.
-- It should satisfy two properties: mono says that the
-- diagram above commutes; unfoot says that the ith element,
-- the foot, is indeed deleted.
-- Hint: at one point, we will have to pattern match on k to
-- ensure that we can still delete something.
mutual -- no mutual recursion! I use mutual merely to postpone
-- monoAux here.
-- The code and proofs are in the comment below.
-- Try it yourself?
alter : ∀ {k xs i} → Dels (suc k) xs
→ HFoot i xs → Dels (suc k) xs
alter = {! !}
mono : ∀ {k xs} {i} → (ds : Dels (suc k) xs) → (ft : HFoot i xs)
→ dels xs ds ⊴ dels xs (alter ds ft)
mono = {! !}
unfoot : ∀ {k xs} {i} → (ds : Dels (suc k) xs) → (ft : HFoot i xs)
→ IsDel i (alter ds ft)
unfoot = {! !}
{-
alter : ∀ {k xs i} → Dels (suc k) xs
→ HFoot i xs → Dels (suc k) xs
alter (keep ds) (this x