Mercurial > hg > Members > kono > Proof > category

comparison deductive.agda @ 791:376c07159acf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
deduction theorem
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Apr 2019 17:43:01 +0900
parents
children 5bee48f7c126
comparison
equal deleted inserted replaced
790:1e7319868d77 791:376c07159acf
1 module deductive (Atom : Set) where
2
3 -- Deduction Theorem
4
5 -- positive logic ( deductive system based on graph )
6
7 data Obj : Set where
8 ⊤ : Obj
9 atom : Atom → Obj
10 _∧_ : Obj → Obj → Obj
11 _<=_ : Obj → Obj → Obj
12
13 data Arrow : Obj → Obj → Set where
14 hom : (a b : Obj) → Arrow a b
15 id : (a : Obj ) → Arrow a a
16 _・_ : {a b c : Obj } → Arrow b c → Arrow a b → Arrow a c
17 ○ : {a : Obj } → Arrow a ⊤
18 π : {a b : Obj } → Arrow ( a ∧ b ) a
19 π' : {a b : Obj } → Arrow ( a ∧ b ) b
20 <_,_> : {a b c : Obj } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
21 ε : {a b : Obj } → Arrow ((a <= b) ∧ b ) a
22 _* : {a b c : Obj } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
23
24 -- every proof b → c with assumption a has following forms
25
26 data φ {a : Obj} ( x : Arrow ⊤ a ) : {b c : Obj} → Arrow b c → Set where
27 i : {b c : Obj} → φ x ( hom b c )
28 ii : φ x {⊤} {a} x
29 iii : {b c' c'' : Obj } { f : Arrow b c' } { g : Arrow b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x < f , g >
30 iv : {b c d : Obj } { f : Arrow d c } { g : Arrow b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
31 v : {b c' c'' : Obj } { f : Arrow (b ∧ c') c'' } (ψ : φ x f ) → φ x ( f * )
32
33 α : {a b c : Obj } → Arrow (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
34 α = < π ・ π , < π' ・ π , π' > >
35
36 -- genetate (a ∧ b) → c proof from proof b → c with assumption a
37
38 kx∈a : {a b c : Obj } → ( x : Arrow ⊤ a ) → {z : Arrow b c } → ( y : φ {a} x z ) → Arrow (a ∧ b) c
39 kx∈a x {k} i = k ・ π'
40 kx∈a x ii = π
41 kx∈a x (iii ψ χ ) = < kx∈a x ψ , kx∈a x χ >
42 kx∈a x (iv ψ χ ) = kx∈a x ψ ・ < π , kx∈a x χ >
43 kx∈a x (v ψ ) = ( kx∈a x ψ ・ α ) *