Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 1:a087d3911b07

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 13 Aug 2020 09:26:06 +0900
parents aeccd3123e03
children 08f8256a6b11
files first-order.agda
diffstat 1 files changed, 64 insertions(+), 149 deletions(-) [+]
line wrap: on
line diff
--- a/first-order.agda	Thu Aug 13 08:08:44 2020 +0900
+++ b/first-order.agda	Thu Aug 13 09:26:06 2020 +0900
@@ -1,157 +1,72 @@
 module first-order where
-open import Data.List hiding (all)
-open import Data.Bool
+open import Data.List hiding (all ; and ; or )
+open import Data.Maybe 
+open import Data.Bool hiding ( and ; or ; not )
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 
-data Var : Set where
-   X : Var
-   Y : Var
-   Z : Var
-
-data Expr : Set where
-   a : Expr
-   b : Expr
-   c : Expr
-   var : Var → Expr
-   f[_] : List Expr → Expr
-   g[_] : List Expr → Expr
-   h[_] : List Expr → Expr
-
-data Form : Set where
-   p : Form
-   q : Form
-   r : Form
-   p[_] : List Expr → Form
-   q[_] : List Expr → Form
-   r[_] : List Expr → Form
-   _/\_   :  Form → Form → Form
-   _\/_   :  Form → Form → Form
-   ¬     :  Form → Form 
-   all_=>_ :  Var → Form → Form
-   ∃_=>_ :  Var → Form → Form
-
-test002 : Form
-test002 = ¬ ( p /\ ( all X => p[ f[  var X  ∷ []  ] ∷ []  ] ))
-
-open import Relation.Nullary hiding (¬_)
--- open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
+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
 
-subst-expr : List Expr → Var → (value : Expr ) → List Expr
-subst-expr [] n v = []
-subst-expr (var X ∷ y) X v = v ∷ subst-expr y X v
-subst-expr (var Y ∷ y) Y v = v ∷ subst-expr y X v
-subst-expr (var Z ∷ y) Z v = v ∷ subst-expr y X v
-subst-expr (x ∷ y) n v = x ∷ subst-expr y X v
 
-subst-prop : (orig : Form ) → Var → (value : Expr ) → Form
-subst-prop p[ x ] n v = p[ subst-expr x n v ]
-subst-prop q[ x ] n v = q[ subst-expr x n v ]
-subst-prop r[ x ] n v = r[ subst-expr x n v ]
-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 
-subst-prop x n v = x
+data Var : Term → Set where
+   varX : Var X
+   varY : Var Y
+   varZ : Var Z
 
