Mercurial > hg > Members > kono > Proof > category

annotate deductive.agda @ 829:6c5cfb9b333e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix deduction theorem
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 Jul 2019 00:18:17 +0900
parents 82a8c1ab4ef5
children 232cea484067
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
829
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
30 i : {b c : Obj A} {k : Hom A b c } → φ x k
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
31 ii : φ x {⊤} {a} x
798
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 >
829
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
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 )
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
34 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * )
798
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
829
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
41 k : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → Hom A (a ∧ b) c
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
42 k x∈a {k} i = k ・ π'
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
43 k x∈a ii = π
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
44 k x∈a (iii ψ χ ) = < k x∈a ψ , k x∈a χ >
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
45 k x∈a (iv ψ χ ) = k x∈a ψ ・ < π , k x∈a χ >
6c5cfb9b333e fix deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
46 k x∈a (v ψ ) = ( k x∈a ψ ・ α ) *