Mercurial > hg > Members > kono > Proof > automaton

changeset 320:4a00e5f2b793

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 Fri, 14 Jan 2022 14:39:36 +0900
parents cd91a9f313dd
children b065ba2f68c5
files automaton-in-agda/src/bijection.agda automaton-in-agda/src/fin.agda automaton-in-agda/src/gcd.agda automaton-in-agda/src/nat.agda automaton-in-agda/src/non-regular.agda automaton-in-agda/src/root2.agda
diffstat 6 files changed, 123 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda	Wed Jan 12 21:20:16 2022 +0900
+++ b/automaton-in-agda/src/bijection.agda	Fri Jan 14 14:39:36 2022 +0900
@@ -152,7 +152,7 @@
           suc j + suc (suc k) ∎ where open ≡-Reasoning
      nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
 
-     -- increment in ths same stage
+     -- increment in the same stage
      nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
      nid2 zero zero = refl
      nid2 zero (suc j) = refl
@@ -177,7 +177,7 @@
           nxn→n (suc (suc i)) (suc j) ∎ where
              open ≡-Reasoning
 
-     -- increment ths stage
+     -- increment the stage
      nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) 
      nid00 zero = refl
      nid00 (suc i) = begin
@@ -400,7 +400,7 @@
             lton1 x + lton1 x ∎  )) where open ≤-Reasoning
 
      ---
-     --- lton uniqueness
+     --- lton injection
      ---
      lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y
      lb=b [] [] eq = refl
--- a/automaton-in-agda/src/fin.agda	Wed Jan 12 21:20:16 2022 +0900
+++ b/automaton-in-agda/src/fin.agda	Fri Jan 14 14:39:36 2022 +0900
@@ -132,6 +132,14 @@
 open import Data.List
 open import Relation.Binary.Definitions
 
+
+-----
+--
+-- find duplicate element in a List (Fin n)
+--
+--    if the length is longer than n, we can find duplicate element as FDup-in-list 
+--
+
 -- fin-count : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → ℕ
 -- fin-count q p[ = 0
 -- fin-count q (q0 ∷ qs ) with <-fcmp q q0 
@@ -145,13 +153,13 @@
 -- 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
 -- fin-not-dup-in-list→len<n = ?
 
-fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool  -- find the dup
 fin-phase2 q [] = false
 fin-phase2 q (x ∷ qs) with <-fcmp q x
 ... | tri< a ¬b ¬c = fin-phase2 q qs
 ... | tri≈ ¬a b ¬c = true
 ... | tri> ¬a ¬b c = fin-phase2 q qs
-fin-phase1 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-phase1 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool  -- find the first element
 fin-phase1 q [] = false
 fin-phase1 q (x ∷ qs) with <-fcmp q x
 ... | tri< a ¬b ¬c = fin-phase1 q qs
--- a/automaton-in-agda/src/gcd.agda	Wed Jan 12 21:20:16 2022 +0900
+++ b/automaton-in-agda/src/gcd.agda	Fri Jan 14 14:39:36 2022 +0900
@@ -696,3 +696,7 @@
 m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1
 m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq 
 
+gcd-is-gratest :  { i j  k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j 
+gcd-is-gratest {i} {j} {k} i>0 j>0 k>1 ki kj = div→k≤m k>1 (gcd>0 i j i>0 j>0 ) gcd001 where
+    gcd001 :  Dividable k ( gcd i  j ) 
+    gcd001 = gcd-div _ _ _ k>1 ki kj
--- a/automaton-in-agda/src/nat.agda	Wed Jan 12 21:20:16 2022 +0900
+++ b/automaton-in-agda/src/nat.agda	Fri Jan 14 14:39:36 2022 +0900
@@ -584,6 +584,17 @@
           k + f * k + 0 ≡⟨ eq ⟩
           m ∎  where open ≤-Reasoning  
 
+0<factor : { m k : ℕ } → k > 0 → m > 0 →  (d :  Dividable k m ) → Dividable.factor d > 0
+0<factor {m} {k} k>0 m>0 d with Dividable.factor d | inspect Dividable.factor d 
+... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< ff1 m>0 ) where
+    ff1 : 0 ≡ m 
+    ff1 = begin
+          0 ≡⟨⟩
+          0 * k + 0 ≡⟨ cong  (λ j → j * k + 0) (sym eq1) ⟩
+          Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d  ⟩
+          m ∎  where open ≡-Reasoning  
+... | suc t | _ = s≤s z≤n 
+
 div→k≤m : { m k : ℕ } → k > 1 → m > 0 →  Dividable k m → m ≥ k
 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k
 ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d )
