-title:    AgdaによるGalois理論のプログラミング

--motivation 

5次方程式が代数的に解けないことの復習

数学書では省略されてても Agda は許してくれない

計算で示しても、それが証明になっているかどうかは別

証明付きデータ構造を使う

計算と証明が「全部つながってる」

　この計算、いったい、何を計算してるの?

それを型で示す

--Galois theory :  多項式方程式

  (x - α)(x - β)(x - γ) = 0

と因数分解されればαβγが解になる。

--Galois theory :  解と置換群(対称群)

αβγを入れ替えても良い(Symmetric Group))。これが

  (x - α)(x - β) = 0

に帰着されるなら、αβ を入れ替えても良い。ならば、αβγ の置換で

   αβγ = βαγ

にならないとおかしい。

--Galois theory :  可解群

   αβγ = βαγ
   α⁻¹β⁻¹αβγγ⁻¹ = α⁻¹β⁻¹βαγγ⁻¹
   α⁻¹β⁻¹αβ = e  (交換子 Commutator)

なので、対称群のすべての要素を α⁻¹β⁻¹αβ の形にするのを繰り返して e になれば良い(可解群)。

(もちろん、これは証明になってない。気分的な説明。本当は正規拡大体とか代数的拡大とか)

ここは今回は Agda で証明しません。

あれ? 割と Agda の得意な分野なのでできるはず。やさしくはないだろうけど

Agdaは抽象的な証明が得意

--5次方程式が代数的に解けないことの証明

5次の対称群は可解でないことを示せばよい。2,3,4次は可解。教科書だと

<center><img src="fig/altin.jpg"></center>

これは良い方で、岩波だと練習問題。

<center><img src="fig/iwanami-gendai.jpg"></center>

--数学の本の記述の特徴

理解した後で読むとちゃんと書いてある

理解する前には何が書いてあるのかわからない

--Agda でちゃんとやろうぜ

Curry Howard 対応に基づく定理証明支援系

    依存型を持つ純関数型言語

    依存型とは、型を値に持つ変数

    命題そのものは Set という型を持つ

構文的には Haskell とほぼ同じ。Coq と違い、何もしてくれない。全部、自分で証明を書く。(いさぎよい)

--Agda :            lambda

A → B の証明

  →intro : {A B : Set } → A →  B → ( A → B )
  →intro _ b = λ x → b
     
  →elim : {A B : Set } → A → ( A → B ) → B
  →elim a f = f a 

引数の値は、型の証明

入力は∀が付いていると考える(∃はあとで)

--Agda :            record

A ∧ B の証明

    record _∧_ (A B : Set) : Set where
      field
         proj1 : A
         proj2 : B

    ∧elim : {A B : Set} → ( A ∧ B ) → A 
    ∧elim a∧b = proj1 a∧b 

    ∧intro : {A B : Set} → A → B → ( A ∧ B ) 
    ∧intro a b = record { proj1 = a ; proj2 = b }

--Agda :            data

A ∨ B の証明

    data _∨_ (A B : Set) : Set where
      case1 : A → A ∨ B
      case2 : B → A ∨ B

    ∨intro : {A B : Set} → A → ( A ∨ B ) 
    ∨intro a =  case1

    ∨elim : {A B : Set} → ( A ∨ A ) → A 
    ∨elim (case1 a) = a
    ∨elim (case2 a) = a

--Agda :            negation

    data ⊥ : Set where

