[Agda] Feedback requested on automated decision module

[Gregory Crosswhite]

 Hey everyone!

I went ahead and wrote up a module that provides functions for
automatically deciding proofs for functions on finite things. I've
attached it and an example file using it to this e-mail. In short, using
it looks like this:

module Pauli

...

data Pauli : Set where
I : Pauli
X : Pauli
Y : Pauli
Z : Pauli

_⋅_ : Pauli → Pauli → Pauli
X ⋅ X = I
X ⋅ Y = Z
X ⋅ Z = Y
Y ⋅ X = Z
Y ⋅ Y = I
Y ⋅ Z = X
Z ⋅ X = Y
Z ⋅ Y = X
Z ⋅ Z = I
I ⋅ a = a
a ⋅ I = a

finite : LeftInverse (P.setoid Pauli) (P.setoid (Fin 4))
...

open Decision finite using (decide; decide₂; decide₃)

⋅-identity : Identity I _⋅_
⋅-identity = fromYes (decide (_⋅_ I) id) refl , fromYes (decide (flip
_⋅_ I) id) refl

⋅-commutative : Commutative _⋅_
⋅-commutative = fromYes (decide₂ (_⋅_) (flip _⋅_)) refl

⋅-inverse : Inverse I id _⋅_
⋅-inverse = fromYes (decide (λ x → x ⋅ x) (const I)) refl , fromYes
(decide (λ x → x ⋅ x) (const I)) refl

⋅-associative : Associative _⋅_
⋅-associative = fromYes (decide₃ (λ x y z → (x ⋅ y) ⋅ z) (λ x y z → x ⋅
(y ⋅ z))) refl

All of the "magic" is in the decide functions, which basically takes the
functions that you give it, chains them with the "from" function in the
LeftInverse record, and then runs all? to decide the equalities. From
there it uses the fact that "(from ∘ to) a = a" to map this result into
a statement on the original function by chaining it with the "to" function.

I wrote a function mapDec that lets one take a value of type Dec A and
map it to a value of type Dec B given A -> B and B -> A. I've e-mailed
this list with patches that add this function to Relation.Nullary, and
which also add a Category.Functor.Exp module for ExpFunctor and
providing an ExpFunctor record for Dec.

I also found it convenient to define functions all?₂, all?₃, cong₃,
Fun₃, and _on₃_, which are just extensions of existing functions to
higher subscript values.

I've attached two modules: Decision.agda, which contains the decision
algorithm, and Pauli.agda, which contains the example I have above but
with the missing parts filled in. They were both coded against the
development version of the standard library pulled from the darcs
repository earlier today.

So, are people interested in seeing this functionality included in the
standard library? If so, do you all have any suggestions for me on how I
should clean up / generalize the module to fit in with the standard
library? I was envisioning it being another submodule of Data.Fin, but I
am sure that people here will come up with better ideas. :-)

Cheers,
Greg

-------------- next part --------------
open import Data.Fin using (Fin)
open import Data.Fin.Dec using (all?)
open import Data.Fin.Props using (eq?)
open import Function using (_∘_; id; _on_; Fun₁; Fun₂)
open import Function.Equality as FEq hiding (_∘_; id)
open import Function.LeftInverse as LeftInverse hiding (_∘_; id)
open import Function.LeftInverse using (LeftInverse)
open import Relation.Binary.PropositionalEquality as PEq
import Relation.Binary.EqReasoning as EqReasoning
open import Relation.Nullary using (Dec; yes; no; expfunctor)

module Decision
  {n}
  {A : Set}
  (finite : LeftInverse (PEq.setoid A) (PEq.setoid (Fin n)))
  where

infix 4 _≟_

private
  to : A → Fin n
  to = FEq._⟨$⟩_ (LeftInverse.to finite)

  from : Fin n → A
  from = FEq._⟨$⟩_ (LeftInverse.from finite)

_≟_ : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)
_≟_ = eq? (LeftInverse.injection finite)