--- a/automaton-in-agda/src/non-regular.agda	Wed Jan 12 21:20:16 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Jan 14 14:39:36 2022 +0900
@@ -46,6 +46,16 @@
 t5 : ( n : ℕ ) → Set
 t5 n = inputnn1 ( inputnn0 n i0 i1 [] ) ≡ true
 
+nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
+nn01 zero = refl
+nn01 (suc i) = {!!} where 
+      nn02 : (i : ℕ) → ( x : List In2) → inputnn ( inputnn0 i i0 i1 x ) ≡ inputnn x
+      nn02 zero _ = refl
+      nn02 (suc i) x with inputnn (inputnn0 (suc i) i0 i1 x)
+      ... | nothing = {!!}
+      ... | just []  = {!!}
+      ... | just (i0 ∷ t1)   = {!!}
+      ... | just (i1 ∷ t1)   = {!!}
 --
 --  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
 --  The function is determinted by inputs,
@@ -199,16 +209,6 @@
     n : ℕ
     n = suc (finite (afin r))
     nn =  inputnn0 n i0 i1 []
-    nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
-    nn01 zero = refl
-    nn01 (suc i) = {!!} where 
-      nn02 : (i : ℕ) → ( x : List In2) → inputnn ( inputnn0 i i0 i1 x ) ≡ inputnn x
-      nn02 zero _ = refl
-      nn02 (suc i) x with inputnn (inputnn0 (suc i) i0 i1 x)
-      ... | nothing = {!!}
-      ... | just []  = {!!}
-      ... | just (i0 ∷ t1)   = {!!}
-      ... | just (i1 ∷ t1)   = {!!}
     nn03 : accept (automaton r) (astart r) nn ≡ true
     nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
     nn09 : (n m : ℕ) → n ≤ n + m
--- a/automaton-in-agda/src/root2.agda	Wed Jan 12 21:20:16 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jan 14 14:39:36 2022 +0900
@@ -16,6 +16,7 @@
 record Rational : Set where
   field
     i j : ℕ
+    0<j : j > 0
     coprime : GCD.gcd i j ≡ 1
 
 -- record Dividable (n m : ℕ ) : Set where
@@ -95,11 +96,92 @@
           n * n * p ∎  ) ⟩
        n * n ∎ }  where open ≡-Reasoning
 
