Mercurial > hg > Members > kono > Proof > category

annotate deductive.agda @ 799:82a8c1ab4ef5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Apr 2019 11:30:34 +0900
parents 6e6c7ad8ea1c
children 6c5cfb9b333e 8c2da34e8dc1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
1 open import Level
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
2 open import Category
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
3 module deductive {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 -- Deduction Theorem
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
7 -- positive logic
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
9 record PositiveLogic {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
10 field
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
11 ⊤ : Obj A
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
12 ○ : (a : Obj A ) → Hom A a ⊤
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
13 _∧_ : Obj A → Obj A → Obj A
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
14 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
15 π : {a b : Obj A } → Hom A (a ∧ b) a
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
16 π' : {a b : Obj A } → Hom A (a ∧ b) b
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
17 _<=_ : (a b : Obj A ) → Obj A
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
18 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
19 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
20
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
798
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
22 module deduction-theorem ( L : PositiveLogic A ) where
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
798
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
24 open PositiveLogic L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
25 _・_ = _[_o_] A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
26
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
27 -- every proof b → c with assumption a has following forms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
29 data φ {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
30 i : {b c : Obj A} {k : Hom A b c } → φ x k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
31 ii : φ x {⊤} {a} x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
32 iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c' ∧ c''} < f , g >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
33 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
34 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
35
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
36 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
37 α = < π ・ π , < π' ・ π , π' > >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
38
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
39 -- genetate (a ∧ b) → c proof from proof b → c with assumption a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
40
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
41 kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y : φ {a} x z ) → Hom A (a ∧ b) c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
42 kx∈a x {k} i = k ・ π'
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
43 kx∈a x ii = π
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
44 kx∈a x (iii ψ χ ) = < kx∈a x ψ , kx∈a x χ >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
45 kx∈a x (iv ψ χ ) = kx∈a x ψ ・ < π , kx∈a x χ >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 793
diff changeset
46 kx∈a x (v ψ ) = ( kx∈a x ψ ・ α ) *