Skip to content

Commit 112f9d3

Browse files
author
geruge
committed
first commit
0 parents  commit 112f9d3

File tree

4 files changed

+547
-0
lines changed

4 files changed

+547
-0
lines changed

‎.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
*.agdai
2+
*.mli

‎Unification/FUSR.agda

Lines changed: 224 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,224 @@
1+
module FUSR where
2+
open import Relation.Binary.PropositionalEquality
3+
open Relation.Binary.PropositionalEquality.≡-Reasoning
4+
open import Data.Nat
5+
open import Data.Product
6+
open import Data.Empty
7+
open import Data.Fin
8+
open import Data.Sum
9+
open import Data.Bool
10+
import Level
11+
---------------------------------------------------------------
12+
13+
--p3
14+
15+
data Maybe (A : Set) : Set where
16+
no : Maybe A
17+
yes : A → Maybe A
18+
19+
--p4
20+
21+
lf : {S T : Set} → (f : S → T) → (S → Maybe T)
22+
lf f = λ x → yes (f x)
23+
rf : {S T : Set} → (f : S → Maybe T) → (Maybe S → Maybe T)
24+
rf f no = no
25+
rf f (yes x) = f x
26+
lrf :{S T : Set} → (f : S → T) → (Maybe S → Maybe T)
27+
lrf f = rf (lf f)
28+
_∘_ : {A B C : Set} → (f : B → C) → (g : A → B) → (A → C)
29+
f ∘ g = λ x → f (g x)
30+
31+
lf2 : {R S T : Set} → (f : R → S → T) → (R → S → Maybe T)
32+
lf2 f = λ x x₁ → yes (f x x₁)
33+
34+
rf2 : {R S T : Set} → (f : R → S → Maybe T) → (R → Maybe S → Maybe T)
35+
rf2 f x no = no
36+
rf2 f x (yes x₁) = f x x₁
37+
38+
cf2 : {R S T : Set} → (f : R → Maybe S → Maybe T) → (Maybe R → Maybe S → Maybe T)
39+
cf2 f no no = no
40+
cf2 f no (yes x) = no
41+
cf2 f (yes x) no = f x no
42+
cf2 f (yes x) (yes x₁) = f x (yes x₁)
43+
44+
lrf2 : {R S T : Set} → (f : R → S → T) → (Maybe R → Maybe S → Maybe T)
45+
lrf2 f = cf2 (rf2 (lf2 f))
46+
47+
-- p5
48+
49+
record ⊤ : Set where
50+
51+
empty : Fin zero → Set
52+
empty x = ⊤
53+
54+
55+
Fin' : ℕ → Set
56+
Fin' zero = ⊥
57+
Fin' (suc n) = Maybe (Fin' n)
58+
59+
open import Data.List
60+
61+
revapp : {T : Set} → (xs ys : List T) → List T
62+
revapp [] ys = ys
63+
revapp (x ∷ xs) ys = revapp xs (x ∷ ys)
64+
65+
ack : (m n : ℕ) → ℕ
66+
ack zero n = suc n
67+
ack (suc m) zero = ack m (suc zero)
68+
ack (suc m) (suc n) = ack m (ack (suc m) n)
69+
70+
-- Chap 3
71+
-- p8
72+
73+
data Term (n : ℕ) : Set where
74+
ι : (x : Fin n) → Term n -- 変数 (de bruijn index)
75+
leaf : Term n -- base case の型
76+
_fork_ : (s t : Term n) → Term n -- arrow 型
77+
78+
▹ : {n m : ℕ} → (r : Fin m → Fin n) → (Fin m → Term n)
79+
▹ r = ι ∘ r
80+
81+
_◃_ : {n m : ℕ} → (f : Fin m → Term n) → (Term m → Term n)
82+
_◃_ f (ι x) = f x
83+
_◃_ f leaf = leaf
84+
_◃_ f (s fork t) = (f ◃ s) fork (f ◃ t)
85+
86+
_◃ : {n m : ℕ} → (f : Fin m → Term n) → (Term m → Term n)
87+
f ◃ = λ x → f ◃ x
88+
89+
▹◃ : {n m : ℕ} → (f : Fin m → Fin n) → (Term m → Term n)
90+
▹◃ f = (▹ f) ◃
91+
92+
_≐_ : {n m : ℕ} → (f g : Fin m → Term n) → Set
93+
_≐_ {n} {m} f g = (x : Fin m) → f x ≡ g x
94+
95+
_◇_ : {m n l : ℕ} → (f : Fin m → Term n) → (g : Fin l → Term m) → (Fin l → Term n)
96+
f ◇ g = (f ◃) ∘ g
97+
98+
-- (ι s) fork (ι t) ⇒ ι (s fork t) = s fork t
99+
-- ι s = s
100+
-- ι t = t
101+
-- p9
102+
103+
thin : {n : ℕ} → Fin (suc n) → Fin n → Fin (suc n) -- thin <-> thick
104+
thin {n} zero y = suc y
105+
thin {suc n} (suc x) zero = zero
106+
thin {suc n} (suc x) (suc y) = suc (thin x y)
107+
108+
109+
thick : {n : ℕ} → (x y : Fin (suc n)) → Maybe (Fin n)
110+
thick {n} zero zero = no
111+
thick {n} zero (suc y) = yes y
112+
thick {zero} (suc ()) zero
113+
thick {suc n} (suc x) zero = yes zero
114+
thick {zero} (suc ()) (suc y)
115+
thick {suc n} (suc x) (suc y) = lrf suc (thick {n} x y)
116+
117+
check : {n : ℕ} → Fin (suc n) → Term (suc n) → Maybe (Term n)
118+
check x (ι y) = lrf ι (thick x y)
119+
check x leaf = yes leaf
120+
check x (s fork t) = lrf2 _fork_ (check x s) (check x t)
121+
122+
_for_ : {n : ℕ} → (t' : Term n) → (x : Fin (suc n)) → (Fin (suc n) → Term n)
123+
_for_ t' x y with thick x y
124+
_for_ t' x y | no = t'
125+
_for_ t' x y | yes y' = ι y'
126+
127+
--- P.11
128+
data AList : ℕ → ℕ → Set where
129+
anil : {m : ℕ} → AList m m
130+
_asnoc_/_ : {m : ℕ} {n : ℕ} → (σ : AList m n) → (t' : Term m) → (x : Fin (suc m)) → AList (suc m) n
131+
--snoc : consの逆 []::2 ::3 :: ...
132+
133+
--_◇_ : {m n l : ℕ} → (f : Fin m → Term n) → (g : Fin l → Term m) → (Fin l → Term n)
134+
sub : {m n : ℕ} → (σ : AList m n) → Fin m → Term n
135+
sub anil = ι --m≡nなら何もしない
136+
sub (σ asnoc t' / x) = (sub σ) ◇ (t' for x)
137+
138+
_⊹⊹_ : {l m n : ℕ} → (ρ : AList m n) → (σ : AList l m) → AList l n
139+
ρ ⊹⊹ anil = ρ
140+
ρ ⊹⊹ (alist asnoc t / x) = (ρ ⊹⊹ alist) asnoc t / x
141+
-- ∃(λx : S.T)
142+
data ∃' {S : Set} (T : S → Set) : Set where
143+
⟪_,_⟫ : (s : S) → (t : T s) → ∃' T
144+
145+
_asnoc'_/_ : {m : ℕ} → (a : ∃' (AList m)) → (t' : Term m) → (x : Fin (suc m)) → ∃' (AList (suc m))
146+
⟪ s , t ⟫ asnoc' t' / x = ⟪ s , t asnoc t' / x ⟫
147+
148+
data AList' : ℕ → Set where
149+
anil' : {m : ℕ} → AList' m
150+
_acons'_/_ : {m : ℕ} → (σ : AList' m) → (t' : Term m) → (x : Fin (suc m)) → AList' (suc m)
151+
152+
targ : {m : ℕ} → (σ : AList' m) → ℕ
153+
targ {m} anil' = m
154+
targ (a acons' t' / x) = targ a
155+
156+
_⊹⊹'_ : {m : ℕ} → (σ : AList' m) → (ρ : AList' (targ σ)) → AList' m
157+
_⊹⊹'_ anil' ρ = ρ
158+
_⊹⊹'_ (alist acons' t' / x) ρ = (_⊹⊹'_ alist ρ) acons' t' / x
159+
160+
161+
162+
163+
sub' : {m : ℕ} → (σ : AList' m) → (Fin m → Term (targ σ))
164+
sub' anil' = ι
165+
sub' (σ acons' t' / x) = (sub' σ) ◇ (t' for x)
166+
167+
168+
-- p14
169+
170+
flexFlex : {m : ℕ} → (x y : Fin m) → (∃' (AList m))
171+
flexFlex {suc m} x y with thick x y
172+
flexFlex {suc m} x y | no = ⟪ (suc m) , anil ⟫
173+
flexFlex {suc m} x y | yes y' = ⟪ m , anil asnoc (ι y') / x ⟫
174+
flexFlex {zero} () y
175+
176+
flexRigid : {m : ℕ} → (x : Fin m) → (t : Term m) → Maybe (∃' (AList m))
177+
flexRigid {zero} () t
178+
flexRigid {suc m} x t with check x t
179+
flexRigid {suc m} x t | no = no
180+
flexRigid {suc m} x t | yes t' = yes ⟪ m , (anil asnoc t' / x) ⟫
181+
182+
amgu : {m : ℕ} → (s t : Term m) → (acc : ∃' (AList m)) → Maybe (∃' (AList m))
183+
amgu {suc m} s t ⟪ n , σ asnoc r / z ⟫ = lrf (λ σ₁ → σ₁ asnoc' r / z) (amgu {m} ((r for z) ◃ s) ((r for z) ◃ t) ⟪ n , σ ⟫)
184+
amgu leaf leaf acc = yes acc
185+
amgu leaf (t fork t₁) acc = no
186+
amgu (ι x) (ι x₁) ⟪ s , anil ⟫ = yes (flexFlex x x₁)
187+
amgu t (ι x) acc = flexRigid x t
188+
amgu (ι x) t acc = flexRigid x t
189+
amgu (s fork s₁) leaf acc = no
190+
amgu {m} (s fork s₁) (t fork t₁) acc = rf (amgu {m} s₁ t₁) (amgu {m} s t acc)
191+
192+
mgu : {m : ℕ} → (s t : Term m) → Maybe (∃' (AList m))
193+
mgu {m} s t = amgu {m} s t ⟪ m , anil ⟫
194+
195+
196+
-- test
197+
198+
t1 : Term 4
199+
t1 = (ι zero) fork (ι zero)
200+
201+
t2 : Term 4
202+
t2 = ((ι (suc zero)) fork (ι (suc (suc zero)))) fork (ι (suc (suc (suc zero))))
203+
204+
u12 : Maybe (∃' (AList 4))
205+
u12 = (mgu t1 t2)
206+
207+
--u12 ≡ yes
208+
--⟪ 2 ,
209+
--(anil asnoc ι zero fork ι (suc zero) / suc (suc zero)) asnoc
210+
--ι zero fork ι (suc zero) / zero
211+
--⟫
212+
-- (1 → 2) → 3
213+
-- 0が無いので
214+
-- 数字がずれて
215+
-- (0 → 1) → 2
216+
-- (0 → 1) → (0 → 1)
217+
218+
-- unifyできない例
219+
220+
t3 : Term 4
221+
t3 = ((ι zero) fork (ι (suc (suc zero)))) fork (ι (suc (suc (suc zero))))
222+
223+
u13 : Maybe (∃' (AList 4))
224+
u13 = (mgu t1 t3)

‎Unification/facts.agda

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
module facts where
2+
open import FUSR
3+
open import Relation.Binary.PropositionalEquality
4+
open Relation.Binary.PropositionalEquality.≡-Reasoning
5+
open import Data.Nat
6+
open import Data.Product
7+
open import Data.Empty
8+
open import Data.Fin
9+
open import Data.Sum
10+
open import Data.Bool
11+
import Level
12+
13+
-------------------------------------------
14+
15+
fact : {S T R : Set} → ∀(f : S → Maybe T) → ∀ (g : R → S) → ∀ (s : Maybe R) → rf (f ∘ g) s ≡ (rf f ∘ lrf g) s
16+
fact f g no = refl
17+
fact f g (yes x) = refl
18+
19+
fact2 : {n : ℕ} → (t : Term n) → (ι ◃ t ≡ t)
20+
fact2 (ι x) = refl
21+
fact2 leaf = refl
22+
fact2 (s fork t) = cong₂ _fork_ (fact2 s) (fact2 t)
23+
24+
fact3 : {l m n : ℕ} → (f : Fin m → Term n) → (g : Fin l → Term m) → (t : Term l)
25+
→ (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
26+
fact3 f g (ι x) = refl
27+
fact3 f g leaf = refl
28+
fact3 f g (t fork t₁) = cong₂ _fork_ (fact3 f g t) (fact3 f g t₁)
29+
30+
fact4 : {l m n : ℕ} → (f : Fin m → Term n) → (r : Fin l → Fin m) → ((f ◇ (▹ r)) ≐ (f ∘ r))
31+
fact4 = λ f r x → refl
32+
33+
-- suc a ≡ suc b → a ≡ b
34+
lemma1 : {n : ℕ} → (a b : Fin n) → (_≡_ {_} {Fin (suc n)} (suc a) (suc b)) → a ≡ b
35+
lemma1 .b b refl = refl
36+
37+
fact5 : {n : ℕ} → (x : Fin (suc n)) → (y : Fin n) → (z : Fin n) → thin x y ≡ thin x z → y ≡ z
38+
fact5 zero zero zero a = refl
39+
fact5 zero zero (suc z) ()
40+
fact5 zero (suc y) .(suc y) refl = refl
41+
fact5 (suc x) zero zero a = refl
42+
fact5 (suc x) zero (suc z) ()
43+
fact5 (suc x) (suc y) zero ()
44+
fact5 (suc x) (suc y) (suc z) a = cong suc (fact5 x y z (lemma1 (thin x y) (thin x z) a))
45+
46+
fact6 : {n : ℕ} → (x : Fin (suc n)) → (y : Fin n) → ((thin x y ≡ x) → ⊥)
47+
fact6 zero zero ()
48+
-- a : suc zero ≡ zero
49+
fact6 zero (suc y) ()
50+
fact6 (suc x) zero ()
51+
fact6 (suc x) (suc y) a = fact6 x y (lemma1 (thin x y) x a)
52+
53+
fact7 : {n : ℕ} → (x y : Fin (suc n)) → (x ≡ y → ⊥) → Σ[ y' ∈ Fin n ] (thin x y' ≡ y)
54+
fact7 zero zero a = ⊥-elim (a refl)
55+
fact7 zero (suc y) a = y , refl
56+
fact7 {zero} (suc ()) zero a
57+
fact7 {suc n} (suc x) zero a = zero , refl
58+
fact7 {zero} (suc ()) (suc y) a
59+
fact7 {suc n} (suc x) (suc y) a with fact7 x y (λ x₁ → a (cong suc x₁))
60+
fact7 {suc n} (suc x) (suc y) a | y' , p = (suc y') , cong suc p
61+
62+
lemma2 : {n : ℕ} → (x : Fin (suc n)) → (y : Fin (suc n)) → (((y ≡ x) × (thick x y) ≡ no) ⊎ (Σ[ y' ∈ Fin n ] y ≡ (thin x y') × ((thick x y) ≡ yes y') ))
63+
lemma2 zero zero = inj₁ (refl , refl)
64+
lemma2 zero (suc y) = inj₂ (y , (refl , refl))
65+
lemma2 {zero} (suc ()) zero
66+
lemma2 {suc n} (suc x) zero = inj₂ (zero , (refl , refl))
67+
lemma2 {zero} (suc ()) (suc y)
68+
lemma2 {suc n} (suc x) (suc y) with lemma2 x y
69+
lemma2 {suc n} (suc x) (suc .x) | inj₁ (refl , thickxx≡no) = inj₁ (refl , cong (λ (a : Maybe (Fin n)) → rf (λ x₁ → yes (suc x₁)) a) thickxx≡no)
70+
lemma2 {suc n} (suc x) (suc y) | inj₂ (y' , proj₂ , proj₃) = inj₂ (suc y' , (cong suc proj₂ , cong (λ a → rf (λ x₁ → yes (suc x₁)) a) proj₃))
71+
72+
fact8 : {n : ℕ} → (x : Fin (suc n)) → (y : Fin (suc n)) → (r : Maybe (Fin n)) → (r ≡ thick x y) → (((y ≡ x) × r ≡ no) ⊎ (Σ[ y' ∈ Fin n ] y ≡ (thin x y') × (r ≡ yes y') ))
73+
fact8 x y .(thick x y) refl = lemma2 x y
74+
75+
fact9 : {n : ℕ} → (t' : Term n) → (x : Fin (suc n)) → ((_for_ t' x) ∘ thin x) ≐ ι
76+
fact9 {n} t' x y with lemma2 x (thin x y)
77+
fact9 t' x y | inj₁ (proj₁ , proj₂) with fact6 x y proj₁
78+
fact9 t' x y | inj₁ (proj₁ , proj₂) | ()
79+
fact9 t' x y | inj₂ (proj₁ , proj₂ , proj₃) with fact5 x y proj₁ proj₂
80+
fact9 t' x .proj₁ | inj₂ (proj₁ , proj₂ , proj₃) | refl rewrite proj₃ = refl
81+
82+
lemma3 : {n : ℕ} → (f : Fin n → Fin (suc n)) → (t : Term n) → (g : Fin (suc n) → Term n) → g ◃ (▹ f ◃ t) ≡ (g ∘ f) ◃ t
83+
lemma3 f (ι x) g = refl
84+
lemma3 f leaf g = refl
85+
lemma3 f (t fork t₁) g = cong₂ (λ x x₁ → x fork x₁) (lemma3 f t g) (lemma3 f t₁ g)
86+
87+
lemma6 : {m n : ℕ} → (f : Fin m → Term n) →(g : Fin m → Term n) → (t' : Term m) → (f ≐ g) → (f ◃ t' ≡ g ◃ t')
88+
lemma6 f g (ι x) = λ x₁ → x₁ x
89+
lemma6 f g leaf = λ x → refl
90+
lemma6 f g (t' fork t'') = λ x → cong₂ (λ x₁ x₂ → x₁ fork x₂) (lemma6 f g t' x) (lemma6 f g t'' x)
91+
92+
--((_for_ t' x) ∘ thin x) ≐ ι
93+
lemma4 : {n : ℕ} → (t' : Term n) → (x : Fin (suc n)) → ((_for_ t' x) ∘ thin x) ◃ t' ≡ t'
94+
lemma4 t' x = begin
95+
((_for_ t' x) ∘ thin x) ◃ t'
96+
≡⟨ lemma6 ((t' for x) ∘ thin x) ι t' (fact9 t' x) ⟩
97+
ι ◃ t'
98+
≡⟨ fact2 t' ⟩
99+
t'
100+
∎
101+
lemma7 : {n : ℕ} → (x : Fin (suc n)) → ((thick x x) ≡ no)
102+
lemma7 zero = refl
103+
lemma7 {zero} (suc ())
104+
lemma7 {suc n} (suc x) = cong (rf (λ x₁ → yes (suc x₁))) (lemma7 x)
105+
--rf (λ x₁ → yes (suc x₁)) (thick x x) ≡ no
106+
107+
lemma5 : {n : ℕ} → (t' : Term n) → (x : Fin (suc n)) → t' ≡ (t' for x) x
108+
lemma5 t' x rewrite lemma7 x = refl
109+
110+
lemma10 : {A : Set} → {a b : A} → (x y : Maybe A) → ((x ≡ y) × (x ≡ yes a) × (y ≡ yes b)) → (a ≡ b)
111+
lemma10 no no (refl , () , proj₃)
112+
lemma10 no (yes x) (proj₁ , () , proj₃)
113+
lemma10 (yes x) no (proj₁ , proj₂ , ())
114+
lemma10 {A} {.b} {b} (yes .b) (yes .b) (refl , refl , refl) = refl
115+
116+
lemma10' : {A : Set} → {a b : A} → ((yes a) ≡ (yes b)) → (a ≡ b)
117+
lemma10' refl = refl
118+
119+
lemma11 : {A : Set} → {x : A} → (a b : Maybe A) → (f : A → A → A) → ((lrf2 f) a b ≡ yes x) → Σ[ p' ∈ A ] Σ[ q' ∈ A ] ((a ≡ yes p') × (b ≡ yes q'))
120+
lemma11 no no f ()
121+
lemma11 no (yes x₁) f ()
122+
lemma11 (yes x₁) no f ()
123+
lemma11 (yes p') (yes q') f refl = p' , q' , refl , refl
124+
125+
lemma8 : {n : ℕ} → (x : Fin (suc n)) → (t : Term (suc n)) → (t' : Term n) → (check x t ≡ yes t') → (t ≡ (▹ (thin x) ◃ t'))
126+
lemma8 x (ι y) t' p with lemma2 x y
127+
lemma8 x (ι .x) t' p | inj₁ (refl , proj₂) rewrite proj₂ with p
128+
... | ()
129+
lemma8 x (ι y) t' p | inj₂ (y' , proj₁ , proj₂) rewrite proj₂ with lemma10' p
130+
... | a rewrite (sym a) | proj₁ = refl
131+
lemma8 x leaf .leaf refl = refl
132+
lemma8 x (t fork t₁) t' p with lemma11 (check x t) (check x t₁) (_fork_) p
133+
lemma8 x (s₁ fork s₂) t' p | s₁' , s₂' , proj₃ , proj₄
134+
with lemma8 x s₁ s₁' proj₃ | lemma8 x s₂ s₂' proj₄
135+
... | a | b rewrite proj₃ | proj₄ with lemma10' p
136+
... | c rewrite (sym c) = cong₂ _fork_ a b
137+
138+
fact10 :{n : ℕ} → (x : Fin (suc n)) → (t : Term (suc n)) → (t' : Term n) → (check x t ≡ yes t') → (t' for x) ◃ t ≡ (t' for x) x
139+
fact10 {n} x t t' p = begin
140+
(t' for x) ◃ t
141+
≡⟨ cong (λ (x₁ : Term (suc n)) → (t' for x) ◃ x₁) (lemma8 x t t' p) ⟩
142+
(t' for x) ◃ (▹ (thin x) ◃ t')
143+
≡⟨ lemma3 (thin x) t' (t' for x) ⟩
144+
((t' for x) ∘ thin x) ◃ t'
145+
≡⟨ lemma4 t' x ⟩
146+
t'
147+
≡⟨ lemma5 t' x ⟩
148+
(t' for x) x
149+
∎
150+
151+
--postulate
152+
-- ext : {A B : Set} → (f g : (A → B)) → {x : A} → (f x ≡ g x) → (f ≡ g)
153+
-- thick x p で場合分けすると、証明する式が簡単になる。
154+
-- さらに t' で場合分けをすると ext が必要そうだったところが、引数が渡
155+
-- される形になって ext なしで証明できるようになる。
156+
-- でも、その中で t' に関する再帰が必要になるので、それを別途、相互再帰
157+
-- させて証明する。
158+
159+
mutual
160+
fact11 : {m n l : ℕ} → (ρ : AList m n) → (σ : AList l m) → (sub (ρ ⊹⊹ σ)) ≐ ((sub ρ) ◇ (sub σ))
161+
fact11 ρ anil p = refl
162+
fact11 ρ (σ asnoc t' / x) p with thick x p
163+
fact11 ρ (σ asnoc t' / x) p | no = fact11' ρ σ t'
164+
fact11 ρ (σ asnoc t' / x) p | yes y = fact11 ρ σ y
165+
166+
fact11' : {m n l : ℕ} → (ρ : AList m n) → (σ : AList l m) → (t : Term l) → (sub (ρ ⊹⊹ σ) ◃ t) ≡ sub ρ ◃ (sub σ ◃ t)
167+
fact11' ρ σ (ι x) = fact11 ρ σ x
168+
fact11' ρ σ leaf = refl
169+
fact11' ρ σ (t1 fork t2) = cong₂ _fork_ (fact11' ρ σ t1) (fact11' ρ σ t2)

0 commit comments

Comments
 (0)