逆方向のリスト

普通はリストは、

　　・ → ・ → ・ → ・ → []
　　↓　　↓　　↓　　↓

見たいに作るわけなんですが、これだと、1 - ( 2 - ( 3 - ... ) みたいになるので、人の直観とは合わないかも。

　　　 ← ・ ← ・ ← ・ ←
　　 　　↓　　↓　　↓

みたいにすると、((( 1 - 2) - 3 ) - 4 ) ... になります。引き算がまともになる。

で、Tree から list に変換する時に、順方向と逆方向が可能。 なのだが、逆方向がなかなか書けない。なんか一時間以上かかったぞ。

だいぶ焼きが廻ってるな。

これで、パターンを作って Agda の群論の式を整形する方式は割と便利。

　　data MP　: Carrier → Set (Level.suc n) where
　　　　am　: (x : Carrier )　 →　MP　x
　　　　_o_ : {x y : Carrier } →　MP　x →　MP　y → MP　( x ∙ y )

　　mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
　　mpf (am x) y = x ∙ y
　　mpf (m o m₁) y = mpf m ( mpf m₁ y )

　　mp-flatten : {x : Carrier } → (m : MP x ) → Carrier
　　mp-flatten　m = mpf m ε

　　mpl1 : Carrier → {x : Carrier } → MP x → Carrier
　　mpl1 x (am y) = x ∙ y
　　mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1

　　mpl : {x z : Carrier } → MP x → MP z　→ Carrier
　　mpl (am x)　m = mpl1 x m
　　mpl (m o m1) m2 = mpl m (m1 o m2)

　　mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier
　　mp-flattenl m = mpl m (am ε)

　　test1 : ( f g : Carrier ) → Carrier
　　test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

　　test2 : ( f g : Carrier ) → test1 f g ≡　g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙　(f ∙ g) ⁻¹　∙ ε
　　test2 f g = _≡_.refl

　　test3 : ( f g : Carrier ) → Carrier
　　test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

　　test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))
　　test4 f g = _≡_.refl