Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 10:edf4a816abff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
starwars exmple
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 13 Aug 2020 18:44:09 +0900
parents 627a6bf54ed5
children 17cd0e70e931
files Logic.agda example1.agda example2.agda simple-logic.agda
diffstat 4 files changed, 198 insertions(+), 145 deletions(-) [+]
line wrap: on
line diff
--- a/Logic.agda	Thu Aug 13 15:24:47 2020 +0900
+++ b/Logic.agda	Thu Aug 13 18:44:09 2020 +0900
@@ -4,37 +4,46 @@
 
 data Expr  : Set  where
    var   : Var → Expr 
-   func  : (f : Func ) → Expr → Expr 
+   func  : Func → Expr → Expr 
    const : Const → Expr 
-   arg   : Expr → Expr 
+   _,_ : Expr →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 
+   pred       : Pred  → Statement 
+   predx  : Pred  → Expr → Statement 
+   _/\_   : Statement → Statement  → Statement 
+   _\/_         : Statement → Statement  → Statement 
+   ¬_         : Statement  → Statement 
+   All_=>_        : Var → Statement → Statement 
+   Exist_=>_      : Var → Statement → Statement 
+
+subst-prop :  (e : Statement  ) → (sbst : Expr  → Var →  Expr  → Expr  )  → Var → Expr → Statement 
+subst-prop (pred x) sbst xv v = pred x
+subst-prop (predx x x₁) sbst xv v = predx x ( sbst x₁ xv v )
+subst-prop (e /\ e₁) sbst xv v = ( subst-prop e sbst xv v ) /\ ( subst-prop e₁ sbst xv v )
+subst-prop (e \/ e₁) sbst xv v = ( subst-prop e sbst xv v ) \/ ( subst-prop e₁ sbst xv v )
+subst-prop (¬ e) sbst xv v = ¬ ( subst-prop e sbst xv v )
+subst-prop (All x => e) sbst xv v = All x => ( subst-prop e sbst xv v )
+subst-prop (Exist x => e) sbst xv v = Exist x => ( subst-prop e sbst xv v )
 
 {-# TERMINATING #-} 
 M : (amap :  Pred  → Bool ) (pmap :  Pred → Expr → Bool )
    →  (all-const   : List Expr )
-   →  (subst-prop :  Statement  → Var  → Expr  → Statement  )
+   →  (subst-prop : Expr  → Var →  Expr  → Expr  )
    → 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 (pred x) = amap x
+   m (predx x x₁) = pmap x x₁
+   m (s /\ s₁) = m s  ∧ m s₁ 
+   m (s \/ s₁) = m s ∨ m s₁ 
+   m (¬ 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-all (x ∷ t) vx s = m (subst-prop s sbst 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
+     m-exist (x ∷ t) vx s = m (subst-prop s sbst vx x ) ∨ m-exist t vx s
 
--- a/example1.agda	Thu Aug 13 15:24:47 2020 +0900
+++ b/example1.agda	Thu Aug 13 18:44:09 2020 +0900
@@ -3,144 +3,51 @@
 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 Const : Set where
+      a : Const
+      b : Const
+      c : Const
 
-
-data Kind : Set where
-      pred : Kind
-      const : Kind
-      var  : Kind
-      func : Kind
-      arg  : Kind
-      args : Kind
+data Var : Set where
+      X : Var
+      Y : Var
+      Z : Var
 
-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)
+data Func : Set where
+      f : Func
+      g : Func
+      h : Func
 
-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
+data Pred : Set where
+      p : Pred
+      q : Pred
+      r : Pred
 
-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
+open import Logic Const Func Var Pred 
+
+ex1 : Statement
+ex1 = ¬ ( pred q  /\ ( All X =>  predx p ( func f (var X) ) ))
 
-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 :  Expr  → Var → Expr → Expr 
+subst-expr  (var X) X v = v
+subst-expr  (var Y) Y v = v
+subst-expr  (var Z) Z 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-expr  (e , e1) xv v = ( subst-expr e xv v ) , ( subst-expr e1 xv v )
+subst-expr  x _ v = x
 
-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 :  Pred ) → Bool 
+amap q = true
 amap px = false
-pmap : (px :  Kinds pred ) → Expr → Bool 
-pmap kp (const kc) = true
+pmap : (px :  Pred ) → Expr → Bool 
+pmap p (const c) = true
+pmap p (func d (const a) , const b ) = 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 ∷ []
+all0 =  const a ∷ const b ∷ const c ∷ []
 
 test003 : Bool 
-test003 with parse ( ∃ X =>  p  X  )
-test003 | just x = M amap pmap all0 subst-prop x
-test003 | nothing = false
+test003 = M amap pmap all0 subst-expr ( Exist X => predx p (var X)  )
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/example2.agda	Thu Aug 13 18:44:09 2020 +0900
@@ -0,0 +1,72 @@
+module example2 where
+open import Data.List hiding (all ; and ; or )
+open import Data.Maybe 
+open import Data.Bool hiding ( not )
+
+data Const : Set where
+      anakin : Const
+      luke : Const
+      leia : Const
+
+data Var : Set where
+      X : Var
+      Y : Var
+      Z : Var
+
+data Func : Set where
+      f : Func
+
+data Pred : Set where
+      father : Pred
+      brother : Pred
+
+open import Logic Const Func Var Pred 
+
+_⇒_ : Statement → Statement → Statement 
+x ⇒ y = ( ¬ x ) \/ y
+
+ex1 : Statement
+ex1 = All X => All Y => (( Exist Z => ( ( predx father ( var X , var Z ) /\  predx father (var Y , var Z ) ))) ⇒ predx brother ( var X , var Y) )
+
+subst-expr :  Expr  → Var → Expr → Expr 
+subst-expr  (var X) X v = v
+subst-expr  (var Y) Y v = v
+subst-expr  (var Z) Z v = v
+subst-expr  (func f₁ e) xv v = func f₁ ( subst-expr e xv v ) 
+subst-expr  (e , e1) xv v = ( subst-expr e xv v ) , ( subst-expr e1 xv v )
+subst-expr  x _ v = x
+
+amap : (px :  Pred ) → Bool 
+amap px = false
+pmap : (px :  Pred ) → Expr → Bool 
+pmap father ( const leia , const anakin ) = true
+pmap father ( const luke , const anakin ) = true
+pmap brother ( const leia , const luke) = true
+pmap px _ = false
+
+-- we only try simple constant, it may contains arbitrary complex functional value
+all0   :  List Expr
+all0 =  const anakin ∷ const luke ∷ const leia ∷ []
+
+test003 : Bool 
+test003 = M amap pmap all0 subst-expr (
+     ( ex1 /\ ( predx father ( const leia , const anakin ) /\ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
+
+--
+-- Valid Proposition true on any interpretation
+--
+pmap1 : (px :  Pred ) → Expr → Bool 
+pmap1 father ( const leia , const anakin ) = true
+pmap1 father ( const luke , const anakin ) = true
+pmap1 brother ( const leia , const luke) = false
+pmap1 px _ = false
+
+test006 : Bool 
+test006 = M amap pmap1 all0 subst-expr (
+     ( ex1 /\ ( predx father ( const leia , const anakin ) /\ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
+
+test004 : Bool 
+test004 = M amap pmap all0 subst-expr ( ex1  )
+
+test005 : Bool 
+test005 = M amap pmap all0 subst-expr (   All X => All Y => ( predx father ( var X , const anakin ) /\  predx father (var Y , const anakin ) ))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple-logic.agda	Thu Aug 13 18:44:09 2020 +0900
@@ -0,0 +1,65 @@
+module simple-logic where
+open import Data.Bool
+
+data Var : Set where
+   X : Var
+   Y : Var
+   Z : Var
+
+data Expr : Set where
+   var : Var → Expr
+   a : Expr
+   b : Expr
+   c : Expr
+   f : Expr → Expr
+   g : Expr → Expr
+   h : Expr → Expr
+   _,_ : Expr → Expr → Expr
+
+data Statement : Set where
+   p : Expr → Statement
+   q : Statement
+   r : Statement
+   _/\_    :  Statement → Statement → Statement
+   _\/_    :  Statement → Statement → Statement
+   ¬       :  Statement → Statement 
+   all_=>_ :  Var → Statement → Statement
+   ∃_=>_   :  Var → Statement → Statement
+
+test002 : Statement
+test002 = ¬ ( q /\ ( all X => p ( f ( var X  ))))
+
+subst-expr : Expr → Var → (value : Expr ) → Expr
+subst-expr (var X ) X v = v 
+subst-expr (var Y ) Y v = v 
+subst-expr (var Z ) Z v = v 
+subst-expr (f x ) n v = f (subst-expr x n v) 
+subst-expr (x , y ) n v = (subst-expr x n v) , (subst-expr y n v) 
+subst-expr x  n v = x 
+
+subst-prop : (orig : Statement ) → Var → (value : Expr ) → Statement
+subst-prop (p x ) n v = p ( subst-expr x n v )
+subst-prop q n v = q
+subst-prop r n v = r
+subst-prop (x /\ y) n v = subst-prop x n v /\ subst-prop x n v
+subst-prop (x \/ y) n v = subst-prop x n v \/ subst-prop x n v
+subst-prop (¬ x) n v = ¬ (subst-prop x n v )
+subst-prop (all x => y) n v = all x => subst-prop y n v 
+subst-prop (∃ x => y) n v =  ∃ x => subst-prop y n v 
+
+{-# TERMINATING #-} 
+M0 : Statement → Bool
+M0 q = true
+M0 r = false
+M0 (p  a ) = true
+M0 (x /\ y) = M0 x ∧ M0 y
+M0 (x \/ y) = M0 x ∨ M0 y
+M0 (¬ x) = not (M0 x)
+-- we only try simple constant, it may contains arbitrary complex functional value
+M0 (all x => y) = M0 ( subst-prop y x a ) ∧ M0 ( subst-prop y x b ) ∧ M0 ( subst-prop y x c ) 
+M0 (∃ x => y)   = M0 ( subst-prop y x a ) ∨ M0 ( subst-prop y x b ) ∨ M0 ( subst-prop y x c ) 
+M0 _ = false
+
+test003 : Bool 
+test003 = M0 ( ∃ X => p ( var X ))
+