constructor のないデータ構造(偽

    ⊥-elim : {A : Set } -> ⊥ -> A
    ⊥-elim ()

起きない入力は () 。λ () とも書ける

    data ⊤ : Set where
       tt : ⊤

要素が一つしかない型(真

--Agda :            unification

    data _≡_ {A : Set } : A → A → Set where
       refl :  {x : A} → x ≡ x

    ≡intro : {A : Set} {x : A } → x ≡ x
    ≡intro  = refl

    ≡elim : {A : Set} {x y : A } → x ≡ y → y ≡ x
    ≡elim refl = refl

項(正規化された)として等しい。変数はどうするの? 十分に instanciation されない場合は黄色くなる。

その他、細かい問題が... internal parametricity... inspect...

でも、これで全部。さぁ、Agda を書こう。

--Galois theory i nAgda :        Commutator

    [_,_] :  Carrier   → Carrier   → Carrier  
    [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 

こんな風に数学の教科書通りに Unicode を使って書けるところが Agda の良いところ

    data Commutator (P : Carrier → Set ) : (f : Carrier) → Set  where
      comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ] 
      ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g

    deriving : ( i : ℕ ) → Carrier → Set 
    deriving 0 x = ⊤
    deriving (suc i) x = Commutator (deriving i) x

Set を返してるのはなに? Set は何かの命題、 つまり真偽として扱って良い。したがって

　　P : Carrier → Set

これは Carrier の部分集合を指定する命題となる。 (Carrier は群の要素の型)

交換子 Commutator p は述語 f p で限定された p : Carrier が [ g , h ] という形で生成されることを示している。

deriving i は、Carrier の部分集合で、Commutator を再帰的に繰り返して得られたもの

--Galois theory in Agda :        Solvable

    record solvable : Set (Level.suc n ⊔ m) where
      field 
         dervied-length : ℕ
         end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε  

存在∃は record で書く。ある dervied-length : ℕ があって、その回数のderive の繰り返しで  x ≈ ε になる

この record を構成できれば、その群は可解ということになる。これで問題は定義できた

--Galois theory in Agda :        Symmetric group 

対称群の要素は置換だが、Agdaの標準ライブラリだと有限な数のBijectionとして定義される

   Permutation p p

定義は複雑だが二つの写像 _⟨$⟩ˡ_  _⟨$⟩ʳ_ と  y ⟨$⟩ˡ (y ⟨$⟩ʳ x) ≡ x と  y ⟨$⟩ʳ (y ⟨$⟩ˡ x) ≡ x からなる record 

残念ながら扱いにくい。同等性とか。単純に x ≡ y を証明できない(Agdaの制約 1)

しかし群であることを示すのは簡単

--Permutation :        Data.Fin

有限な数

   data Fin : ℕ → Set where
     zero : {n : ℕ} → Fin (suc n)
     suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

x : Fin 3 のように使う

Fin 0 の値は存在しない

     _⟨$⟩ˡ_ : Fin p →  Fin p

--Permutation :        List

置換は List ℕ で表されるので、それで良いのだが、List  ℕ が全部置換になるわけではない

そこで減少列 FL とその大小関係を定義する

    data  FL : (n : ℕ )→ Set where
       f0 :  FL 0 
       _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)

    data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
       f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
       f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )

すると、これは置換と 1 to 1 になる。しかし  1 to 1 の証明は煩雑。しかし、簡単な方法があるかも。

煩雑でも証明できてしまえば問題ないので、簡単にする motivation はあまりでない。

でも簡単にしておくと、次に使えるかも。

--Proofs : 2

これで道具立てはそろったので証明に行く

まず、二次対称群から

   sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
   sym2lem0 = ?
   solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
   solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  }

となるのだが、g と h が何かわからないので FL 2 に変換する

FL 2 は

   zero :: (zero :: f0)

というものなので、これが pid つまり恒等置換であることは証明してあるのだが

   FL-inject : {n : ℕ }  → {g h : Permutation n n }  → perm→FL g ≡  perm→FL h → g =p= h

