Wiki

Bitbucket

Dashboard
チーム
リポジトリ
Snippets

owner/repository
Logged in as HirokazuYatsu

2
3

Wiki CafeOBJ / OSEK / contents / index-e / 04_Complement 表示履歴編集削除タイトルrequired ページの内容

Complement of Invresed Relation

In this section, we introduce two modules. One is a module to extend a relation on a set to that on a powerset. The other is a module to produce the complement of the inverse of a given relation.

EXTEND

Let R be an arbitrary binary relation on a set S. The module EXTEND enables us to extend R to a relation on the powerset of S.

#!python
module EXTEND
(
  X :: TRIV,
  C :: SET(X),
  R :: RELATION(X)
)
{
  imports
  {
    ex(DEDUCIBLE)
  }
  signature
  {
    op  ___ : Set Relation Set -> Prop
  }
  axioms
  {
    vars X Y : Elt
    vars S U V : Set
    vars R : Relation
    cq S R nil = true
       if neg(S = nil) .
    eq nil R S = false .
--  (S R (U,V)) = (S R U)/\(S R V)
    eq deducible((S R (U,V)) |- (S R U)) = true .
    eq deducible((S R U),(S R V) |- (S R (U,V))) = true .
--  ((U,V) R S) = (U R S)\/(V R S)
    eq deducible(((U,V) R S) |- (U R S),(V R S)) = true .
    eq deducible((U R S) |- ((U,V) R S)) = true .
  }
}

COMPLEMENT

The module COMPLEMENT is to declare a function which returns the complement of the inverse of a given relation.

Let R be an arbitrary relation on a set S. Then, the relation [R] represents the complement of the inverse of R. For any x,y∈S,

x [R] y ⇔ ¬(y R x)

#!python
module COMPLEMENT
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  imports
  {
    ex(DEDUCIBLE)
  }
  signature
  {
    op [_] : Relation -> Relation
  }
  axioms
  {
    vars X Y : Elt
    vars R : Relation
--  X [R] Y = (neg Y R X) .
    eq deducible((X [R] Y),(Y R X) |- nil) = true .
    eq deducible(nil |- (X [R] Y),(Y R X)) = true .
  }
}

LEMMA1/COMPLEMENT

For any irreflexive relation R, the complement of its reverse [R] is also irreflexive. This claim can be declared as the following module.

#!python
module CLAIM1/COMPLEMENT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMPLEMENT(X,R))
  }
  signature
  {
    op r : -> Irreflexive
    op x : -> Elt
    op claim : -> Prop
  }
  axioms
  {
    eq claim = deducible(nil |- (x [r] x)) .
  }
}

This claim can be reduced to true by executing the following proof score:

#!python
open CLAIM1/COMPLEMENT .
ops q1 q2 : -> Sequent .
eq q1 = (nil |- (x [r] x),(x r x)) .
eq q2 = ((x r x) |- nil) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2) .
eq (nil |- (x [r] x)) = consequent(i) .
red claim .
close

The result of the execution of the above score is:

#!python
-- reduce in %CLAIM1/COMPLEMENT(X, S, R, I) : (claim):Prop

** Found [state 3] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 30 rewrites(0.010 sec), 217 matches, 1 memo hits)

Then, we obtain the following lemma:

module LEMMA1/COMPLEMENT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  C :: COMPLEMENT(X,R)
)
{
  imports
  {
    pr(LK)
  }
  axioms
  {
    vars X : Elt
    vars R : Irreflexive
    eq deducible(nil |- (X [R] X)) = true .
  }
}

LEMMA2/COMPLEMENT

For any asymmetric relation R on a set S, the complement of the inverse of R becomes to be total, i.e.,

∀s⊆S,x∈S・(x [R] s)∨(s [R] x)

#!python
module CLAIM2/COMPLEMENT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  A :: ASYMMETRIC(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMPLEMENT(X,R))
    pr(EXTEND(X,S,R))
  }
  signature
  {
    op x : -> Elt
    op r : -> Asymmetric 
    op claim : Set -> Prop
  }
  axioms
  {
    vars S : Set
    eq claim(S) = deducible(nil |- ((x [r] S),(S [r] x))) .
  }
}

This claim is proved with structural induction on S. The proof score to prove that the claim becomes true is as follows:

#!python
-- [base case]
open CLAIM2/COMPLEMENT .
red claim(nil) .
close

