blob: b340df90bb9abb4d6982439954fef3f66864ad65 (
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
|
{-# OPTIONS --safe #-}
module Problem3 where
open import Data.List
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Empty
open import Data.Nat.Properties using (≤-step; n<1+n; <⇒≢; module ≤-Reasoning)
data _⊑_ {A : Set} : List A → List A → Set where
⊑-nil : [] ⊑ []
⊑-cons : ∀{x}{xs ys} → xs ⊑ ys → (x ∷ xs) ⊑ (x ∷ ys)
⊑-skip : ∀{x}{xs ys} → xs ⊑ ys → xs ⊑ (x ∷ ys)
⊑-refl : ∀{A : Set}(xs : List A) → xs ⊑ xs
⊑-refl [] = ⊑-nil
⊑-refl (x ∷ xs) = ⊑-cons (⊑-refl xs)
-- Induct on the second relation, then the first.
⊑-trans : ∀{A : Set}{xs ys zs : List A} → xs ⊑ ys → ys ⊑ zs → xs ⊑ zs
⊑-trans xs⊑ys (⊑-skip ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)
⊑-trans ⊑-nil ⊑-nil = ⊑-nil
⊑-trans (⊑-cons xs⊑ys) (⊑-cons ys⊑zs) = ⊑-cons (⊑-trans xs⊑ys ys⊑zs)
⊑-trans (⊑-skip xs⊑ys) (⊑-cons ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)
⊑-len : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → length xs ≤ length ys
⊑-len ⊑-nil = z≤n
⊑-len (⊑-cons xs⊑ys) = s≤s (⊑-len xs⊑ys)
⊑-len (⊑-skip xs⊑ys) = ≤-step (⊑-len xs⊑ys)
∷-injectiveᵣ : {A : Set} {x y : A} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
∷-injectiveᵣ refl = refl
private
lemma : {A : Set} {w : A} {xs ys zs ws : List A} → xs ≡ w ∷ ws → xs ⊑ ys → ys ≡ zs → zs ⊑ ws → ⊥
lemma {w = w} {xs} {ys} {zs} {ws} xs≡w∷ws xs⊑ys ys≡zs zs⊑ws = <⇒≢ prf (cong length (xs≡w∷ws))
where
open ≤-Reasoning
prf : length xs < length (w ∷ ws)
prf = begin-strict
length xs ≤⟨ ⊑-len xs⊑ys ⟩
length ys ≡⟨ cong length ys≡zs ⟩
length zs ≤⟨ ⊑-len zs⊑ws ⟩
length ws <⟨ n<1+n (length ws) ⟩
length (w ∷ ws) ∎
⊑-antisym-no-K :
∀{A : Set}{xs ys zs ws : List A} → xs ⊑ zs → ws ⊑ ys → xs ≡ ys → zs ≡ ws → xs ≡ zs
⊑-antisym-no-K ⊑-nil ⊑-nil []≡[] []≡[]′ = refl
⊑-antisym-no-K (⊑-cons xs⊑zs) (⊑-cons ws⊑ys) x∷xs≡y∷ys x∷zs≡y∷ws = cong (_ ∷_) (⊑-antisym-no-K xs⊑zs ws⊑ys (∷-injectiveᵣ x∷xs≡y∷ys) (∷-injectiveᵣ x∷zs≡y∷ws))
⊑-antisym-no-K (⊑-skip xs⊑zs) ws⊑ys xs≡ys z∷zs≡ws = ⊥-elim (lemma (sym z∷zs≡ws) ws⊑ys (sym xs≡ys) xs⊑zs)
⊑-antisym-no-K xs⊑zs (⊑-skip ws⊑ys) xs≡y∷ys zs≡ws = ⊥-elim (lemma xs≡y∷ys xs⊑zs zs≡ws ws⊑ys)
⊑-antisym : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → ys ⊑ xs → xs ≡ ys
⊑-antisym xs⊑ys ys⊑xs = ⊑-antisym-no-K xs⊑ys ys⊑xs refl refl
|