from∘to : ∀ {a} → (from ∘ to) a ≡ a
from∘to {a} = LeftInverse.left-inverse-of finite a

mapDec : ∀ {P : Set} {Q : Set} → (P → Q) → (Q → P) → Dec P → Dec Q
mapDec f _ (yes p) = yes (f p)
mapDec _ g (no p) = no (p ∘ g)
                              
decide : ∀ (f g : Fun₁ A) → Dec (∀ a → f a ≡ g a)
decide f g =
  mapDec
    f∘from≡g∘from→f≡g
    f≡g→f∘from≡g∘from
    (all? (λ a → (f ∘ from) a ≟ (g ∘ from) a))
  where
    open EqReasoning (PEq.setoid A)

    f≡g→f∘from≡g∘from :
      ∀ {f g : Fun₁ A}
      → (∀ a → f a ≡ g a)
      → (∀ b → (f ∘ from) b ≡ (g ∘ from) b)
    f≡g→f∘from≡g∘from proveFor = proveFor ∘ from

    f∘from≡g∘from→f≡g :
      ∀ {f g : Fun₁ A}
      → (∀ b → (f ∘ from) b ≡ (g ∘ from) b)
      → (∀ a → f a ≡ g a)
    f∘from≡g∘from→f≡g {f} {g} proveFor a = begin
      f a                ≈⟨ sym (PEq.cong f from∘to) ⟩
      (f ∘ from ∘ to) a  ≈⟨ proveFor (to a) ⟩
      (g ∘ from ∘ to) a  ≈⟨ PEq.cong g from∘to ⟩
      g a                ∎

all?₂ : ∀ {P : Fin n → Fin n → Set} → (∀ a b → Dec (P a b)) → Dec (∀ a b → P a b)
all?₂ f = all? (λ a → all? (λ b → f a b))

decide₂ : ∀ (f g : Fun₂ A) → Dec (∀ a b → f a b ≡ g a b)
decide₂ f g =
  mapDec
    f∘from≡g∘from→f≡g
    f≡g→f∘from≡g∘from
    (all?₂ (λ a b → (f on from) a b ≟ (g on from) a b))
  where
    open EqReasoning (PEq.setoid A)

    f≡g→f∘from≡g∘from :
      ∀ {f g : Fun₂ A}
      → (∀ a b → f a b ≡ g a b)
      → (∀ a b → (f on from) a b ≡ (g on from) a b)
    f≡g→f∘from≡g∘from proveFor a b = proveFor (from a) (from b)

    f∘from≡g∘from→f≡g :
      ∀ {f g : Fun₂ A}
      → (∀ a b → (f on from) a b ≡ (g on from) a b)
      → (∀ a b → f a b ≡ g a b)
    f∘from≡g∘from→f≡g {f} {g} proveFor a b = begin
      f a b                  ≈⟨ sym (PEq.cong₂ f from∘to from∘to) ⟩
      (f on (from ∘ to)) a b ≈⟨ proveFor (to a) (to b) ⟩
      (g on (from ∘ to)) a b ≈⟨ PEq.cong₂ g from∘to from∘to ⟩
      g a b                  ∎

cong₃ : ∀ {A B C D : Set}
        (f : A → B → C → D) {a b c x y z} → a ≡ x → b ≡ y → c ≡ z → f a b c ≡ f x y z
cong₃ f refl refl refl = refl

Fun₃ : (A : Set) → Set
Fun₃ A = A → A → A → A

_on₃_ : ∀ {A B C} → (B → B → B → C) → (A → B) → (A → A → A → C)
_on₃_ f g x y z = f (g x) (g y) (g z)

all?₃ : ∀ {P : Fin n → Fin n → Fin n → Set} → (∀ a b c → Dec (P a b c)) → Dec (∀ a b c → P a b c)
all?₃ f = all? (λ a → all?₂ (λ b c → f a b c))