-{-# TERMINATING #-} 
-M0 : Form → Bool
-M0 p = false
-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 (¬ f) = not (M0 f)
-M0 (all x => f) = M0 ( subst-prop f x a ) ∧ M0 ( subst-prop f x b ) ∧ M0 ( subst-prop f x c ) 
-M0 (∃ x => f)   = M0 ( subst-prop f x a ) ∨ M0 ( subst-prop f x b ) ∨ M0 ( subst-prop f x c ) 
-M0 _ = false
-
-test003 : Bool 
-test003 = M0 ( ∃ X => p[ var X ∷ [] ] )
+data Func : Term → Set where
+   funcf : Func f
+   funcg : Func g
+   funch : Func h
 
-_=n?_ : (x y : List Expr )→ Dec ( x ≡ y )
-_=?_ : (x y : Expr )→ Dec ( x ≡ y )
-a =? a = yes refl
-a =? b = no (λ ())
-a =? c =  no (λ ())
-a =? var x =  no (λ ())
-a =? f[ x ] =  no (λ ())
-a =? g[ x ] =  no (λ ())
-a =? h[ x ] =  no (λ ())
-b =? b = yes refl
-b =? a = no (λ ())
-b =? c = no (λ ())
-b =? var x = no (λ ())
-b =? f[ x ] = no (λ ())
-b =? g[ x ] = no (λ ())
-b =? h[ x ] = no (λ ())
-c =? c = yes refl
-c =? a =  no (λ ())
-c =? b =  no (λ ())
-c =? var x =  no (λ ())
-c =? f[ x ] =  no (λ ())
-c =? g[ x ] =  no (λ ())
-c =? h[ x ] =  no (λ ())
-var X =? var X =  yes refl
-var X =? var Y = no (λ ())
-var X =? var Z = no (λ ())
-var Y =? var X = no (λ ())
-var Y =? var Y = yes refl
-var Y =? var Z = no (λ ())
-var Z =? var X = no (λ ())
-var Z =? var Y = no (λ ())
-var Z =? var Z = yes refl
-var x =? a = no (λ ())
-var x =? b = no (λ ())
-var x =? c = no (λ ())
-var x =? f[ x₁ ] = no (λ ())
-var x =? g[ x₁ ] = no (λ ())
-var x =? h[ x₁ ] = no (λ ())
-f[ x ] =? a = no (λ ())
-f[ x ] =? b = no (λ ())
-f[ x ] =? c = no (λ ())
-f[ x ] =? var x₁ = no (λ ())
-f[ x ] =? g[ x₁ ] = no (λ ())
-f[ x ] =? h[ x₁ ] = no (λ ())
-f[ x ] =? f[ y ] with x  =n? y  
-... | yes eq = yes ( cong (λ k → f[ k ] ) eq )
-... | no ¬p = no (λ eq → ¬p ( lemma eq )) where
-   lemma : f[ x ] ≡ f[ y ] → x ≡ y
-   lemma refl = refl
-g[ x ] =? a = no (λ ())
-g[ x ] =? b = no (λ ())
-g[ x ] =? c = no (λ ())
-g[ x ] =? var x₁ = no (λ ())
-g[ x ] =? f[ x₁ ] = no (λ ())
-g[ x ] =? h[ x₁ ] = no (λ ())
-g[ x ] =? g[ y ] with x  =n? y  
-... | yes eq = yes ( cong (λ k → g[ k ] ) eq )
-... | no ¬p = no (λ eq → ¬p ( lemma eq )) where
-   lemma : g[ x ] ≡ g[ y ] → x ≡ y
-   lemma refl = refl
-h[ x ] =? a = no (λ ())
-h[ x ] =? b = no (λ ())
-h[ x ] =? c = no (λ ())
-h[ x ] =? var x₁ = no (λ ())
-h[ x ] =? f[ x₁ ] = no (λ ())
-h[ x ] =? g[ x₁ ] = no (λ ())
-h[ x ] =? h[ y ] with x  =n? y  
-... | yes eq = yes ( cong (λ k → h[ k ] ) eq )
-... | no ¬p = no (λ eq → ¬p ( lemma eq )) where
-   lemma : h[ x ] ≡ h[ y ] → x ≡ y
-   lemma refl = refl
-[] =n? [] = yes refl
-[] =n? (x ∷ y) = no (λ ())
-(x ∷ x₁) =n? [] = no (λ ())
-(x0 ∷ t0) =n? (x1 ∷ t1) with x0 =? x1
-... | no ¬p = no (λ eq → ¬p (lemma eq) ) where
-   lemma :  x0 ∷ t0 ≡ x1 ∷ t1 →  x0 ≡ x1
-   lemma refl = refl
-... | yes eq with t0 =n? t1
-... | yes eql = yes (cong₂ (λ j k → j ∷ k ) eq eql)
-... | no ¬p = no (λ eq → ¬p ( lemma eq) ) where
-   lemma :  x0 ∷ t0 ≡ x1 ∷ t1 →  t0 ≡ t1
-   lemma refl = refl
+data Const : Term → Set where
+   ca : Const a
+   cb : Const b
+   cc : Const c
+
+data Predicate  : Term → Set where
+   pp : Predicate p
+   pq : Predicate q
+   pr : Predicate r
+
+ex1 : Term
+ex1 = ¬ ( p /\ ( all X => ( p ⟨ f ⟨ X ⟩ ⟩ )))
+
+module Logic (Const Func Var : Term → Set)  where
 
+  data Expr  : Set 
+  data Args  : List Expr  → Set  where
+     last : (last : Expr ) → Args [ last ]
+     next : (h : Expr ) → {t : List Expr  } → Args   t   → Args  ( h ∷ t )
+
+  data Expr  where
+     var   : {v : Term} → Var v → Expr 
+     func  : {x : Term} → (f : Func x) → {args : List Expr } → Args  args → Expr 
+     const : {c : Term} → Const c → Expr 
+
+  data Statement : Term → Set where
+     and  :  {x y : Term } → Statement x → Statement y  → Statement ( x /\ y )
+     or   :  {x y : Term } → Statement x → Statement y  → Statement ( x \/ y )
+     not   :  {x : Term } → Statement x → Statement ( ¬ x  )
+     All    :  {x t : Term} → Var x → Statement t → Statement ( all x => t )
+     Exist  :  {x t : Term} → Var x → Statement t → Statement ( ∃ x => t )
+
+  parse : (t : Term ) → Maybe (Statement t )
+  parse t = {!!}