-- [induction step]
open CLAIM2/COMPLEMENT .
ops s n : -> Set .
ops y : -> Elt .
eq n = (s,y) .
-- [induction hypothesis]
eq deducible(nil |- ((x [r] s),(s [r] x))) = true .
-- under the hypothesis, claim(n) is reduced to be true
ops q1 q2 q3 q4 q5 q6 q7 : -> Sequent .
-- asymmetricity of r
eq q1 = ((x r y),(y r x) |- nil) .
-- definitions of the complement of r
eq q2 = (nil |- (x [r] y),(y r x)) .
eq q3 = (nil |- (y [r] x),(x r y)) .
-- asummption of induction
eq q4 = (nil |- (x [r] s),(s [r] x)) .
-- definition of extention of [r]
eq q5 = ((x [r] s),(x [r] y) |- (x [r] n)) .
eq q6 = ((s [r] x) |- (n [r] x)) .
eq q7 = ((y [r] x) |- (n [r] x)) .
ops i1 i2 i3 : -> Inference .
eq antecedent(i1) = (q1,q2,q3) .
trans (nil |- (x [r] y),(y [r] x)) => consequent(i1) .
trans consequent(i1) => (nil |- (x [r] y),(y [r] x)) .
eq antecedent(i2) = (consequent(i1),q4,q5) .
trans (nil |- (x [r] (s,y)),(s [r] x),(y [r] x)) => consequent(i2) .
trans consequent(i2) => (nil |- (x [r] (s,y)),(s [r] x),(y [r] x)) .
eq antecedent(i3) = (consequent(i2),q6,q7) .
eq (nil |- ((x [r] (s,y)),((s,y) [r] x))) = consequent(i3) .
red claim(n) .
close

The result of the execution of the above score is:

#!python
-- opening module CLAIM2/COMPLEMENT(X, S, R, A).. done.
-- reduce in %CLAIM2/COMPLEMENT(X, S, R, A) : (claim(nil)):Prop
(true):Bool
(0.000 sec for parse, 6 rewrites(0.000 sec), 41 matches)

-- opening module CLAIM2/COMPLEMENT(X, S, R, A).. done.
___*
-- reduce in %CLAIM2/COMPLEMENT(X, S, R, A) : (claim(n)):Prop

** Found [state 719] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1240] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 268] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 32388 rewrites(13.420 sec), 1786294 matches, 18344 memo hits)

This result indicates that the claim holds. So, we obtain the following lemma:

#!python
module LEMMA2/COMPLEMENT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  A :: ASYMMETRIC(X,R),
  C :: COMPLEMENT(X,R),
  E :: EXTEND(X,S,R)
)
{
  imports
  {
    pr(LK)
  }
  axioms
  {
    vars S : Set
    vars X : Elt
    vars R : Asymmetric
    eq deducible(nil |- ((X [R] S),(S [R] X))) = true .
  }
}

LEMMA3/COMPLEMENT

For any transitive relation R on a set S, the following traisitivity holds:

∀x,y∈S・∀s⊆S・(x R y)∧(y [R] s) ⇒ (x [R] s)

#!python
module CLAIM3/COMPLEMENT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  T :: TRANSITIVE(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMPLEMENT(X,R))
    pr(EXTEND(X,S,R))
  }
  signature
  {
    ops x y : -> Elt
    op r : -> Transitive
    op claim : Set -> Prop
  }
  axioms
  {
    vars S : Set
    eq claim(S) = deducible((x r y),(y [r] S) |- (x [r] S)) .
  }
}

We can prove this claim with structural induction on S. The following is the proof score to reduce the claim to true.

#!python
-- [base case]
open CLAIM3/COMPLEMENT .
red claim(nil) .
close

