# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574672451 -32400
# Node ID 06002e20ce5cf29ec7d24cf6e66d8b3e927835af

incudtion selection on diophantos equation

diff -r 000000000000 -r 06002e20ce5c logic.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/logic.agda	Mon Nov 25 18:00:51 2019 +0900
@@ -0,0 +1,150 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _/\_
+
+open import Relation.Binary.PropositionalEquality
+
+≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
+≡-Bool-func {true} {true} a→b b→a = refl
+≡-Bool-func {false} {true} a→b b→a with b→a refl
+... | ()
+≡-Bool-func {true} {false} a→b b→a with a→b refl
+... | ()
+≡-Bool-func {false} {false} a→b b→a = refl
+
+bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
+bool-≡-? true true = yes refl
+bool-≡-? true false = no (λ ())
+bool-≡-? false true = no (λ ())
+bool-≡-? false false = yes refl
+
+¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
+¬-bool-t {true} ne = ⊥-elim ( ne refl )
+¬-bool-t {false} ne = refl
+
+¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
+¬-bool-f {true} ne = refl
+¬-bool-f {false} ne = ⊥-elim ( ne refl )
+
+¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
+¬-bool refl ()
+
+lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
+lemma-∧-0 {true} {true} refl ()
+lemma-∧-0 {true} {false} ()
+lemma-∧-0 {false} {true} ()
+lemma-∧-0 {false} {false} ()
+
+lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
+lemma-∧-1 {true} {true} refl ()
+lemma-∧-1 {true} {false} ()
+lemma-∧-1 {false} {true} ()
+lemma-∧-1 {false} {false} ()
+
+bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
+bool-and-tt refl refl = refl
+
+bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
+bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {false} {_} ()
+
+bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
+bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {false} ()
+bool-∧→tt-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
+bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
+bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
+bool-or-41 {true} {b} refl = refl
+
+bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+
diff -r 000000000000 -r 06002e20ce5c nat.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nat.agda	Mon Nov 25 18:00:51 2019 +0900
@@ -0,0 +1,56 @@
+module nat where
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Empty
+open import Relation.Nullary
+open import  Relation.Binary.PropositionalEquality
+open import  logic
+
+
+nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+
+nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+
+nat-<≡ : { x : Nat } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
+¬a≤a  (s≤s lt) = ¬a≤a  lt
+
+a<sa : {la : Nat} → la < Suc la 
+a<sa {Zero} = s≤s z≤n
+a<sa {Suc la} = s≤s a<sa 
+
+=→¬< : {x : Nat  } → ¬ ( x < x )
+=→¬< {Zero} ()
+=→¬< {Suc x} (s≤s lt) = =→¬< lt
+
+>→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+
+<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
+<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
+<-∨ {Suc x} {Zero} (s≤s ())
+<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
+<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
+<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+
+max : (x y : Nat) → Nat
+max Zero Zero = Zero
+max Zero (Suc x) = (Suc x)
+max (Suc x) Zero = (Suc x)
+max (Suc x) (Suc y) = Suc ( max x y )
+
+-- _*_ : Nat → Nat → Nat
+-- _*_ zero _ = zero
+-- _*_ (suc n) m = m + ( n * m )
+
+exp : Nat → Nat → Nat
+exp _ Zero = 1
+exp n (Suc m) = n * ( exp n m )
diff -r 000000000000 -r 06002e20ce5c prob1.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prob1.agda	Mon Nov 25 18:00:51 2019 +0900
@@ -0,0 +1,113 @@
+module prob1 where
+
+open import Relation.Binary.PropositionalEquality 
+open import Relation.Binary.Core
+open import Data.Nat
+open import Data.Nat.Properties
+open import logic
+open import nat
+open import Data.Empty
+open import Relation.Nullary
+
+minus : (a b : ℕ ) →  ℕ
+minus a zero = a
+minus zero (suc b) = zero
+minus (suc a) (suc b) = minus a b
+
+-- All variables are positive integer
+-- A = -M*n + i +k*M  - M
+-- where n is in range (0,…,k-1) and i is in range(0,…,M-1)
+-- Goal: Prove that A can take all values of (0,…,k*M-1)
+-- A1 = -M*n1 + i1 +k*M  M, A2 = -M*n2 + i2 +k*M  - M
+-- (1) If n1!=n2 or i1!=i2 then A1!=A2
+-- Or its contraposition: (2) if A1=A2 then n1=n2 and i1=i2
+-- Proof by contradiction: Suppose A1=A2 and (n1!=n2 or i1!=i2) becomes
+-- contradiction
+-- Induction on n and i
+
+record Cond1 (A M k : ℕ )  : Set where
+   field
+      n : ℕ 
+      i : ℕ 
+      range-n : n < k 
+      range-i : i < M 
+      rule1 : i + k * M  ≡ M * (suc n) + A    -- A ≡ (i + k * M ) - (M * (suc n)) 
+
+--   k = 1 → n = 0 →  ∀ M → A = i
+--   k = 2 → n = 1 →
+
+--   i + 2 * M = M * (suc n) + A    i = suc n → A = 0 
+
+m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
+m+= {i} {j} {zero} refl = refl
+m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
+
++m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
++m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
+
+less-1 :  { n m : ℕ } → suc n < m → n < m
+less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
+less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
+
+test1 : {A M : ℕ } → (c : Cond1 A M 1 ) → Cond1.n c ≡ 0 → A ≡ Cond1.i c
+test1 {A} {M} c refl = lemma2 where
+    lemma1 : Cond1.i c + 1 * M ≡ M * 1 + A
+    lemma1 = Cond1.rule1 c
+    lemma2 : A ≡  Cond1.i c
+    lemma2 = begin
+            A
+        ≡⟨  +m= ( begin
+            A + M * 1 
+        ≡⟨ +-comm A _ ⟩
+            M * 1 + A
+        ≡⟨ sym (Cond1.rule1 c)  ⟩
+            Cond1.i c + 1 * M
+        ≡⟨ cong ( λ k → Cond1.i c + k ) (*-comm 1 _ ) ⟩
+            Cond1.i c + M * 1
+        ∎ ) ⟩
+            Cond1.i c 
+        ∎  where open ≡-Reasoning
+
+problem0-k=1 : ( A M : ℕ ) → (suc A <  M ) → Cond1 A M 1
+problem0-k=1 A M A<km = record { n = 0 ; i = A ; range-n = s≤s z≤n ; range-i = less-1 A<km ; rule1 = lemma1 }
+  where
+    lemma1 : A + 1 * M ≡ M * 1 + A
+    lemma1 = trans (+-comm A _) ( cong ( λ k → k + A ) ( *-comm _ M ) )
+
+
+problem0 : ( A M k : ℕ ) → M > 0 → k > 0 → (suc A <  k * M ) → Cond1 A M k
+problem0 A (suc M) (suc k) 0<M 0<k A<km = lemma1 k M A<km a<sa a<sa where
+    --- i loop in n loop
+    lemma1-i : ( n i : ℕ ) → (suc A <  suc k * suc M ) → n < suc k → i < suc M →  Dec ( Cond1 A (suc M) (suc k) )
+    lemma1-i n zero A<km _ _ with <-cmp (1 + suc k * suc M ) (  suc M * suc n + A)
+    lemma1-i n zero A<km _ _ | tri< a ¬b ¬c = no {!!}
+    lemma1-i n zero A<km n<k i<M | tri≈ ¬a b ¬c = yes record { n = n ; i = suc zero ; range-n = n<k ; range-i = {!!} ; rule1 = b }
+    lemma1-i n zero A<km _ _ | tri> ¬a ¬b c = no {!!}
+    lemma1-i n (suc i) A<km _ _ with <-cmp (suc i + suc k * suc M ) (  suc M * suc n + A)
+    lemma1-i n (suc i) A<km n<k i<M | tri≈ ¬a b ¬c = yes record { n = n ; i = suc i ; range-n = n<k ; range-i = i<M ; rule1 = b }
+    lemma1-i n (suc i) A<km n<k i<M | tri< a ¬b ¬c = lemma1-i n i A<km n<k (less-1 i<M)
+    lemma1-i n (suc i) A<km n<k i<M | tri> ¬a ¬b c = no {!!}
+    --- n loop
+    lemma1 : ( n i : ℕ ) → (suc A <  suc k * suc M ) → n < suc k → i < suc M →  Cond1 A (suc M) (suc k)
+    lemma1 n i A<km _ _ with <-cmp (i + suc k * suc M ) (  suc M * suc n + A)
+    lemma1 n i A<km n<k i<M | tri≈ ¬a b ¬c = record { n = n ; i = i ; range-n = n<k ; range-i = i<M ; rule1 = b }
+    lemma1 zero i A<km n<k i<M | tri< a ¬b ¬c = lemma2 i A<km i<M where
+         --- i + k * M ≡ M + A case
+         lemma2 : (  i : ℕ ) → (suc A <  suc k * suc M ) → i < suc M →  Cond1 A (suc M) (suc k) 
+         lemma2 zero A<km i<M = {!!} -- A = A = k * M
+         lemma2 (suc i) A<km i<M with <-cmp ( suc i + suc k * suc M ) ( suc M * 1 + A)
+         lemma2 (suc i) A<km i<M | tri≈ ¬a b ¬c = record { n = zero ; i = suc i ; range-n = n<k ; range-i = i<M ; rule1 = b }
+         lemma2 (suc i) A<km i<M | tri< a ¬b ¬c = lemma2 i A<km (less-1 i<M)
+         lemma2 (suc i) A<km i<M | tri> ¬a ¬b c = {!!}  -- can't happen
+    lemma1 (suc n) i A<km n<k i<M | tri< a ¬b ¬c with lemma1-i (suc n) i A<km n<k i<M
+    lemma1 (suc n) i A<km n<k i<M | tri< a ¬b ¬c | yes p = p
+    lemma1 (suc n) i A<km n<k i<M | tri< a ¬b ¬c | no ¬p = lemma1 n i A<km (less-1 n<k) i<M
+    lemma1 n i A<km n<k i<M | tri> ¬a ¬b c =  {!!}  where -- can't happen
+         cannot1 :  { n k M i A : ℕ } → n < suc k → i < suc M →  (i + suc k * suc M ) > (  suc M * suc n + A)  → ¬ ( suc A <  suc k * suc M )
+         cannot1 = {!!}
+
+problem1 : (A1 A2 M k : ℕ ) 
+    → (c1 : Cond1 A1 M k ) → (c2 : Cond1 A2 M k )
+    → ( A1 ≡ A2 ) → (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )
+problem1 = {!!}
+