ロマサガ3のパーティ外成長について．

RS3.agda

-- see. http://www.nicovideo.jp/watch/sm17339259
module RS3 where

open import Function
open import Function.Equivalence using (_⇔_; equivalence)
open import Data.Bool
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Product
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl; cong)
open import Data.Nat.Properties using (commutativeSemiring)
import Algebra
open Algebra.CommutativeSemiring commutativeSemiring using (+-comm; *-comm)

data イベントバトルお供Lv上昇量 : ℕ → Set where
  Lv⇑ : ∀ n → n ≤ 8 → イベントバトルお供Lv上昇量 n

パーティ外HP上昇量 : ℕ → ℕ
パーティ外HP上昇量 別れたときと再加入時のお供Lv差
  = 別れたときと再加入時のお供Lv差 div 8 * 15

パーティ外技能Lv上昇量 : ℕ → ℕ
パーティ外技能Lv上昇量 別れたときと再加入時のお供Lv差
  = 別れたときと再加入時のお供Lv差 div 16

n₁≤m₁→n₂≤m₂→n₁+n₂≤m₁+m₂ : ∀ n₁ n₂ m₁ m₂ →
                          n₁ ≤ m₁ → n₂ ≤ m₂ → n₁ + n₂ ≤ m₁ + m₂
n₁≤m₁→n₂≤m₂→n₁+n₂≤m₁+m₂ .0 .0 m₁ m₂ z≤n z≤n = z≤n
n₁≤m₁→n₂≤m₂→n₁+n₂≤m₁+m₂ .0 .(suc n₂) m₁ .(suc m₂) z≤n (s≤s {n₂} {m₂} n₂≤m₂)
  rewrite +-comm m₁ (suc m₂)
        | +-comm m₂ m₁
        = s≤s (n₁≤m₁→n₂≤m₂→n₁+n₂≤m₁+m₂ zero n₂ m₁ m₂ z≤n n₂≤m₂)
n₁≤m₁→n₂≤m₂→n₁+n₂≤m₁+m₂ .(suc m) n₂ .(suc n) m₂ (s≤s {m} {n} n₁≤m₁) n₂≤m₂
  = s≤s (n₁≤m₁→n₂≤m₂→n₁+n₂≤m₁+m₂ m n₂ n m₂ n₁≤m₁ n₂≤m₂)

n≤m→n*a≤m*a : ∀ n m a → n ≤ m → n * a ≤ m * a
n≤m→n*a≤m*a n m zero n≤m
  rewrite *-comm n 0
        | *-comm m 0
        = z≤n
n≤m→n*a≤m*a n m (suc a) n≤m
  rewrite *-comm n (suc a)
        | *-comm m (suc a)
        | *-comm a n
        | *-comm a m
        = n₁≤m₁→n₂≤m₂→n₁+n₂≤m₁+m₂ n (n * a) m (m * a) n≤m (n≤m→n*a≤m*a n m a n≤m)

drop-suc : ∀ n m → suc n ≡ suc m → n ≡ m
drop-suc .m m refl = refl

a+n≡a+m→n≡m : ∀ n m a → a + n ≡ a + m → n ≡ m
a+n≡a+m→n≡m n m zero a+n≡a+m = a+n≡a+m
a+n≡a+m→n≡m n m (suc a) a+n≡a+m = a+n≡a+m→n≡m n m a (drop-suc (a + n) (a + m) a+n≡a+m)

n*Sa≡m*Sa→n≡m : ∀ n m a → n * suc a ≡ m * suc a → n ≡ m
n*Sa≡m*Sa→n≡m zero zero a n*Sa≡m*Sa = refl
n*Sa≡m*Sa→n≡m zero (suc m) a ()
n*Sa≡m*Sa→n≡m (suc n) zero a ()
n*Sa≡m*Sa→n≡m (suc n) (suc m) a n*Sa≡m*Sa
  = cong suc (n*Sa≡m*Sa→n≡m n m a
      (a+n≡a+m→n≡m (n * suc a) (m * suc a) a
        (drop-suc (a + n * suc a) (a + m * suc a) n*Sa≡m*Sa)))

パーティ外HP15上昇ならお供Lv差は8以上 : ∀ n →
                                        パーティ外HP上昇量 n ≡ 15 →
                                        8 ≤ n
パーティ外HP15上昇ならお供Lv差は8以上 n HP15上昇
  = assert (n divMod 8) (n*Sa≡m*Sa→n≡m _ _ 14 HP15上昇)
  where
    open import Data.Fin using (toℕ)
    open import Data.Nat.Properties
    assert : (x : DivMod n 8) → DivMod.quotient x ≡ 1 → 8 ≤ n
    assert (result quotient remainder property) up
      rewrite up
            | property
            = n≤m+n (toℕ remainder) 8

パーティ外技能Lv1上昇ならお供Lv差は16以上 : ∀ n →
                                            パーティ外技能Lv上昇量 n ≡ 1 →
                                            16 ≤ n