+mkRational : ( i j : ℕ ) → 0 < j → Rational
+mkRational zero j 0<j = record { i = 0 ; j = 1 ; coprime = refl  ; 0<j = s≤s z≤n } 
+mkRational (suc i) j (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where
+   d : ℕ
+   d = gcd (suc i) j
+   d>0 : gcd (suc i) j > 0
+   d>0 = GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n )
+   0<fj : Dividable.factor jd > 0
+   0<fj = 0<factor d>0  (s≤s z≤n ) jd
+   id  : Dividable d (suc i)
+   id  = proj1 (GCD.gcd-dividable (suc i) j)
+   jd  : Dividable d j 
+   jd  = proj2 (GCD.gcd-dividable (suc i) j)
+   cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
+   cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd)
+   ... | zero | record { eq  = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (GCD.gcd>0 (Dividable.factor id) (Dividable.factor jd)
+       (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) ))
+   ... | suc zero | record { eq  = eq1 } = refl
+   ... | suc (suc t) | record { eq  = eq1 } = ⊥-elim ( nat-≤> (GCD.gcd-is-gratest {suc i} {j} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where
+        -- gcd-is-gratest :  { i j  k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j
+        d1 : ℕ
+        d1 = gcd (Dividable.factor id) (Dividable.factor jd) 
+        d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1
+        d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n))
+        mul1 :  {x : ℕ} → 1 * x ≡ x
+        mul1 {zero} = refl
+        mul1 {suc x} = begin
+              1 * suc x  ≡⟨ cong suc (+-comm x _ ) ⟩ 
+              suc x ∎   where open ≡-Reasoning
+        co1  : gcd (suc i) j * d1 > 1
+        co1  = begin
+              2 ≤⟨ d1>1 ⟩ 
+              d1  ≡⟨ sym mul1 ⟩ 
+              1 * d1  ≤⟨ *≤ {1} {gcd (suc i) j } {d1} d>0 ⟩ 
+              gcd (suc i) j * d1 ∎   where open ≤-Reasoning
+        gcdd1 = GCD.gcd-dividable (Dividable.factor id) (Dividable.factor jd)
+        gcdf1 = Dividable.factor (proj1 gcdd1)
+        gcdf2 = Dividable.factor (proj2 gcdd1)
+        d1id :  Dividable (gcd (suc i) j * d1) (suc i)
+        d1id = record { factor = gcdf1 ; is-factor = begin
+              gcdf1 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ 
+              gcdf1 * (d * d1) ≡⟨ cong (λ k1 → gcdf1 * k1) (*-comm d d1) ⟩ 
+              gcdf1 * (d1 * d) ≡⟨ sym (*-assoc gcdf1 d1 d) ⟩ 
+              gcdf1 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ 
+              (gcdf1 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf1 * d1) 0)) ⟩ 
+              (gcdf1 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj1 gcdd1) ) ⟩ 
+              Dividable.factor id * d + 0 ≡⟨ Dividable.is-factor id ⟩ 
+              suc i ∎ }  where open ≡-Reasoning
+        d1jd :  Dividable (gcd (suc i) j * d1) j
+        d1jd = record { factor = gcdf2 ; is-factor = begin
+              gcdf2 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ 
+              gcdf2 * (d * d1) ≡⟨ cong (λ k1 → gcdf2 * k1) (*-comm d d1) ⟩ 
+              gcdf2 * (d1 * d) ≡⟨ sym (*-assoc gcdf2 d1 d) ⟩ 
+              gcdf2 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ 
+              (gcdf2 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf2 * d1) 0)) ⟩ 
+              (gcdf2 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj2 gcdd1) ) ⟩ 
+              Dividable.factor jd * d + 0 ≡⟨ Dividable.is-factor jd ⟩ 
+              j ∎ }  where open ≡-Reasoning
+        mul2 : {g d1 : ℕ } → g > 0 → d1 > 1 → g < g * d1
+        mul2 {suc g} {suc zero} g>0 (s≤s ())
+        mul2 {suc g} {suc (suc d2)} g>0 d1>1 = begin
+              suc (suc g) ≡⟨ cong suc (+-comm 0 _ ) ⟩ 
+              suc (suc g + 0) ≤⟨ s≤s (≤-plus-0  z≤n) ⟩ 
+              suc (suc g + (g + d2 * suc g)) ≡⟨ cong suc (sym (+-assoc  1 g _) ) ⟩ 
+              suc ((1 + g) + (g + d2 * suc g)) ≡⟨  cong (λ k → suc (k + (g + d2 * suc g) )) (+-comm 1 g) ⟩ 
+              suc ((g + 1) + (g + d2 * suc g)) ≡⟨ cong suc (+-assoc g 1 _ )  ⟩ 
+              suc (g + (1 + (g + d2 * suc g))) ≡⟨⟩ 
+              suc (g + suc (g + d2 * suc g)) ≡⟨⟩ 
+              suc (suc d2) * suc g  ≡⟨ *-comm (suc (suc d2)) _ ⟩ 
+              suc g * suc (suc d2) ∎   where open ≤-Reasoning
+        gcd<d1 : gcd (suc i) j < gcd (suc i ) j * d1
+        gcd<d1 = mul2 (GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n) ) d1>1 
+
+
 Rational* : (r s : Rational) → Rational
-Rational* r s = record  { i = {!!} ; j = {!!} ; coprime = {!!} }
+Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) ) where
+    r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0
+    r1 {x} {y} x>0 y>0 = begin
+        1 * 1 ≤⟨ *≤ {1} {x} {1} x>0 ⟩
+        x * 1 ≡⟨ *-comm x 1  ⟩
+        1 * x ≤⟨ *≤ {1} {y} {x} y>0 ⟩
+        y * x ≡⟨ *-comm y x ⟩
+        x * y ∎ where open ≤-Reasoning
 
 _r=_ : Rational → ℕ → Set
 r r= n  = (Rational.i r ≡ n) ∧ (Rational.j r ≡ 1)
 
-root-prime-irrational1 : ( p : ℕ ) → Prime p → ¬ ( ( r  : Rational ) → Rational* r r r= p )
-root-prime-irrational1 = {!!}
+root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r  : Rational ) → ¬ ( Rational* r r r= p )
+root-prime-irrational1 p pr r div = root-prime-irrational (Rational.i r) (Rational.j r) {!!} {!!} pr {!!} {!!} (Rational.coprime r)