annotate src/fin.agda @ 320:8fb16f9a882a

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 19 Sep 2023 11:11:38 +0900
parents fff18d4a063b
children e9de2bfef88d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 module fin where
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
5 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
6 open import Data.Fin.Properties hiding (≤-trans ; <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp )
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Data.Nat
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
8 open import Data.Nat.Properties
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import logic
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import nat
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Binary.PropositionalEquality
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
14 -- toℕ<n
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 fin<n {_} {zero} = s≤s z≤n
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
19 -- toℕ≤n
83
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
20 fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
21 fin≤n {_} zero = z≤n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
22 fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
23
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0 → Data.Nat.pred (toℕ f) < n
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 pred<n {suc n} {suc f} (s≤s z≤n) = fin<n
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
131
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
28 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
29 fin<asa = toℕ-fromℕ< nat.a<sa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
30
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
31 -- fromℕ<-toℕ
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 toℕ→from {0} {zero} refl = refl
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
36 -- 0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
37 -- 0≤fmax {n} = ?
210
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 131
diff changeset
38
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
39 -- 0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
40 -- 0<fmax {n} = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< {suc n} {suc (suc n)} a<sa)) (s≤s z≤n)
210
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 131
diff changeset
41
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
42 -- toℕ-injective
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 i=j {suc n} zero zero refl = refl
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
47 -- raise 1
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 fin+1 : { n : ℕ } → Fin n → Fin (suc n)
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 fin+1 zero = zero
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 fin+1 (suc x) = suc (fin+1 x)
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 open import Data.Nat.Properties as NatP hiding ( _≟_ )
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
54 fin+1≤ : { i n : ℕ } → (a : i < n) → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 fin+1≤ {0} {suc i} (s≤s z≤n) = refl
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 fin+1-toℕ : { n : ℕ } → { x : Fin n} → toℕ (fin+1 x) ≡ toℕ x
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 fin+1-toℕ {suc n} {zero} = refl
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 fin+1-toℕ {suc n} {suc x} = cong (λ k → suc k ) (fin+1-toℕ {n} {x})
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 open import Relation.Nullary
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 open import Data.Empty
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 fin-1 : { n : ℕ } → (x : Fin (suc n)) → ¬ (x ≡ zero ) → Fin n
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 fin-1 zero ne = ⊥-elim (ne refl )
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 fin-1 {n} (suc x) ne = x
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 fin-1-sx : { n : ℕ } → (x : Fin n) → fin-1 (suc x) (λ ()) ≡ x
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 fin-1-sx zero = refl
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 fin-1-sx (suc x) = refl
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 fin-1-xs : { n : ℕ } → (x : Fin (suc n)) → (ne : ¬ (x ≡ zero )) → suc (fin-1 x ne ) ≡ x
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 fin-1-xs zero ne = ⊥-elim ( ne refl )
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 fin-1-xs (suc x) ne = refl
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
77 -- suc-injective
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 -- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y → x ≡ y
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 -- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq )
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
81 -- this is refl
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
82 lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 lemma3 (s≤s lt) = refl
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
84
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
85 -- fromℕ<-toℕ
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
86 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
88 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl )
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
90 -- this requires K
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
91 --
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
92 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
94 -- <-irrelevant
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
95 -- <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
96 -- <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
97 -- <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl )
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
98
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
99 -- lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
100 -- lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
101 -- lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl )
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
102
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
103 -- fromℕ<-irrelevant
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
104 -- lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
105 -- lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl ))
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
106
320
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
107 lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
108 lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
109 lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
110
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
111 -- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
112 -- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl)
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
113
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
114 -- toℕ-fromℕ<
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
115 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 lemma11 {n} {m} {x} n<m = begin
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
117 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
118 ≡⟨ toℕ-fromℕ< _ ⟩
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 toℕ x
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 ∎ where
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 open ≡-Reasoning
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
123 x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} → toℕ x < toℕ y → Fin n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
124 x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ ))
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
126 x<y→fin-1-eq : {n : ℕ } → { x y : Fin (suc n)} → (lt : toℕ x < toℕ y ) → toℕ x ≡ toℕ (x<y→fin-1 lt )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
127 x<y→fin-1-eq {n} {x} {y} lt = sym ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
128 toℕ (fromℕ< (≤-trans lt (fin≤n y)) ) ≡⟨ toℕ-fromℕ< _ ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
129 toℕ x ∎ ) where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
130
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
131 f<→< : {n : ℕ } → { x y : Fin n} → x Data.Fin.< y → toℕ x < toℕ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
132 f<→< {_} {zero} {suc y} (s≤s lt) = s≤s z≤n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
133 f<→< {_} {suc x} {suc y} (s≤s lt) = s≤s (f<→< {_} {x} {y} lt)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
134
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
135 f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
136 f≡→≡ refl = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
137
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
138 open import Data.List
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
139 open import Relation.Binary.Definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
140
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
141 -----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
142 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
143 -- find duplicate element in a List (Fin n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
144 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
145 -- if the length is longer than n, we can find duplicate element as FDup-in-list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
146 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
147 -- How about do it in ℕ ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
148
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
149 -- fin-count : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → ℕ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
150 -- fin-count q p[ = 0
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
151 -- fin-count q (q0 ∷ qs ) with <-fcmp q q0
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
152 -- ... | tri-e = suc (fin-count q qs)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
153 -- ... | false = fin-count q qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
154
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
155 -- fin-not-dup-in-list : { n : ℕ} (qs : List (Fin n) ) → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
156 -- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
157
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
158 -- this is far easier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
159 -- fin-not-dup-in-list→len<n : { n : ℕ} (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
160 -- fin-not-dup-in-list→len<n = ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
161
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
162 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the dup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
163 fin-phase2 q [] = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
164 fin-phase2 q (x ∷ qs) with <-fcmp q x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
165 ... | tri< a ¬b ¬c = fin-phase2 q qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
166 ... | tri≈ ¬a b ¬c = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
167 ... | tri> ¬a ¬b c = fin-phase2 q qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
168 fin-phase1 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the first element
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
169 fin-phase1 q [] = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
170 fin-phase1 q (x ∷ qs) with <-fcmp q x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
171 ... | tri< a ¬b ¬c = fin-phase1 q qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
172 ... | tri≈ ¬a b ¬c = fin-phase2 q qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
173 ... | tri> ¬a ¬b c = fin-phase1 q qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
174
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
175 fin-dup-in-list : { n : ℕ} (q : Fin n) (qs : List (Fin n) ) → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
176 fin-dup-in-list {n} q qs = fin-phase1 q qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
177
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
178 record FDup-in-list (n : ℕ ) (qs : List (Fin n)) : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
179 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
180 dup : Fin n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
181 is-dup : fin-dup-in-list dup qs ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
182
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
183 list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
184 list-less [] = []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
185 list-less {n} (i ∷ ls) with <-fcmp (fromℕ< a<sa) i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
186 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ i < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
187 ... | tri≈ ¬a b ¬c = list-less ls
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
188 ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
190 fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
191 fin010 {_} {_} {x} c = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
192 toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡⟨ toℕ-fromℕ< _ ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
193 toℕ x ∎ where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
194
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
195 ---
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
196 --- if List (Fin n) is longer than n, there is at most one duplication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
197 ---
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
198 fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n)) → (len> : length qs > n ) → FDup-in-list n qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
199 fin-dup-in-list>n {zero} [] ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
200 fin-dup-in-list>n {zero} (() ∷ qs) lt
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
201 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
202 open import Level using ( Level )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
203 -- make a dup from one level below
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
204 fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list (fromℕ< a<sa ) qs ≡ false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
205 → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
206 fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
207 -- we have two loops on the max element and the current level. The disjuction means the phases may differ.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
208 f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
209 → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
210 → fin-phase2 (fin+1 i) qs ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
211 f1-phase2 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
212 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
213 f1-phase2 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
214 ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
215 ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
216 ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
217 -- two fcmp is only different in the size of Fin, but to develop both f1-phase and list-less both fcmps are required
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
218 f1-phase2 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
219 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case1 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
220 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
221 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
222 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
223 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
224 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
225 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
226 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
227 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case1 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
228 f1-phase2 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
229 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
230 f1-phase2 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
231 ... | tri< a ¬b ¬c₁ = ⊥-elim ( ¬-bool q1 refl )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
232 ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
233 ... | tri> ¬a₁ ¬b c = ⊥-elim ( ¬-bool q1 refl )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
234 f1-phase2 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
235 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
236 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
237 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
238 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
239 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
240 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
241 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
242 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
243 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case2 q1 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
244 f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
245 → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
246 → fin-phase1 (fin+1 i) qs ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
247 f1-phase1 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
248 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
249 f1-phase1 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
250 ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
251 ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
252 fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
253 fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) fin<n )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
254 ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
255 f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
256 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
257 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
258 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
259 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
260 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case1 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
261 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
262 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
263 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
264 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case1 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
265 f1-phase1 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
266 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
267 f1-phase1 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c = ⊥-elim ( ¬-bool q1 refl )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
268 f1-phase1 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
269 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
270 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
271 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
272 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
273 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
274 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
275 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
276 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
277 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
278 fdup-phase0 : FDup-in-list (suc n) qs
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
279 fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs in eq
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
280 ... | true = record { dup = fromℕ< a<sa ; is-dup = eq }
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
281 ... | false = fdup+1 qs (FDup-in-list.dup fdup) eq (FDup-in-list.is-dup fdup) where
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
282 -- if no dup in the max element, the list without the element is only one length shorter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
283 fless : (qs : List (Fin (suc n))) → length qs > suc n → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
284 fless qs lt p = fl-phase1 n qs lt p where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
285 fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1 → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
286 fl-phase2 zero (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
287 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
288 ... | tri> ¬a ¬b c = s≤s z≤n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
289 fl-phase2 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
290 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
291 ... | tri> ¬a ¬b c = s≤s ( fl-phase2 n1 qs lt p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
292 fl-phase1 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > suc n1 → fin-phase1 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
293 fl-phase1 zero (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
294 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
295 ... | tri≈ ¬a b ¬c = fl-phase2 0 qs lt p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
296 ... | tri> ¬a ¬b c = s≤s z≤n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
297 fl-phase1 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
298 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
299 ... | tri≈ ¬a b ¬c = fl-phase2 (suc n1) qs lt p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
300 ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
301 -- if the list without the max element is only one length shorter, we can recurse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
302 fdup : FDup-in-list n (list-less qs)
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
303 fdup = fin-dup-in-list>n (list-less qs) (fless qs lt eq)
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
304
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
305 --