パーティ外技能Lv1上昇ならお供Lv差は16以上 n 技能Lv1上昇
  = assert (n divMod 16) 技能Lv1上昇
  where
    open import Data.Fin using (toℕ)
    open import Data.Nat.Properties
    assert : (x : DivMod n 16) → DivMod.quotient x ≡ 1 → 16 ≤ n
    assert (result quotient remainder property) up
      rewrite up
            | property
            = n≤m+n (toℕ remainder) 16

n≤m→m≤n→n≡m : ∀ n m → n ≤ m → m ≤ n → n ≡ m
n≤m→m≤n→n≡m .0 .0 z≤n z≤n = refl
n≤m→m≤n→n≡m .(suc n) .(suc m) (s≤s {n} {m} n≤m) (s≤s m≤n)
  rewrite n≤m→m≤n→n≡m n m n≤m m≤n
        = refl

drop-s≤s : ∀ n m → suc n ≤ suc m → n ≤ m
drop-s≤s n m (s≤s Sn≤Sm) = Sn≤Sm

n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ : ∀ n₁ n₂ m₁ m₂ →
                                      n₁ ≤ m₁ → n₂ ≤ m₂ → m₁ + m₂ ≤ n₁ + n₂ →
                                      n₁ ≡ m₁ × n₂ ≡ m₂
n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ .0 .0 zero zero z≤n z≤n m₁+m₂≤n₁+n₂ = refl , refl
n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ .0 .0 zero (suc m₂) z≤n z≤n ()
n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ .0 .0 (suc m₁) m₂ z≤n z≤n ()
n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ .0 .(suc n₂) m₁ .(suc m₂) z≤n (s≤s {n₂} {m₂} n₂≤m₂) m₁+m₂≤n₁+n₂
  rewrite +-comm m₁ (suc m₂)
        | +-comm m₂ m₁
        = map id (cong suc) $
            n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ 0 n₂ m₁ m₂ z≤n n₂≤m₂ $
              drop-s≤s _ _ m₁+m₂≤n₁+n₂
n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ .(suc n₁) n₂ .(suc m₁) m₂ (s≤s {n₁} {m₁} n₁≤m₁) n₂≤m₂ m₁+m₂≤n₁+n₂
  = map (cong suc) id $
      n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ n₁ n₂ m₁ m₂ n₁≤m₁ n₂≤m₂ $
        drop-s≤s (m₁ + m₂) (n₁ + n₂) m₁+m₂≤n₁+n₂

2回で技能Lv1上昇するには各回でHP15上昇 : ∀ {n₁ n₂} →
                                         イベントバトルお供Lv上昇量 n₁ →
                                         イベントバトルお供Lv上昇量 n₂ →
                                         パーティ外技能Lv上昇量 (n₁ + n₂) ≡ 1 ⇔
                                         (パーティ外HP上昇量 n₁ ≡ 15 × パーティ外HP上昇量 n₂ ≡ 15)
2回で技能Lv1上昇するには各回でHP15上昇 {n₁} {n₂} Lv⇑₁ Lv⇑₂
  = equivalence (⇔→ {n₁} {n₂} Lv⇑₁ Lv⇑₂) (⇔← {n₁} {n₂} Lv⇑₁ Lv⇑₂)
  where
    ⇔→ : ∀ {n₁ n₂} →
         イベントバトルお供Lv上昇量 n₁ →
         イベントバトルお供Lv上昇量 n₂ →
         パーティ外技能Lv上昇量 (n₁ + n₂) ≡ 1 →
         パーティ外HP上昇量 n₁ ≡ 15 × パーティ外HP上昇量 n₂ ≡ 15
    ⇔→ {n₁} {n₂} (Lv⇑ .n₁ n₁≤8) (Lv⇑ .n₂ n₂≤8) WLv⇑≡1
      rewrite proj₁ (n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ n₁ n₂ 8 8 n₁≤8 n₂≤8 $ パーティ外技能Lv1上昇ならお供Lv差は16以上 (n₁ + n₂) WLv⇑≡1)
            | proj₂ (n₁≤m₁→n₂≤m₂→m₁+m₂≤n₁+n₂→n₁+n₂≡m₁+m₂ n₁ n₂ 8 8 n₁≤8 n₂≤8 $ パーティ外技能Lv1上昇ならお供Lv差は16以上 (n₁ + n₂) WLv⇑≡1)
            = refl , refl
    ⇔← : ∀ {n₁ n₂} →
         イベントバトルお供Lv上昇量 n₁ →
         イベントバトルお供Lv上昇量 n₂ →
         パーティ外HP上昇量 n₁ ≡ 15 × パーティ外HP上昇量 n₂ ≡ 15 →
         パーティ外技能Lv上昇量 (n₁ + n₂) ≡ 1
    ⇔← {n₁} {n₂} (Lv⇑ .n₁ n₁≤8) (Lv⇑ .n₂ n₂≤8) (proj₁ , proj₂)
      rewrite n≤m→m≤n→n≡m n₁ 8 n₁≤8 (パーティ外HP15上昇ならお供Lv差は8以上 n₁ proj₁)
            | n≤m→m≤n→n≡m n₂ 8 n₂≤8 (パーティ外HP15上昇ならお供Lv差は8以上 n₂ proj₂)
            = refl