FirstOrderUnificationbyStructuralRecursion.agda

module FirstOrderUnificationbyStructuralRecursion where
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning
open import Data.Nat
open import Data.Product
open import Data.Empty
open import Data.Fin
open import Data.Bool

data Maybe (A : Set) : Set where
  no  : Maybe A
  yes : A → Maybe A

lf : {S T : Set} → (f : S → T) → (S → Maybe T)
lf f = λ x → yes (f x)
rf : {S T : Set} → (f : S → Maybe T) → (Maybe S → Maybe T)
rf f no = no
rf f (yes x) = f x
lrf :{S T : Set} → (f : S → T) → (Maybe S → Maybe T)
lrf f = rf (lf f)
_∘_ : {A B C : Set} → (f : B → C) → (g : A → B) → (A → C)
f ∘ g = λ x → f (g x)

-- fact 
fact : {S T R : Set} → ∀(f : S → Maybe T)  → ∀ (g : R → S) → ∀ (s : Maybe R) → rf (f ∘ g) s ≡ (rf f ∘ lrf g) s
fact f g no = refl
fact f g (yes x) = refl

lf2 : {R S T : Set} → (f : R → S → T) → (R → S → Maybe T)
lf2 f = λ x x₁ → yes (f x x₁)

rf2 : {R S T : Set} → (f : R → S → Maybe T) → (R → Maybe S → Maybe T)
rf2 f x no = no
rf2 f x (yes x₁) = f x x₁

cf2 : {R S T : Set} → (f : R → Maybe S → Maybe T) → (Maybe R → Maybe S → Maybe T)
cf2 f no no = no
cf2 f no (yes x) = no
cf2 f (yes x) no = f x no
cf2 f (yes x) (yes x₁) = f x (yes x₁)

lrf2 : {R S T : Set} → (f : R → S → T) → (Maybe R → Maybe S → Maybe T)
lrf2 f = cf2 (rf2 (lf2 f))

record ⊤ : Set where

empty : Fin zero → Set
empty x = ⊤

-- data ⊥ : Set where

Fin' : ℕ →  Set
Fin' zero = ⊥
Fin' (suc n) = Maybe (Fin' n)

open import Data.List

revapp : {T : Set} → (xs ys : List T) → List T
revapp [] ys = ys
revapp (x ∷ xs) ys = revapp xs (x ∷ ys)

ack : (m n : ℕ) → ℕ
ack zero n = suc n
ack (suc m) zero = ack m (suc zero)
ack (suc m) (suc n) = ack m (ack (suc m) n)


data Term (n : ℕ) : Set where
  ι : (x : Fin n) → Term n -- 変数 (de bruijn index) 
  leaf : Term n -- base case の型
  _fork_ : (s t : Term n) → Term n -- arrow 型

▹ : {n m : ℕ} → (r : Fin m → Fin n) → (Fin m → Term n)
▹ r = ι ∘ r

_◃_ : {n m : ℕ} → (f : Fin m → Term n) → (Term m → Term n)
_◃_ f (ι x) = f x
_◃_ f leaf = leaf
_◃_ f (s fork t) = (f ◃ s) fork (f ◃ t) 

_◃ : {n m : ℕ} → (f : Fin m → Term n) → (Term m → Term n)
f ◃ = λ x → f ◃ x

_≐_ : {n m : ℕ} → (f g : Fin m → Term n) → Set
_≐_ {n} {m} f g = (x : Fin m) → f x ≡ g x

_◇_ : {m n l : ℕ} → (f : Fin m → Term n) → (g : Fin l → Term m) → (Fin l → Term n)
f ◇ g = (f ◃) ∘ g

fact2 : {n : ℕ} →  (t : Term n) → (ι ◃ t ≡ t)
fact2 (ι x) = refl
fact2 leaf = refl
fact2 (s fork t) = cong₂ _fork_ (fact2 s) (fact2 t)

-- (ι s) fork (ι t) ⇒ ι (s fork t) = s fork t
-- ι s = s
-- ι t = t

fact3 : {l m n : ℕ} → (f : Fin m → Term n) →  (g : Fin l → Term m)  → (t : Term l)
        → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