-- [induction step]
open CLAIM3/COMPLEMENT .
ops c n : -> Set .
ops z : -> Elt .
eq n = c,z .
-- [induction hypothesis]
eq deducible((x r y),(y [r] c) |- (x [r] c)) = true .
ops q1 q2 q3 q4 q5 q6 q7 : -> Sequent .
-- transitivity of r
eq q1 = ((z r x),(x r y) |- (z r y)) .
-- definition of complement
eq q2 = ((y [r] z),(z r y) |- nil) .
eq q3 = (nil |- (x [r] z),(z r x)) .
-- hypothesis of induction
eq q4 = ((x r y),(y [r] c) |- (x [r] c)) .
-- definitions of extension
eq q5 = ((x [r] z),(x [r] c) |- (x [r] n)) .
eq q6 = ((y [r] n) |- (y [r] z)) .
eq q7 = ((y [r] n) |- (y [r] c)) .
ops i1 i2 i3 i4 : -> Inference .
eq antecedent(i1) = (q1,q2,q3) .
trans ((x r y),(y [r] z) |- (x [r] z)) => consequent(i1) .
trans consequent(i1) => ((x r y),(y [r] z) |- (x [r] z)) .
eq antecedent(i2) = (consequent(i1),q5) .
trans ((x r y),(y [r] z),(x [r] c) |- (x [r] (c,z))) => consequent(i2) .
trans consequent(i2) => ((x r y),(y [r] z),(x [r] c) |- (x [r] (c,z))) .
eq antecedent(i3) = (consequent(i2),q4) .
trans ((x r y),(y [r] z),(y [r] c) |- (x [r] (c,z))) => consequent(i3) .
trans consequent(i3) => ((x r y),(y [r] z),(y [r] c) |- (x [r] (c,z))) .
eq antecedent(i4) = (consequent(i3),q6,q7) .
eq ((x r y),(y [r] (c,z)) |- (x [r] (c,z))) = consequent(i4) .
red claim(n) .
close

The result of the execution of the above score is:

#!python
-- opening module CLAIM3/COMPLEMENT(X, S, R, T).. done.
-- reduce in %CLAIM3/COMPLEMENT(X, S, R, T) : (claim(nil)):Prop
(true):Bool
(0.000 sec for parse, 14 rewrites(0.000 sec), 154 matches)

-- opening module CLAIM3/COMPLEMENT(X, S, R, T).. done.
___*
-- reduce in %CLAIM3/COMPLEMENT(X, S, R, T) : (claim(n)):Prop

** Found [state 1366] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 267] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 179] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 376] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 23159 rewrites(12.780 sec), 1304434 matches, 12495 memo hits)

So, we obtain the following lemma:

#!python
module LEMMA3/COMPLEMENT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  T :: TRANSITIVE(X,R),
  C :: COMPLEMENT(X,R),
  E :: EXTEND(X,S,R)
)
{
  imports
  {
    pr(LK)
  }
  axioms
  {
    vars X Y : Elt
    vars R : Transitive
    vars S : Set
    eq deducible((X R Y),(Y [R] S) |- (X [R] S)) = true .
  }
}

LEMMA4/COMPLEMENT

For any asymmetric relation R on a set S, the complement of the inverse of R includes R itself.

∀x,y∈S・(x R y) ⇒ (x [R] y)

This claim can be represented as the following module:

#!python
module CLAIM4/COMPLEMENT
(
  X :: TRIV,
  R :: RELATION(X),
  A :: ASYMMETRIC(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMPLEMENT(X,R))
  }
  signature
  {
    ops x y : -> Elt
    op  r : -> Asymmetric 
    op  claim : -> Prop
  }
  axioms
  {
    eq claim = deducible((x r y) |- (x [r] y)) .
  }
}

We can prove this claim becomes true easily from the definition of asymmetricity and complement. The proof score for the claim is described as follows:

#!python
open CLAIM4/COMPLEMENT .
ops q1 q2 : -> Sequent .
eq q1 = ((x r y),(y r x) |- nil) .
eq q2 = (nil |- (x [r] y),(y r x)) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2) .
eq ((x r y) |- (x [r] y)) = consequent(i) .
red claim .
close

The result of the execution of the above score is:

#!python
-- opening module CLAIM4/COMPLEMENT(X, R, A).. done.
__*
-- reduce in %CLAIM4/COMPLEMENT(X, R, A) : (claim):Prop

** Found [state 1] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 42 rewrites(0.000 sec), 412 matches, 7 memo hits)

So, we obtain the following lemma:

#!python
module LEMMA4/COMPLEMENT
(
  X :: TRIV,
  R :: RELATION(X),
  A :: ASYMMETRIC(X,R),
  C :: COMPLEMENT(X,R)
)
{
  imports
  {
    pr(LK)
  }
  axioms
  {
    vars X Y : Elt
    vars R : Asymmetric
    eq deducible((X R Y) |- (X [R] Y)) = true .
  }
}

