Mercurial > hg > Members > kono > Proof > FirstOrder

comparison Logic.agda @ 18:6cd5b63ecc38

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replace syntax
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Aug 2020 13:34:12 +0900
parents 2f4db56bb289
children 55a0d814fce7
comparison
equal deleted inserted replaced
17:76e933149151 18:6cd5b63ecc38
1 module Logic (Const Func Var Pred : Set) where 1 module Logic (Const Func Var Pred : Set) where
2 open import Data.List hiding (all ; and ; or ) 2 open import Data.List hiding (all ; and ; or )
3 open import Data.Bool hiding ( not ; _∧_ ; _∨_ ) 3 open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
4 4
5 data Expr : Set where 5 data Expr : Set where
6 var : Var → Expr 6 var : Var → Expr
7 func : Func → Expr → Expr 7 func : Func → Expr → Expr
8 const : Const → Expr 8 const : Const → Expr
9 _,_ : Expr → Expr → Expr 9 _,_ : Expr → Expr → Expr
10 10
11 data Statement : Set where 11 data Statement : Set where
12 pred : Pred → Statement 12 pred : Pred → Statement
13 predx : Pred → Expr → Statement 13 predx : Pred → Expr → Statement
14 _∧_ : Statement → Statement → Statement 14 _∧_ : Statement → Statement → Statement
15 _∨_ : Statement → Statement → Statement 15 _∨_ : Statement → Statement → Statement
16 ¬_ : Statement → Statement 16 ¬_ : Statement → Statement
17 All_=>_ : Var → Statement → Statement 17 All_=>_ : Var → Statement → Statement
18 Exist_=>_ : Var → Statement → Statement 18 Exist_=>_ : Var → Statement → Statement
19
20 -- Exprindepenent variable substituion using dependent substution (sbst)
21 subst-prop : (e : Statement ) → (sbst : Expr → Var → Expr → Expr ) → Var → Expr → Statement
22 subst-prop (pred x) sbst xv v = pred x
23 subst-prop (predx x x₁) sbst xv v = predx x ( sbst x₁ xv v )
24 subst-prop (e ∧ e₁) sbst xv v = ( subst-prop e sbst xv v ) ∧ ( subst-prop e₁ sbst xv v )
25 subst-prop (e ∨ e₁) sbst xv v = ( subst-prop e sbst xv v ) ∨ ( subst-prop e₁ sbst xv v )
26 subst-prop (¬ e) sbst xv v = ¬ ( subst-prop e sbst xv v )
27 subst-prop (All x => e) sbst xv v = All x => ( subst-prop e sbst xv v )
28 subst-prop (Exist x => e) sbst xv v = Exist x => ( subst-prop e sbst xv v )
29 19
30 -- 20 --
31 -- The interpretation 21 -- The interpretation
32 -- all-const is a list of all possible arguments of predicates (possibly infinite) 22 -- all-const is a list of all possible arguments of predicates (possibly infinite)
33 -- sbst is an Expr depenent variable substituion 23 -- sbst is an Expr depenent variable substituion
34 -- 24 --
35 {-# TERMINATING #-} 25 {-# TERMINATING #-}
36 M : (amap : Pred → Bool ) (pmap : Pred → Expr → Bool ) 26 M : (amap : Pred → Bool ) (pmap : Pred → Expr → Bool )
37 → (all-const : List Expr ) 27 → (all-const : List Expr )
38 → (sbst : Expr → Var → Expr → Expr ) 28 → (sbst : Expr → Var → Expr → Expr )
39 → Statement → Bool 29 → Statement → Bool
40 M amap pmap all0 sbst s = m s where 30 M amap pmap all0 sbst s = m s where
31
32 -- Expr indepenent variable substituion using Expr substution (sbst)
33 _[_/_] : (e : Statement ) → Var → Expr → Statement
34 (pred x) [ xv / v ] = pred x
35 (predx x x₁) [ xv / v ] = predx x ( sbst x₁ xv v )
36 (e ∧ e₁) [ xv / v ] = ( e [ xv / v ]) ∧ ( e₁ [ xv / v ])
37 (e ∨ e₁) [ xv / v ] = ( e [ xv / v ]) ∨ ( e₁ [ xv / v ])
38 (¬ e) [ xv / v ] = ¬ ( e [ xv / v ])
39 (All x => e) [ xv / v ] = All x => ( e [ xv / v ])
40 (Exist x => e) [ xv / v ] = Exist x => ( e [ xv / v ])
41
41 m : Statement → Bool 42 m : Statement → Bool
42 m (pred x) = amap x 43 m (pred x) = amap x
43 m (predx x x₁) = pmap x x₁ 44 m (predx x x₁) = pmap x x₁
44 m (s ∧ s₁) = m s Data.Bool.∧ m s₁ 45 m (s ∧ s₁) = m s Data.Bool.∧ m s₁
45 m (s ∨ s₁) = m s Data.Bool.∨ m s₁ 46 m (s ∨ s₁) = m s Data.Bool.∨ m s₁
46 m (¬ s) = Data.Bool.not (m s ) 47 m (¬ s) = Data.Bool.not (m s )
48 -- an esasy emulation of quantifier using a variable free expr list
47 m (All x => s) = m-all all0 x s where 49 m (All x => s) = m-all all0 x s where
48 m-all : List Expr → Var → Statement → Bool 50 m-all : List Expr → Var → Statement → Bool
49 m-all [] vx s = true 51 m-all [] vx s = true
50 m-all (x ∷ t) vx s = m (subst-prop s sbst vx x ) Data.Bool.∧ m-all t vx s 52 m-all (x ∷ t) vx s = m ( s [ vx / x ]) Data.Bool.∧ m-all t vx s
51 m (Exist x => s) = m-exist all0 x s where 53 m (Exist x => s) = m-exist all0 x s where
52 m-exist : List Expr → Var → Statement → Bool 54 m-exist : List Expr → Var → Statement → Bool
53 m-exist [] vx s = false 55 m-exist [] vx s = false
54 m-exist (x ∷ t) vx s = m (subst-prop s sbst vx x ) Data.Bool.∨ m-exist t vx s 56 m-exist (x ∷ t) vx s = m ( s [ vx / x ] ) Data.Bool.∨ m-exist t vx s
55 57
58