を証明して使う。ところが、

  pleq  : {n  : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y

を使うと

   p0 :  FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
   p0 = pleq _ _ refl

とできる。Injection は圏論でいう Equalizaer で写像した先で等しいなら手元でも等しいという性質

--Proofs : 3

2でこれなので 3 は絶望的に煩雑になる

たぶん、ガロアはそれを手で計算したはず

--Proofs : 5

5は、solvable が存在しない、つまり否定を示せばよい
solvable から矛盾 counter-example を作る

    ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
    ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where

3次の対称群を含むことを示せばよいのだが、それが dervie-any-3rot0 
実は dervie-any-3rot0 と dervie-any-3rot1 がいる

教科書だと「要素三つがとれるよね」と書いてあるが、Agda だと具体的に取ってくる必要がある。「あとは同じだよね」
と書いてあっても、それを示す必要がある。

--もっと簡単にできるでしょ

derving は簡単に計算できるので、それで証明した方が良いんじゃないの?

確かにその通り

計算は簡単だが、それを証明にするにはどうすれば良いの?

    すべての交換子の組み合せを計算している

を証明すればよい

つまり sort された List に、全部の要素が含まれている (どんな要素でも入っている) any
ことを Agda で書く

それには Fresh List というのを使う

--Fresh List

(A : Set )と (R : A → A → Set) に対して

      data List# : Set 
        []   : List#
        cons : (a : A) (as : List#) → fresh a as → List#

という List を定義する

      fresh : (a : A) (as : List#) → Set 
      fresh a []        = ⊤
      fresh a (cons x xs _) = R a ∧ fresh a xs

普通の∷ (cons)の代わりに _∷#_ を使う

      infixr 5 _∷#_
      pattern _∷#_ x xs = cons x xs _

これも Set を値にしている。Fresh List の最後とそうでないもので fresh の中身が違う

List の要素毎に、fresh が存在するので、結構でかいものになる(O(2^n))。

<center><img src="fig/fresh.svg"></center>

    FList : (n : ℕ ) → Set
    FList n = List# (FL n) ⌊ _f<?_ ⌋

    fr1 : FList 3
    fr1 =
       ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
       ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
       []

と定義できる。これで FList 3 が sort されていることが「証明されている」。
⌊ _f<?_ ⌋ が不思議だが...

--Fresh List :        Any

  data Any : List# A R → Set  where
    here  : ∀ {x xs pr} → P x → Any (cons x xs pr)
    there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)

ここにあったら here、先にあるなら there

    Any (x ≡_) (FLinsert x xs)

という形で使う。
      x ≡_
は
      λ y → x ≡ y
のこと。  _≡_ x と書いても良い。

ちなみに、
      x _≡
は
      λ y → y ≡ x
なので意味が異なる (≡は対称なので結局は同じなのだが、Agda の推論はそこまでカバーしない)

これで三日くらい悩みました

--Fresh List :        Insert

普通の insert と変わらないけど、fresh を作る必要がある

    FLinsert : {n : ℕ } → FL n → FList n  → FList n 
    FLinsert {zero} f0 y = f0 ∷# []
    FLinsert {suc n} x [] = x ∷# []
    FLinsert {suc n} x (cons a y x₁) with FLcmp x a
    ... | tri≈ ¬a b ¬c  = cons a y x₁
    ... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
    FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
    FLinsert {suc n} x (cons a y yr)  | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )

--Fresh List :        Property on Insert / Cons 

    x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_) (FLinsert x xs)
    nextAny : {n : ℕ} → {x h : FL n } → {L : FList n}  → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_) L → Any (x ≡_) (cons h L hr )
    insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)

あたりがあると便利

--Fresh List :        Any on Pair