LEMMA5/COMPLEMENT

Let (S,R) be an arbitrary totally ordered set. Then the following three properties on transitivity hold.

∀x,y,z∈S・(x [R] y)∧(y R z) ⇒ (x R z)
∀x,y,z∈S・(x R y)∧(y [R] z) ⇒ (x R z)
∀x,y,z∈S・(x [R] y)∧(y [R] z) ⇒ (x [R] z)

#!python
module CLAIM5/COMPLEMENT
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  V :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,V),
  T :: TOTALORDER(X,R,I,A,V,P)
)
{
  imports
  {
    pr(LEMMA1/TOTALORDER(X,R,I,A,V,P,T))
    pr(COMPLEMENT(X,R))
  }
  signature
  {
    ops x y z : -> Elt
    op  r : -> TotalOrder
    ops claim1 claim2 claim3 : -> Prop
    }
    axioms
  {
    eq claim1 = deducible((x [r] y),(y r z) |- (x r z)) .
    eq claim2 = deducible((x r y),(y [r] z) |- (x r z)) .
    eq claim3 = deducible((x [r] y),(y [r] z) |- (x [r] z)) .
  }
}

These claims can be proved to become true using LEMMA1/TOTALORDER. The proof score to prove these claims is:

#!python
open CLAIM5/COMPLEMENT .
ops q1 q2 : -> Sequent .
eq q1 = ((y r z) |- (x r z),(y r x)) .
eq q2 = ((x [r] y),(y r x) |- nil) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2) .
eq ((x [r] y),(y r z) |- (x r z)) = consequent(i) .
red claim1 .
close
--
open CLAIM5/COMPLEMENT .
ops q1 q2 : -> Sequent .
eq q1 = ((x r y) |- (x r z),(z r y)) .
eq q2 = ((y [r] z),(z r y) |- nil) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2) .
eq ((x r y),(y [r] z) |- (x r z)) = consequent(i) .
red claim2 .
close
--
open CLAIM5/COMPLEMENT .
ops q1 q2 q3 q4 : -> Sequent .
eq q1 = ((z r x) |- (y r x),(z r y)) .
eq q2 = ((x [r] y),(y r x) |- nil) .
eq q3 = ((y [r] z),(z r y) |- nil) .
eq q4 = (nil |- (x [r] z),(z r x)) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2,q3,q4) .
eq ((x [r] y),(y [r] z) |- (x [r] z)) = consequent(i) .
red claim3 .
close

The result of the execution of the above score is:

#!python
-- opening module CLAIM5/COMPLEMENT(X, R, I, A, V, P, T).. done.
__*
-- reduce in %CLAIM5/COMPLEMENT(X, R, I, A, V, P, T) : 
    (claim1):Prop

** Found [state 1] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 47 rewrites(0.000 sec), 676 matches, 7 memo hits)

-- opening module CLAIM5/COMPLEMENT(X, R, I, A, V, P, T).. done.
__*
-- reduce in %CLAIM5/COMPLEMENT(X, R, I, A, V, P, T) : 
    (claim2):Prop

** Found [state 1] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 47 rewrites(0.000 sec), 676 matches, 7 memo hits)

-- opening module CLAIM5/COMPLEMENT(X, R, I, A, V, P, T).. done.
__*
-- reduce in %CLAIM5/COMPLEMENT(X, R, I, A, V, P, T) : 
    (claim3):Prop

** Found [state 982] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 47936 rewrites(45.600 sec), 2301887 matches, 30145 memo hits)

We obtain the following lemma:

#!python
module LEMMA5/COMPLEMENT
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  V :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,V),
  T :: TOTALORDER(X,R,I,A,V,P),
  C :: COMPLEMENT(X,R)
)
{
  imports
  {
    pr(LK)
  }
    axioms
  {
    vars X Y Z : Elt
    vars R : TotalOrder
    eq deducible((X [R] Y),(Y R Z) |- (X R Z)) = true .
    eq deducible((X R Y),(Y [R] Z) |- (X R Z)) = true  .
    eq deducible((X [R] Y),(Y [R] Z) |- (X [R] Z)) = true  .
  }
}

コミットメッセージキャンセル

ブログ サポート Plans & pricing ドキュメント API Site status Version info サービス利用規約 プライバシー ポリシー

JIRA Confluence Bamboo SourceTree HipChat

Atlassian