Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 9:627a6bf54ed5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 13 Aug 2020 15:24:47 +0900
parents 0737e6671061
children edf4a816abff
files Logic.agda example1.agda first-order.agda
diffstat 3 files changed, 186 insertions(+), 215 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Logic.agda	Thu Aug 13 15:24:47 2020 +0900
@@ -0,0 +1,40 @@
+module Logic (Const Func Var Pred : Set)  where
+open import Data.List hiding (all ; and ; or )
+open import Data.Bool hiding ( not )
+
+data Expr  : Set  where
+   var   : Var → Expr 
+   func  : (f : Func ) → Expr → Expr 
+   const : Const → Expr 
+   arg   : Expr → Expr 
+
+data Statement : Set where
+   atom       : Pred  → Statement 
+   predicate  : Pred  → Expr → Statement 
+   and        : Statement → Statement  → Statement 
+   or         : Statement → Statement  → Statement 
+   not        : Statement  → Statement 
+   All        : Var → Statement → Statement 
+   Exist      : Var → Statement → Statement 
+
+{-# TERMINATING #-} 
+M : (amap :  Pred  → Bool ) (pmap :  Pred → Expr → Bool )
+   →  (all-const   : List Expr )
+   →  (subst-prop :  Statement  → Var  → Expr  → Statement  )
+   → Statement  → Bool
+M amap pmap all0 sbst s = m s where
+   m :  Statement  → Bool
+   m (atom x) = amap x
+   m (predicate x x₁) = pmap x x₁
+   m (and s s₁) = m s  ∧ m s₁ 
+   m (or s s₁) = m s ∨ m s₁ 
+   m (not s) = Data.Bool.not (m s )
+   m (All x s) = m-all all0 x s  where
+     m-all :  List Expr → Var → Statement → Bool
+     m-all [] vx s = true
+     m-all (x ∷ t) vx s = m (sbst s vx x ) ∧ m-all t vx s
+   m (Exist x s) = m-exist all0 x s  where
+     m-exist :  List Expr → Var  → Statement → Bool
+     m-exist [] vx s = false
+     m-exist (x ∷ t) vx s = m (sbst s vx x ) ∨ m-exist t vx s
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/example1.agda	Thu Aug 13 15:24:47 2020 +0900
@@ -0,0 +1,146 @@
+module example1 where
+open import Data.List hiding (all ; and ; or )
+open import Data.Maybe 
+open import Data.Bool hiding ( not )
+
+data Term : Set where
+      X : Term
+      Y : Term
+      Z : Term
+      a : Term
+      b : Term
+      c : Term
+      f : Term → Term
+      g : Term → Term
+      h : Term → Term
+      p : Term → Term
+      q : Term
+      r : Term
+      _/\_    : Term → Term → Term
+      _\/_    : Term → Term → Term
+      ¬       : Term → Term 
+      all_=>_ : Term → Term → Term
+      ∃_=>_   : Term → Term → Term
+
+
+data Kind : Set where
+      pred : Kind
+      const : Kind
+      var  : Kind
+      func : Kind
+      arg  : Kind
+      args : Kind
+
+data Kinds : Kind → Set where
+      kX : Kinds var
+      kY : Kinds var
+      kZ : Kinds var
+      ka : Kinds const
+      kb : Kinds const
+      kc : Kinds const
+      kf : Kinds func
+      kg : Kinds func
+      kh : Kinds func
+      kp : Kinds pred
+      kq : Kinds pred
+      kr : Kinds pred
+
+open import Logic (Kinds const) (Kinds func) (Kinds var) (Kinds pred)
+
+ex1 : Term
+ex1 = ¬ ( q  /\ ( all X =>  p ( f  X ) ))
+
+parse-arg : (t : Term ) → Maybe Expr 
+parse-arg  X = just (var kX)
+parse-arg  Y = just (var kY)
+parse-arg  Z = just (var kZ)
+parse-arg  a = just (const ka)
+parse-arg  b = just (const kb)
+parse-arg  c = just (const kc)
+parse-arg (f  x ) with parse-arg x
+parse-arg (f  x ) | just pt = just ( func kf pt )
+parse-arg (f  x ) | nothing = nothing
+parse-arg (g  x ) with parse-arg x
+parse-arg (g  x ) | just pt = just ( func kg pt )
+parse-arg (g  x ) | nothing = nothing
+parse-arg (h  x ) with parse-arg x
+parse-arg (h  x ) | just pt = just ( func kh pt )
+parse-arg (h  x ) | nothing = nothing
+parse-arg _ = nothing
+
+parse : (t : Term ) → Maybe Statement 
+parse q = just ( atom kq )
+parse r = just ( atom kr )
+parse (p  x ) with parse-arg x
+parse (p  x ) | just y = just ( predicate kp y )
+parse (p  x ) | nothing = nothing
+parse (t /\ t₁) with parse t | parse t₁
+parse (t /\ t₁) | just p₁ | just p₂ = just ( and p₁ p₂ )
+parse (t /\ t₁) | _ | _ = nothing
+parse (t \/ t₁) with parse t | parse t₁
+parse (t \/ t₁) | just p₁ | just p₂ = just ( or p₁ p₂ )
+parse (t \/ t₁) | _ | _ = nothing
+parse (¬ t)  with parse t 
+parse (¬ t)  | just tx = just ( not tx )
+parse (¬ t)  | _ = nothing
+parse (all X => t₁) with parse t₁
+... | just tx = just ( All kX tx )
+... | _ = nothing
+parse (all Y => t₁) with parse t₁
+... | just tx = just ( All kY tx )
+... | _ = nothing
+parse (all Z => t₁) with parse t₁
+... | just tx = just ( All kZ tx )
+... | _ = nothing
+parse (∃ X => t₁) with parse t₁
+... | just tx = just ( Exist kX tx )
+... | _ = nothing
+parse (∃ Y => t₁) with parse t₁
+... | just tx = just ( Exist kY tx )
+... | _ = nothing
+parse (∃ Z => t₁) with parse t₁
+... | just tx = just ( Exist kZ tx)
+... | _ = nothing
+parse _ = nothing
+
+ex2 = parse ex1
+
+subst-expr :  Expr  → Kinds var → (value : Expr ) → Expr 
+subst-expr  (var kX) kX v = v
+subst-expr  (var kY) kX v = var kY
+subst-expr  (var kZ) kX v = var kZ
+subst-expr  (var kX) kY v = var kX
+subst-expr  (var kY) kY v = v
+subst-expr  (var kZ) kY v = var kZ
+subst-expr  (var kX) kZ v = var kX
+subst-expr  (var kY) kZ v = var kY
+subst-expr  (var kZ) kZ v = v
+subst-expr  (func f₁ e) xv v = func f₁ ( subst-expr e xv v ) 
+subst-expr  (const x₁) xv v = (const x₁)
+subst-expr  (arg e ) xv v = arg ( subst-expr e xv v ) 
+
+subst-prop :  (e : Statement  ) → Kinds var → (value : Expr ) → Statement 
+subst-prop (atom x) xv v = atom x
+subst-prop (predicate x x₁) xv v = predicate x ( subst-expr x₁ xv v )
+subst-prop (and e e₁) xv v = and ( subst-prop e xv v ) ( subst-prop e₁ xv v )
+subst-prop (or e e₁) xv v =  or ( subst-prop e xv v ) ( subst-prop e₁ xv v )
+subst-prop (not e) xv v = not ( subst-prop e xv v )
+subst-prop (All x e) xv v = All x ( subst-prop e xv v )
+subst-prop (Exist x e) xv v = Exist x ( subst-prop e xv v )
+
+amap : (px :  Kinds pred ) → Bool 
+amap kq = true
+amap px = false
+pmap : (px :  Kinds pred ) → Expr → Bool 
+pmap kp (const kc) = true
+pmap px _ = false
+
+-- we only try simple constant, it may contains arbitrary complex functional value
+all0   :  List Expr
+all0 =  const ka ∷ const kb ∷ const kc ∷ []
+
+test003 : Bool 
+test003 with parse ( ∃ X =>  p  X  )
+test003 | just x = M amap pmap all0 subst-prop x
+test003 | nothing = false
+
--- a/first-order.agda	Thu Aug 13 12:50:30 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,215 +0,0 @@
-module first-order where
-open import Data.List hiding (all ; and ; or )
-open import Data.Maybe 
-open import Data.Bool hiding ( not )
-open import Relation.Nullary hiding (¬_)
-open import Relation.Binary.PropositionalEquality hiding ( [_] )
-
-module Logic (Term : Set ) (Const Func Var Pred : Term → Set)  where
-
-  data Expr  : Set  where
-     var   : {v : Term } → Var v → Expr 
-     func  : {x : Term }  → (f : Func x) → Expr → Expr 
-     const : {c : Term } → Const c → Expr 
-     args : Expr → Expr  → Expr 
-
-  data Statement : Set where
-     atom       : {x : Term } → Pred x → Statement 
-     predicate  : {p : Term }  → Pred p → Expr → Statement 
-     and        : Statement → Statement  → Statement 
-     or         : Statement → Statement  → Statement 
-     not        : Statement  → Statement 
-     All        : {x : Term } → Var x → Statement → Statement 
-     Exist      : {x : Term } → Var x → Statement → Statement 
-
-  {-# TERMINATING #-} 
-  Model : (ampa :  {x : Term } → (px :  Pred x ) → Bool )
-       →  (pmap : {p : Term }  → (px :  Pred p ) → Expr → Bool )
-       →  (all-const   : List Expr )
-       → ( subst-prop :  {x : Term } (e : Statement  ) → Var x → (value : Expr ) → Statement  )
-       → Statement  → Bool
-  Model amap pmap all0 sbst s = model s where
-      model :  Statement  → Bool
-      model (atom x) = amap x
-      model (predicate x x₁) = pmap x x₁
-      model (and s s₁) = model s  ∧ model s₁ 
-      model (or s s₁) = model s ∨ model s₁ 
-      model (not s) = Data.Bool.not (model s )
-      model (All x s) = model-all all0 x s  where
-          model-all :  List Expr → {x : Term } → Var x → Statement → Bool
-          model-all [] vx s = true
-          model-all (x ∷ t) vx s = model (sbst s vx x ) ∧ model-all t vx s
-      model (Exist x s) = model-exist all0 x s  where
-          model-exist :  List Expr → {x : Term } → Var x → Statement → Bool
-          model-exist [] vx s = false
-          model-exist (x ∷ t) vx s = model (sbst s vx x ) ∨ model-exist t vx s
-
-data Term : Set where
-      X : Term
-      Y : Term
-      Z : Term
-      a : Term
-      b : Term
-      c : Term
-      f : Term
-      g : Term
-      h : Term
-      p : Term
-      q : Term
-      r : Term
-      _⟨_⟩    : Term → Term → Term
-      _,_     : Term → Term → Term
-      _/\_    : Term → Term → Term
-      _\/_    : Term → Term → Term
-      ¬       : Term → Term 
-      all_=>_ : Term → Term → Term
-      ∃_=>_   : Term → Term → Term
-
-
-data Kind : Set where
-      pred : Kind
-      const : Kind
-      var  : Kind
-      func : Kind
-      arg  : Kind
-      args : Kind
-
-data Kinds : Term → Kind → Set where
-      kX : Kinds X var
-      kY : Kinds Y var
-      kZ : Kinds Z var
-      ka : Kinds a const
-      kb : Kinds b const
-      kc : Kinds c const
-      kf : Kinds f func
-      kg : Kinds g func
-      kh : Kinds h func
-      kp : Kinds p pred
-      kq : Kinds q pred
-      kr : Kinds r pred
-
-Const : Term → Set
-Const x = Kinds x const
-
-Func : Term → Set
-Func x = Kinds x func
-
-Var : Term → Set
-Var x = Kinds x var
-
-Pred : Term → Set
-Pred x = Kinds x pred
-
-open Logic Term Const Func Var Pred 
-
-ex1 : Term
-ex1 = ¬ ( p  /\ ( all X => ( p ⟨ f ⟨ X ⟩ ⟩ )))
-
-parse-arg : (t : Term ) → Maybe Expr 
-parse-arg ( X) = just (var kX)
-parse-arg ( Y) = just (var kY)
-parse-arg ( Z) = just (var kZ)
-parse-arg ( a) = just (const ka)
-parse-arg ( b) = just (const kb)
-parse-arg ( c) = just (const kc)
-parse-arg (f ⟨ x ⟩) with parse-arg x
-parse-arg (f ⟨ x ⟩) | just pt = just ( func kf pt )
-parse-arg (f ⟨ x ⟩) | nothing = nothing
-parse-arg (g ⟨ x ⟩) with parse-arg x
-parse-arg (g ⟨ x ⟩) | just pt = just ( func kg pt )
-parse-arg (g ⟨ x ⟩) | nothing = nothing
-parse-arg (h ⟨ x ⟩) with parse-arg x
-parse-arg (h ⟨ x ⟩) | just pt = just ( func kh pt )
-parse-arg (h ⟨ x ⟩) | nothing = nothing
-parse-arg (_ ⟨ x ⟩) = nothing
-parse-arg (t , t₁) with parse-arg t | parse-arg t₁
-... | just x | just y = just ( args x y )
-... | _ | _ = nothing
-parse-arg _ = nothing
-
-parse : (t : Term ) → Maybe Statement 
-parse ( p) = just ( atom kp )
-parse ( q) = just ( atom kq )
-parse ( r) = just ( atom kr )
-parse (p ⟨ x ⟩) with parse-arg x
-parse (p ⟨ x ⟩) | just y = just ( predicate kp y )
-parse (p ⟨ x ⟩) | nothing = nothing
-parse (q ⟨ x ⟩) with parse-arg x
-parse (q ⟨ x ⟩) | just y = just ( predicate kq y )
-parse (q ⟨ x ⟩) | nothing = nothing
-parse (r ⟨ x ⟩) with parse-arg x
-parse (r ⟨ x ⟩) | just y = just ( predicate kr y )
-parse (r ⟨ x ⟩) | nothing = nothing
-parse (_ ⟨ x ⟩) = nothing
-parse (t /\ t₁) with parse t | parse t₁
-parse (t /\ t₁) | just p₁ | just p₂ = just ( and p₁ p₂ )
-parse (t /\ t₁) | _ | _ = nothing
-parse (t \/ t₁) with parse t | parse t₁
-parse (t \/ t₁) | just p₁ | just p₂ = just ( or p₁ p₂ )
-parse (t \/ t₁) | _ | _ = nothing
-parse (¬ t)  with parse t 
-parse (¬ t)  | just tx = just ( not tx )
-parse (¬ t)  | _ = nothing
-parse (all X => t₁) with parse t₁
-... | just tx = just ( All kX tx )
-... | _ = nothing
-parse (all Y => t₁) with parse t₁
-... | just tx = just ( All kY tx )
-... | _ = nothing
-parse (all Z => t₁) with parse t₁
-... | just tx = just ( All kZ tx )
-... | _ = nothing
-parse (∃ X => t₁) with parse t₁
-... | just tx = just ( Exist kX tx )
-... | _ = nothing
-parse (∃ Y => t₁) with parse t₁
-... | just tx = just ( Exist kY tx )
-... | _ = nothing
-parse (∃ Z => t₁) with parse t₁
-... | just tx = just ( Exist kZ tx )
-... | _ = nothing
-parse _ = nothing
-
-ex2 = parse ex1
-
-subst-expr :  { x : Term } → Expr  → Var x → (value : Expr ) → Expr 
-subst-expr  (var kX) kX v = v
-subst-expr  (var kY) kX v = var kY
-subst-expr  (var kZ) kX v = var kZ
-subst-expr  (var kX) kY v = var kX
-subst-expr  (var kY) kY v = v
-subst-expr  (var kZ) kY v = var kZ
-subst-expr  (var kX) kZ v = var kX
-subst-expr  (var kY) kZ v = var kY
-subst-expr  (var kZ) kZ v = v
-subst-expr  (func f₁ e) xv v = func f₁ ( subst-expr e xv v ) 
-subst-expr  (const x₁) xv v = (const x₁)
-subst-expr  (args e e₁) xv v = args ( subst-expr e xv v ) ( subst-expr e₁ xv v ) 
-
-subst-prop :  {x : Term } (e : Statement  ) → Var x → (value : Expr ) → Statement 
-subst-prop (atom x) xv v = atom x
-subst-prop (predicate x x₁) xv v = predicate x ( subst-expr x₁ xv v )
-subst-prop (and e e₁) xv v = and ( subst-prop e xv v ) ( subst-prop e₁ xv v )
-subst-prop (or e e₁) xv v =  or ( subst-prop e xv v ) ( subst-prop e₁ xv v )
-subst-prop (not e) xv v = not ( subst-prop e xv v )
-subst-prop (All x e) xv v = All x ( subst-prop e xv v )
-subst-prop (Exist x e) xv v = Exist x ( subst-prop e xv v )
-
-amap :  {x : Term } → (px :  Pred x ) → Bool 
-amap {p} px = false
-amap {q} px = true
-amap {r} px = false
-pmap : {p : Term } → (px :  Pred p ) → Expr → Bool 
-pmap {p} px (Logic.const kc) = true
-pmap {p}  px _ = false
-pmap {q}  px _ = false
-pmap {r}  px _ = false
-
-all0   :  List Expr
-all0 =  const ka ∷ const kb ∷ const kc ∷ []
-
-test003 : Bool 
-test003 with parse ( ∃ X => ( p  ⟨  X ⟩ ) )
-test003 | just x = Model amap pmap all0 subst-prop x
-test003 | nothing = false
-