--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/first-order.agda	Thu Aug 13 08:08:44 2020 +0900
@@ -0,0 +1,157 @@
+module first-order where
+open import Data.List hiding (all)
+open import Data.Bool
+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
+
+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
+
+{-# 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 ∷ [] ] )
+
+_=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
+