Commutator (それを作っていたのだった) は任意の pair なので

    record AnyComm {n m l : ℕ}  (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
       field
         commList : FList l
         commAny : (p : FL n) (q : FL m)
             → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q
             → Any (fpq p q ≡_) commList

つまり二つの FList から、組を全部生成する必要がある。(fpq は ∧  の方が良かったか?)

    (p,q)   (p,qn) ....           (p,q0)
    pn,q       
    :        AnyComm FL0 FL0 P  Q
    p0,q       

こんな風に再帰で作れる(やさしくない

--Fresh List :        Solved using Fresh List

まず全部の FL が入ってる FList

    record AnyFL (n : ℕ) : Set where
       field
         allFL : FList n
         anyP : (x : FL n) → Any (x ≡_ ) allFL 

これは AnyComm から作れる (やさしくない

次に Commutator 

    CommFListN  : ℕ →  FList n
    CommFListN  zero = allFL (anyFL n)
    CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))

そして、Commutator がちゃんと全部入っていることを示す(やさしい

    CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i)

すると

    CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid

という形で可解を定義できる。

--Proofs :        2

以下のように極めて簡単になった(やった!

   stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt)
   stage2FList = refl

   solved1 :  (x : Permutation 2 2) → deriving 1 x → x =p= pid
   solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where
      solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 )
      solved0 = CommStage→ 2 1 x dr

このまま 3, 4を証明可能

--Proofs :        5

e 以外を含む stage 3 が stage 4 と同じことを示すだけで可解でないことを示せる

しかし5を計算すると停まらない(きっと停まるが遅すぎる

メモリは食わない (FList 5 自体は計算できて、それで抑えられる)

単に計算が遅い

--時間

    agda sym3.agda  258.01s user 2.95s system 98% cpu 4:23.68 total
    agda sym3n.agda  9.18s user 0.45s system 95% cpu 10.089 total
    agda sym2n.agda  9.09s user 0.35s system 99% cpu 9.454 total
    agda sym2.agda  9.34s user 0.50s system 94% cpu 10.448 total
    agda sym4.agda  9.38s user 0.37s system 99% cpu 9.784 total
    agda sym5.agda  9.04s user 0.34s system 99% cpu 9.427 total


--しかし、Agda には compiler が!

コンパイルすれば計算可能

    ./sym5n  0.00s user 0.01s system 37% cpu 0.044 total


ただし、それは証明には接続できない

型検査時に compile して計算する機能はない

これが証明に接続されると、5次が可解でないことはわかるが、その理由はわからない。
不可解な証明だということになる。

--Analysis :        overhead of proof carrying data structure

Fin, Commutator, FL, Fresh , Any, FList は、すべて証明付きデータ構造

証明は実行時ではなく型検査時に行われるので実行時のオーバヘッドは理論的にはない

Any や fresh は実行されない型しか計算しないコードになる

しかし、Fresh は Product を含んでいるので実際に heapを食うのでオーバーヘッドがあるように見える

ところが、それは使われないので実行時には明示的に触らない限り生成されない(遅延評価

なので、普通に高速に計算される

--Analysis        connection of computation and type

普通は何を計算したのかは計算機は知らない

まして作った人以外はさっぱりわからない

しかし、証明付きデータならば、そこに何を計算したのかが書いてある

ただ

　　プログラミングは、めっちゃ面倒

でも、それができるならプログラミングの信頼性は上がる

しかし、それでも完全に正しいとは...

--Appendix : ZF fix

証明があっても正しいとは限らない

去年のZFには間違いがあって

    record OD : Set (suc n ) where
      field
        def : (x : Ordinal  ) → Set n

OD ⇔ Ordinal を要求すると矛盾になる

    ¬OD-order : ( & : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( & x ) → & x o< & y) → ⊥
    ¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )

なので最大値を付けてやると良い

    record HOD : Set (suc n) where
      field
        od : OD
        odmax : Ordinal
        <odmax : {y : Ordinal} → def od y → y o< odmax

つまり証明が合ってても仮定が間違ってたらダメ

これは (集合論の用語での) Set と Class の区別になっている。つまり OD が Class で、最大値があれば集合になる。

--Appendix : Topology

今年は

    record Toplogy  ( L : HOD ) : Set (suc n) where
       field
           OS    : HOD
           OS⊆PL :  OS ⊆ Power L 
           o∪ : { P : HOD }  →  P  ⊆ OS           → OS ∋ Union P
           o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q  → OS ∋ (p ∩ q)

やっても良いかも。 Tychonovの定理の証明とか(やさしくなさそう

あるいは ZF の cohen model とか

    record Filter  ( L : HOD  ) : Set (suc n) where
       field
           filter : HOD   
           f⊆PL :  filter ⊆ Power L 
           filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
           filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)

Topology と Filter は似てることがわかる

--Permutation :        等号

    record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
        field
           peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q

を統合して使う   

    x  ≡ y → x =p y

は言えるが

    x =p y → x  ≡ y

は仮定するしかない。(Functional Extentionality)

--Permutation :        Data.Fin と Data.Nat

suc と zero が自然数と重なっていて扱いを気をつける必要がある

   data ℕ : Set where
     zero : ℕ
     suc  : ℕ  → ℕ

x ∧ x < n で不等号を持ち歩く方法でも良いのだが...

x < n も 

    data _≤_ : Rel ℕ 0ℓ where
      z≤n : ∀ {n}                 → zero  ≤ n
      s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

と再帰的データ構造なので二重に持ち歩くことになるので美しくない

--Permutation :        FL と Permutation の対応の証明

Permutation の combinator 表現を使う

    pprep  先頭に一つ置換を増やす
    pswap  先頭の二つを入れ替える

これだけで任意の置換を構成できる

これから pins という任意の置換に任意の位置に 0(の位置の要素) を入れる関数を作る

そして、pins の逆を

    pshrink 置換を一つ減らす

を作って構成する

極めて煩雑な証明になる


--Fresh List : witness

⌊ _f<?_ ⌋ は witness と呼ばれるもので、 

    data Dec : {R : FL → FL → Set} : Set where
        yes :   R → Dec R
        no  : ¬ R → Dec R

    x f<? y with FLcmp x y
    ... | tri< a ¬b ¬c = yes a
    ... | tri≈ ¬a refl ¬c = no ( ¬a )
    ... | tri> ¬a ¬b c = no ( ¬a )


--sym5

abc が反例。これが常に残ることを示す

     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
     counter-example eq with ←pleq _ _ eq
     ...  | ()

二つ余地を確保する

     ins2 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) 