fact3 f g (ι x) = refl
fact3 f g leaf = refl
fact3 f g (t fork t₁) = cong₂ _fork_ (fact3 f g t) (fact3 f g t₁)


fact4 : {l m n : ℕ} → (f : Fin m → Term n) → (r : Fin l → Fin m) → ((f ◇ (▹ r)) ≐ (f ∘ r))
fact4 = λ f r x → refl

thin : {n : ℕ} → Fin (suc n) → Fin n → Fin (suc n)  -- thin <-> thick
thin {n} zero y = suc y
thin {suc n} (suc x) zero = zero
thin {suc n} (suc x) (suc y) = suc (thin x y)


-- suc a ≡ suc b → a ≡ b 
lemma1 : {n : ℕ} → (a b : Fin n) → (_≡_ {_} {Fin (suc n)} (suc a) (suc b))  → a ≡ b
lemma1 .b b refl = refl


fact5 : {n : ℕ} → (x : Fin (suc n)) → (y : Fin n) → (z : Fin n) → thin x y ≡ thin x z → y ≡ z
fact5 zero zero zero a = refl
fact5 zero zero (suc z) ()
fact5 zero (suc y) .(suc y) refl = refl
fact5 (suc x) zero zero a = refl
fact5 (suc x) zero (suc z) ()
fact5 (suc x) (suc y) zero ()
fact5 (suc x) (suc y) (suc z) a = cong suc (fact5 x y z (lemma1 (thin x y) (thin x z) a))

fact6 : {n : ℕ} → (x : Fin (suc n))  → (y : Fin n) → ((thin x y ≡ x) → ⊥)
fact6 zero zero ()
-- a  : suc zero ≡ zero
fact6 zero (suc y) ()
fact6 (suc x) zero ()
fact6 (suc x) (suc y) a = fact6 x y (lemma1 (thin x y) x a)


-- Fin (suc n) p → Fin n p
fact7 : {n : ℕ} → (x y : Fin (suc n)) → (x ≡ y → ⊥) → Σ[ y' ∈ Fin n ] (thin x y' ≡ y)
fact7 zero zero a = ⊥-elim (a refl)
fact7 zero (suc y) a = y , refl 
fact7 {zero} (suc ()) zero a
fact7 {suc n} (suc x) zero a = zero , refl
fact7 {zero} (suc ()) (suc y) a
fact7 {suc n} (suc x) (suc y) a with fact7 x y (λ x₁ → a (cong suc x₁))
fact7 {suc n} (suc x) (suc y) a | y' , p = (suc y') , cong suc p

thick : {n : ℕ} → (x y : Fin (suc n)) → Maybe (Fin n)
thick {n} zero zero = no
thick {n} zero (suc y) = yes y
thick {zero} (suc ()) zero
thick {suc n} (suc x) zero = yes x
thick {zero} (suc ()) (suc y)
thick {suc n} (suc x) (suc y) = lrf suc (thick {n} x y)

