Mercurial > hg > Members > kono > Proof > automaton

changeset 133:65bea0aad363

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Nov 2019 14:30:11 +0900
parents 370b3fc69c1a
children 14cf0e1c8d91
files agda/finiteSet.agda
diffstat 1 files changed, 48 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Sun Nov 24 11:37:00 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 14:30:11 2019 +0900
@@ -388,6 +388,16 @@
     elm<n : toℕ (FiniteSet.F←Q fa elm ) < n
 
 open Fin-<
+
+Fin-<-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
+   → ( s t : Fin-< n<m fa ) 
+   → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → s ≡ t
+Fin-<-cong n<m fa _ _ refl HE.refl = refl
+
+lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j
+lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl
+lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j )
+
 fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (Fin-< n<m fa) {n}
 fin-< {A} {zero} {m} (s≤s z≤n) fa  = record { Q←F = λ () ; F←Q = λ () ; finiso← = λ () ; finiso→ = λ ()  }
 fin-< {A} {suc n} {m} (s≤s n<m) fa = iso-fin (fin-∨1 (fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa)) iso where
@@ -395,11 +405,11 @@
    fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa
    iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa)
    lastf = FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))
-   last1 = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
    c1 : toℕ lastf ≡ n 
    c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl )
    f<n : toℕ lastf < suc n
    f<n = subst ( λ k → k < suc n ) (sym c1) a<sa
+   last1 = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
    ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
    ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a }
    ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one
@@ -412,16 +422,48 @@
    ISO.iso← iso (case1 one) | tri> ¬a ¬b c = ⊥-elim ( ¬b c1 )
    ISO.iso← iso (case2 x) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x))) n
    ISO.iso← iso (case2 x) | tri< a ¬b ¬c = cong ( λ k → case2 record { elm = elm x ; elm<n = k } ) (lemma1 _ _) where
-     lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j
-     lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl
-     lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j )
    ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) )
    ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) )
    ISO.iso→ iso x with ISO.A←B iso x  
    ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n | inspect (λ x → ISO.B←A iso ( ISO.A←B iso x )) x
+   ... | tri> ¬a ¬b c | record { eq = e } = ⊥-elim ( nat-≤> c (elm<n x) )
    ... | tri< a ¬b ¬c | record { eq = e } = {!!}
-   ... | tri≈ ¬a b ¬c | record { eq = e } = {!!} 
-   ... | tri> ¬a ¬b c | record { eq = e } = ⊥-elim ( nat-≤> c (elm<n x) )
+   ... | tri≈ ¬a b ¬c | record { eq = e } = begin
+           record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) ; elm<n = lemma5 }
+       ≡⟨ Fin-<-cong (s≤s n<m) fa _ _ (sym (lemma2 b)) lemma7 ⟩
+           record { elm = elm x ; elm<n = elm<n x }
+       ≡⟨⟩
+           x
+       ∎
+    where
+      open ≡-Reasoning
+      lemma3 : {n m : ℕ } (x : Fin m)  → toℕ x ≡ n → (n<m : n < m ) → x ≡ fromℕ≤ n<m
+      lemma3 _ refl n<m = sym ( fromℕ≤-toℕ  _ n<m )
+      lemma4 : {x : A } → (x=n : toℕ (FiniteSet.F←Q fa x)  ≡ n ) → fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ≡ FiniteSet.F←Q fa x
+      lemma4 {x} refl = sym ( lemma3 _ refl (Data.Nat.Properties.<-trans n<m a<sa)) 
+      lemma2 : {x : A} → toℕ (FiniteSet.F←Q fa x) ≡ n → x ≡ FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
+      lemma2 {x} refl = sym ( begin
+                 FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) 
+              ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma4 refl) ⟩
+                 FiniteSet.Q←F fa ( FiniteSet.F←Q fa x )
+              ≡⟨ FiniteSet.finiso→ fa _ ⟩
+                 x 
+              ∎ ) where open ≡-Reasoning
+      lemma5 : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) < suc n
+      lemma5 = subst (λ k → suc k ≤ suc n)
+            (sym
+             (subst (λ k → toℕ k ≡ n)
+              (sym
+               (FiniteSet.finiso← fa
+                (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))))
+              (subst (λ k → k ≡ n)
+               (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))) refl)))
+                    a<sa
+      lemma7 : lemma5 ≅ elm<n x
+      lemma7 with lemma2 b
+      ... | refl with lemma1 lemma5 (elm<n x)
+      ... | refl = HE.refl
+
    ISO.iso→ iso x | case2 x1 = {!!}
    -- ISO.iso→ iso x | case2 x1 | tri< a ¬b ¬c = ?
    -- ISO.iso→ iso x | case2 x1 | tri≈ ¬a b ¬c = {!!}