abc と dba を作る

     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     abc i<3 j<4 = ins2 3rot i<3 j<4
     dba : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4

abc が derive されることを示す

     dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
          → deriving n (abc i<3 j<4 ) 
     dervie-any-3rot0 0 i<3 j<4 = lift tt 
     dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where
        commd : {n : ℕ } → (f g : Permutation 5 5)
               →  deriving n f
               →  deriving n g
               → Commutator (deriving n) [ f , g ]
        commd {n} f g df dg =  comm {deriving n} {f} {g} df dg

df と dg が前に derive されたもの

        df =  dervie-any-3rot1 i  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
        dg =  dervie-any-3rot1 i  (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) 

それは、再帰的に作れるのだが種(dbaとaec)を二つ計算する必要がある

それは右回転と左回転があって、 dervie-any-3rot0 と dervie-any-3rot1 で交互に作られる

そのつくり方だが...

        tc = triple i<3 j<4
        dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
        aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
        ceq : abc i<3 j<4  =p=  [ dba0 , aec0 ]  
        ceq = record { peq = peq (abc= tc) }

dba と aec を作るのだが

     record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
       field 
         dba0<3 : Fin 4
         dba1<4 : Fin 5
         aec0<3 : Fin 4
         aec1<4 : Fin 5
         abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot)  (fin≤n {3} dba0<3) (fin≤n {4} dba1<4)  , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]

     open Triple
     triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot
     triple z≤n z≤n =                               record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple z≤n (s≤s z≤n) =                         record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
       ....

と自分でうまく2つの余地を選択する必要がある

もちろん、計算することは可能だが...