--fact8 : ∀ x → ∀ y → ∀ r → (thick x y ≡ r) → (y ≡ ?) ∨ ( Σ[ y' ∈ ? ] (thin x y' ≡ y) ∧ (yes y'))
--fact8 x y r = ?

check : {n : ℕ} → Fin (suc n) → Term (suc n) → Maybe (Term n)
check x (ι y) = lrf ι (thick x y)
check x leaf = yes leaf
check x (s fork t) = lrf2 _fork_ (check x s) (check x t)

_for_ : {n : ℕ} → (t' : Term n) → (x : Fin (suc n)) → (Fin (suc n) → Term n)
_for_ t' x y with thick x y
_for_ t' x y | no = t'
_for_ t' x y | yes y' = ι y'

fact9 : {n : ℕ} →  (t' : Term n) →  (x : Fin (suc n)) →  ((_for_ t' x) ∘ thin x) ≐ ι
fact9 {zero} t' zero = λ x → refl
fact9 {zero} t' (suc x) = λ x₁ → {!!}
fact9 {suc n} t' x = λ x₁ → {!!}


--- P.11
data AList : ℕ → ℕ → Set where
  anil : {m : ℕ} → AList m m
  _asnoc_/_ : {m : ℕ} {n : ℕ} → (σ : AList m n) → (t' : Term m) → (x : Fin (suc m)) → AList (suc m) n

sub : {m n : ℕ} → (σ : AList m n) → Fin m → Term n
sub anil = ι
sub (σ asnoc t' / x) = (sub σ) ◇ (t' for x)

_⊹⊹_ : {l m n : ℕ} → (ρ : AList m n) → (σ : AList l m) →  AList l n
ρ ⊹⊹ anil = ρ
ρ ⊹⊹ (alist asnoc t / x) = (ρ ⊹⊹ alist) asnoc t / x

fact10 : {m : ℕ} → (ρ : AList m m) → (σ : AList m m) → (sub (ρ ⊹⊹ σ)) ≐ ((sub ρ) ◇ (sub ρ))
fact10 anil anil = λ x → refl
fact10 anil (r asnoc t' / x) = λ x₁ → (sub ▹ {!!})
fact10 (p asnoc t' / x) anil = λ x₁ → {!!}
fact10 (p asnoc t' / x) (r asnoc t'' / x₁) = λ x₂ → {!!}

data ∃' {S : Set} (T : S → Set) : Set where
  ⟪_,_⟫ : (s : S) → (t : T s) →  ∃' T

_asnoc'_/_ : {m : ℕ} → (a : ∃' (AList m)) → (t' : Term m) → (x : Fin (suc m)) → ∃' (AList (suc m))
⟪ s , t ⟫ asnoc' t' / x = ⟪ s , t asnoc t' / x ⟫

data AList' : ℕ →  Set where
  anil' : {m : ℕ} → AList' m
  _acons'_/_ : {m : ℕ} → (σ : AList' m) → (t' : Term m) → (x : Fin (suc m)) → AList' (suc m)

targ : {m : ℕ} → (σ : AList' m) → ℕ
targ {m} anil' = m
targ (a acons' t' / x) = targ a

sub' : {m : ℕ} →  (σ : AList' m) → (Fin m → Term (targ σ))
sub' anil' = ι
sub' (σ acons' t' / x) =  (sub' σ) ◇ (t' for x)

⊹⊹' : {m : ℕ} → (σ : AList' m) → (ρ : AList' (targ σ)) → AList' m
⊹⊹' anil' ρ = ρ
⊹⊹' (alist acons' t' / x)  ρ = (⊹⊹' alist ρ) acons' t' / x

---------------------------------------------------------------------------
-- p14

flexFlex : {m : ℕ} → (x y : Fin m) → (∃' (AList m))
flexFlex {suc m} x y with thick x y 
flexFlex {suc m} x y | no = ⟪ (suc m) , anil ⟫
flexFlex {suc m} x y | yes y' = ⟪ m , anil asnoc (ι y') / x ⟫
flexFlex {zero} () y

flexRigid : {m : ℕ} → (x : Fin m) → (t : Term m) → Maybe (∃' (AList m))
flexRigid {zero} () t
flexRigid {suc m} x t with check x t
flexRigid {suc m} x t | no = no
flexRigid {suc m} x t | yes t' = yes ⟪ m , (anil asnoc t' / x) ⟫

amgu : {m : ℕ} → (s t : Term m) → (acc : ∃' (AList m)) →  Maybe (∃' (AList m))
amgu {suc m} s t ⟪ n , σ asnoc r / z ⟫ = lrf (λ σ₁ → σ₁ asnoc' r / z) (amgu {m} ((r for z) ◃ s) ((r for z) ◃ t) ⟪ n , σ ⟫)
amgu leaf leaf acc = yes acc
amgu leaf (t fork t₁) acc = no
amgu (ι x) (ι x₁) ⟪ s , anil ⟫ = yes (flexFlex x x₁)
amgu t (ι x) acc = flexRigid x t
amgu (ι x) t acc = flexRigid x t
amgu (s fork s₁) leaf acc = no
amgu {m} (s fork s₁) (t fork t₁) acc = rf (amgu {m} s₁ t₁) (amgu {m} s t acc)

mgu : {m : ℕ} → (s t : Term m) → Maybe (∃' (AList m))
mgu {m} s t = amgu {m} s t ⟪ m , anil ⟫