Mercurial > hg > Members > kono > Proof > automaton

changeset 217:119ab3f823f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
NInduction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Jun 2021 17:57:07 +0900
parents 06df58697178
children 689be82c08fa
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/nat.agda
diffstat 2 files changed, 26 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 11:52:50 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 17:57:07 2021 +0900
@@ -246,14 +246,18 @@
         ... | tri≈ ¬a refl ¬c = yes record { factor = 1 ; is-factor = div1*k+0=k }
         ... | tri> ¬a ¬b c = no (div<k k>1 (s≤s z≤n ) c )
         decl : {m  : ℕ } → 0 < m → m - k < m
-        decl {zero} ()
-        decl {suc m} = {!!}
+        decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
+        ind : (p : ℕ ) → Dec (Dividable k (p - k)) → Dec (Dividable k p)
+        ind p (yes y) = yes (subst (λ g → Dividable k g) (minus+n k≤p ) (proj1 ( div+div y div= ))) where
+           k≤p :  k < suc p -- k * factor y + 0 ≡ p - k 
+           k≤p  = {!!}
+        ind p (no n) = no (λ d → n {!!} )
         I : Ninduction ℕ  _  F
         I = record {
               pnext = λ p → p - k
-            ; fzero = λ {m} eq → {!!}
-            ; decline = λ {m} lt → decl lt
-            ; ind = λ {p} prev → {!!}
+            ; fzero = λ {m} eq → F0 m eq
+            ; decline = λ {m} lt → decl lt -- Dec (Dividable k (p - k)) → Dec (Dividable k p)
+            ; ind = λ {p} prev → ind p prev
           } 
 
 gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
--- a/automaton-in-agda/src/nat.agda	Mon Jun 21 11:52:50 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Mon Jun 21 17:57:07 2021 +0900
@@ -381,6 +381,9 @@
 y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x
 y<sx→y≤x (s≤s lt) = lt 
 
+fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
+fi0 .0 z≤n = refl
+
 f-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
   → (f : P → ℕ) 
   → Finduction P Q f
@@ -391,8 +394,6 @@
 ... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where 
    f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p
    f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) where
-      fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
-      fi0 .0 z≤n = refl
    f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x)
    ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a 
    ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where
@@ -409,24 +410,23 @@
     decline : {p : P} → 0 < f p  → f (pnext p) < f p
     ind : {p : P} → Q (pnext p) → Q p
 
+s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j
+s≤s→≤ (s≤s lt) = lt
+
 n-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
   → (f : P → ℕ) 
   → Ninduction P Q f
   → (p : P ) → Q p
-n-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f (Ninduction.pnext I p))
-... | tri> ¬a ¬b ()
-... | tri≈ ¬a b ¬c = Ninduction.fzero I (sym b) 
-... | tri< lt _ _ = f-induction0 p (f p) {!!}  where 
-   f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x → Q p
-   f-induction0 p zero le = Ninduction.ind I (Ninduction.fzero I {!!}) where
-      fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
-      fi0 .0 z≤n = refl
-   f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x)
-   ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a 
-   ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (y<sx→y≤x f1)) where
-       f1 : f (Ninduction.pnext I (Ninduction.pnext I p)) < suc x
-       f1 = subst (λ k → f (Ninduction.pnext I (Ninduction.pnext I p)) < k ) b ( Ninduction.decline I {Ninduction.pnext I p}
-         (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) ))
-   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c ) 
+n-induction {n} {m} {P} {Q} f I p  = f-induction0 p (f (Ninduction.pnext I p)) ≤-refl where 
+   f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x  →  Q p
+   f-induction0 p zero lt = Ninduction.fzero I {p} (fi0 _ lt) 
+   f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x) 
+   ... | tri< (s≤s a)  ¬b ¬c = f-induction0 p x a
+   ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (s≤s→≤ nle) ) where
+      f>0 :  0 < f (Ninduction.pnext I p)
+      f>0 = subst (λ k → 0 < k ) (sym b) ( s≤s z≤n ) 
+      nle : suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ suc x
+      nle = subst (λ k → suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ k) b (Ninduction.decline I {Ninduction.pnext I p} f>0 ) 
+   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )