blob: 6b41a6754aa570970539b702f9e91cebd5f76de7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
module Data.List.Relation.Binary.Suffix where
open import Data.Bool using (true; false; _∧_; _∨_)
open import Data.Empty using (⊥-elim)
open import Data.List using (List; []; _∷_; length)
open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_; setoid)
open import Data.Nat using (suc; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (n<1+n; ≤-step; <⇒≱; module ≤-Reasoning)
open import Data.Sum using (inj₁; inj₂; [_,_])
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Nullary using (yes; no; ¬_)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Sum using (_⊎-dec_)
private
variable
a ℓ : Level
module _
{A : Set a} (_≈_ : Rel A ℓ)
where
data Suffix : Rel (List A) (a ⊔ ℓ) where
base : ∀ {xs ys} → (xs≋ys : Pointwise _≈_ xs ys) → Suffix xs ys
next : ∀ y {xs ys} → Suffix xs ys → Suffix xs (y ∷ ys)
module _
{A : Set a} {_≈_ : Rel A ℓ}
where
private
_≋_ = Pointwise _≈_
_<_ = Suffix _≈_
length≤ : ∀ {xs ys} → xs < ys → length xs ≤ length ys
length≤ (base []) = z≤n
length≤ (base (x∼y ∷ xs≋ys)) = s≤s (length≤ (base xs≋ys))
length≤ (next y xs<ys) = ≤-step (length≤ xs<ys)
refl : Reflexive _≈_ → Reflexive _<_
refl refl {xs} = base (Pointwise.refl refl)
transitive : Transitive _≈_ → Transitive _<_
transitive trans xs<ys (next z ys<zs) = next z (transitive trans xs<ys ys<zs)
transitive trans (base xs≋ys) (base ys≋zs) = base (Pointwise.transitive trans xs≋ys ys≋zs)
transitive trans (next y xs<ys) (base (y∼z ∷ ys≋zs)) = next _ (transitive trans xs<ys (base ys≋zs))
antisymmetric : Symmetric _≈_ → Antisymmetric _≋_ _<_
antisymmetric sym (base xs≋ys) _ = xs≋ys
antisymmetric sym (next _ _) (base ys≋xs) = Pointwise.symmetric sym ys≋xs
antisymmetric sym (next y {x ∷ xs} {ys} x∷xs<ys) (next x y∷ys<xs) =
⊥-elim
(<⇒≱ (≤-step (n<1+n (length xs)))
(begin
suc (suc (length xs)) ≡⟨⟩
suc (length (x ∷ xs)) ≤⟨ s≤s (length≤ x∷xs<ys) ⟩
suc (length ys) ≡⟨⟩
length (y ∷ ys) ≤⟨ length≤ y∷ys<xs ⟩
length xs ∎))
where open ≤-Reasoning
minimum : Minimum _<_ []
minimum [] = base []
minimum (x ∷ xs) = next x (minimum xs)
decidable : Decidable _≈_ → Decidable _<_
decidable ≈? [] ys = yes (minimum ys)
decidable ≈? (x ∷ xs) [] = no (λ { (base ()) })
decidable ≈? (x ∷ xs) (y ∷ ys) =
Dec.map′ [ base , next y ]
(λ { (base xs≋ys) → inj₁ xs≋ys ; (next _ xs<ys) → inj₂ xs<ys })
(Pointwise.decidable ≈? (x ∷ xs) (y ∷ ys) ⊎-dec decidable ≈? (x ∷ xs) ys)
|