decide₃ : ∀ (f g : Fun₃ A) → Dec (∀ a b c → f a b c ≡ g a b c)
decide₃ f g =
  mapDec
    f∘from≡g∘from→f≡g
    f≡g→f∘from≡g∘from
    (all?₃ (λ a b c → (f on₃ from) a b c ≟ (g on₃ from) a b c))
  where
    open EqReasoning (PEq.setoid A)

    f≡g→f∘from≡g∘from :
      ∀ {f g : Fun₃ A}
      → (∀ a b c → f a b c ≡ g a b c)
      → (∀ a b c → (f on₃ from) a b c ≡ (g on₃ from) a b c)
    f≡g→f∘from≡g∘from proveFor a b c = proveFor (from a) (from b) (from c)

    f∘from≡g∘from→f≡g :
      ∀ {f g : Fun₃ A}
      → (∀ a b c → (f on₃ from) a b c ≡ (g on₃ from) a b c)
      → (∀ a b c → f a b c ≡ g a b c)
    f∘from≡g∘from→f≡g {f} {g} proveFor a b c = begin
      f a b c                   ≈⟨ sym (cong₃ f from∘to from∘to from∘to) ⟩
      (f on₃ (from ∘ to)) a b c ≈⟨ proveFor (to a) (to b) (to c) ⟩
      (g on₃ (from ∘ to)) a b c ≈⟨ cong₃ g from∘to from∘to from∘to ⟩
      g a b c                   ∎
-------------- next part --------------
module Pauli where

import Algebra.FunctionProperties
open import Data.Fin using (Fin; #_; suc; zero)
open import Data.Fin.Props using (eq?)
open import Data.Product
open import Function using (id; flip; const)
import Function.LeftInverse as LeftInverse
open import Function.LeftInverse using (LeftInverse)
open import Relation.Binary.PropositionalEquality as P 
open import Relation.Nullary.Core using (Dec; yes; no)
import Decision

data Pauli : Set where
  I : Pauli
  X : Pauli
  Y : Pauli
  Z : Pauli

_⋅_ : Pauli → Pauli → Pauli
X ⋅ X = I
X ⋅ Y = Z
X ⋅ Z = Y
Y ⋅ X = Z
Y ⋅ Y = I
Y ⋅ Z = X
Z ⋅ X = Y
Z ⋅ Y = X
Z ⋅ Z = I
I ⋅ a = a
a ⋅ I = a

to : Pauli → Fin 4
to I = # 0
to X = # 1
to Y = # 2
to Z = # 3

from : Fin 4 → Pauli
from zero = I
from (suc zero) = X
from (suc (suc zero)) = Y
from (suc (suc (suc zero))) = Z
from (suc (suc (suc (suc ()))))

finite : LeftInverse (P.setoid Pauli) (P.setoid (Fin 4))
finite = record
  { to              = P.→-to-⟶ to
  ; from            = P.→-to-⟶ from
  ; left-inverse-of = from∘to
  }
  where
  from∘to : ∀ x → from (to x) ≡ x
  from∘to I = refl
  from∘to X = refl
  from∘to Y = refl
  from∘to Z = refl

fromYes : ∀ {P} {p} (x : Dec P) → x ≡ yes p → P
fromYes {P} {p} .(yes p) refl = p

open Decision finite using (decide; decide₂; decide₃)
open Algebra.FunctionProperties {A = Pauli} _≡_

⋅-identity : Identity I _⋅_
⋅-identity = fromYes (decide (_⋅_ I) id) refl , fromYes (decide (flip _⋅_ I) id) refl

⋅-commutative : Commutative _⋅_
⋅-commutative = fromYes (decide₂ (_⋅_) (flip _⋅_)) refl

⋅-inverse : Inverse I id _⋅_
⋅-inverse = fromYes (decide (λ x → x ⋅ x) (const I)) refl , fromYes (decide (λ x → x ⋅ x) (const I)) refl

⋅-associative : Associative _⋅_
⋅-associative = fromYes (decide₃ (λ x y z → (x ⋅ y) ⋅ z) (λ x y z → x ⋅ (y ⋅ z))) refl