logo

Demonstrations for the theory of proveit.logic.sets.equivalence

In [1]:
import proveit
from proveit import a, b, c, d, e, x, A, B, C
from proveit import InstantiationFailure, ProofFailure
from proveit.logic import Equals, Forall, InSet, Not, Set, SetEquiv, SetNotEquiv
from proveit.numbers import one, two, three, four, five, Real
from proveit.logic.sets.equivalence  import set_equiv_def, set_not_equiv_def
from proveit.logic.sets.equivalence import (
        set_equiv_reflexivity, set_equiv_reversal, set_equiv_transitivity)
%begin demonstrations

Set Equivalence $A \cong B$ and Set Non-Equivalence $A\not\cong B$

[Under Construction]

Introduction

The Set Equivalence class, SetEquiv, is intended to capture the membership equivalence of 2 structures A and B. $A \cong B$, coded in Prove-It by SetEquiv(A, B) is a claim that all elements of A are also elements of B and vice-versa, and uses the congruence symbol $\cong$ to distinguish the SetEquiv claim from the stronger claim that $A = B$.</font>

Simple Expressions Set Equivalence

Set Equivalence expressions are easy to construct …

Common Attributes of Set Equivalence Expressions

Let's look at some simple examples of set equivalence expressions and their common attributes.

In [2]:
SetEquiv(A, B)

Axioms

The axiomatic basis for set equivalence currently consists of two axioms, one defining set equivalence in terms of membership and one defining set non-equivlance (these can be found in the [set equivalence theorems Jupyter Python notebook](axioms.ipynb) ):

In [3]:
set_equiv_def
 ⊢  
In [4]:
set_not_equiv_def
 ⊢  

Theorems & Conjectures

The `logic.sets/equivalence` theory already has a number of related theorems and conjectures established, many of which are related to set equivalence being an equivalence relation. Some illustrative examples of the theorems are shown below, and the remainder can be found in the [set equivalence theorems Jupyter Python notebook](theorems.ipynb).

In [5]:
set_equiv_reflexivity
 ⊢  
In [6]:
set_equiv_reversal
 ⊢  
In [7]:
set_equiv_transitivity
 ⊢  

Demonstrations

1. TBA.

Under Construction

2. TBA.

Under Construction

3. TBA.

Under construction

Miscellaneous Testing

The material below was developed to test various SetEquiv-related methods. Some of this material could be integrated into the `_demonstrations_` page eventually and/or deleted as development continues.

Some Example Sets For Testing

In [8]:
# some standard enumerated sets
from proveit import e
set_12345, set_abcde, set_1a2b3c, power_set_of_ab, empty_set = (
    Set(one, two, three, four, five),
    Set(a, b, c, d, e),
    Set(one, a, two, b, three, c),
    Set(Set(), Set(a), Set(b), Set(a,b)),
    Set())
set_12345:
set_abcde:
set_1a2b3c:
power_set_of_ab:
empty_set:
In [9]:
# some non-standard enumerated sets pretending to be multi-sets (but not!)
set_12131, set_1a1b2a = (
    Set(one, two, one, three, one),
    Set(one, a, one, b, two, a))
set_12131:
set_1a1b2a:

Testing the SetEquiv.conclude() method

The conclude() method is a general method with the following format:

conclude(**defaults_config)

and attempts to conclude the equivalence in various ways: (1) using simple reflexivity (A equiv A); (2) via an evaluation (if one side is an irreducible); or (3) via transitivity.

In [10]:
SetEquiv(C, C).conclude()
 ⊢  
In [11]:
# As one would expect, we cannot conclude a set-equivalence between 
# two arbitrary sets
try:
    SetEquiv(Set(one, two, three), Set(a, b, c)).conclude()
    assert False, "Should not get this far!"
except ProofFailure as the_error:
    print("ProofFailure: {}".format(the_error))

ProofFailure: Unable to prove {1, 2, 3} equiv {a, b, c}:
Unable to automatically conclude by standard means.  To try to prove this via transitive implication relations, try 'conclude_via_transitivity'.
In [12]:
# This also doesn't work even with these proper assumptions because
# these substitutions are not made automatically.
try:
    SetEquiv(Set(one, d, three), Set(a, b, c)).conclude(
        assumptions=[Equals(a, one), Equals(b, d), Equals(c, three)])
    assert False, "Should not get this far!"
except ProofFailure as the_error:
    print("ProofFailure: {}".format(the_error))

ProofFailure: Unable to prove {1, d, 3} equiv {a, b, c} assuming {a = 1, b = d, c = 3}:
Unable to automatically conclude by standard means.  To try to prove this via transitive implication relations, try 'conclude_via_transitivity'.
In [13]:
# But evaluations to irreducible values are special in this regard and we can prove the following.
SetEquiv(Set(one, two, three), Set(a, b, c)).conclude(
        assumptions=[Equals(a, one), Equals(b, two), Equals(c, three)])
, ,  ⊢  

Testing the SetEquiv.conclude_via_reflexivity() method

The conclude_via_reflexivity() method has the following format:

conclude_via_reflexivity(**defaults_config)

and attempts to prove and return self of the form A equiv A.

In [14]:
# Notice that reflexivity of set equivalence should generally
# not require any assumptions
SetEquiv(A, A).conclude_via_reflexivity()
 ⊢  
In [15]:
SetEquiv(Set(a, two, c), Set(a, two, c)).conclude_via_reflexivity()
 ⊢  
In [16]:
# We can use standard pre-defined sets as well
SetEquiv(Real, Real).conclude_via_reflexivity()
 ⊢  
In [17]:
# in fact, reflexivity is captured generally in the conclude()
# method, allowing Prove-It to prove() reflexive set equivalence claims
SetEquiv(Set(a, b, three), Set(a, b, three)).prove()
 ⊢  
In [18]:
# If the 'self' object on which we call the conclude_via_reflexivity() method
# is not actually reflexive (i.e. the lhs and rhs are not literally the same),
# we get an error:
try:
    SetEquiv(A, B).conclude_via_reflexivity()
    assert False, "Should not make it this far!"
except ProofFailure as the_error:
    print("AssertionError: {}".format(the_error))

AssertionError: Proof step failed:
Attempting to instantiate |- forall_{A, B | A = B} (A equiv B) with {A: A, B: B}:
Unsatisfied condition: A = B. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [19]:
SetEquiv(A, B).conclude_via_reflexivity(assumptions=[Equals(A, B)])
 ⊢  

Testing the SetEquiv.conclude_as_folded() method

The conclude_as_folded() method has the following format:

conclude_as_folded(**defaults_config)

and is described as attempting to conclude A set_equiv B from $\forall_{x} [(x \in A) = (x \in B)]$. This is somewhat confusing, since the method is called on the SetEquiv(A, B) object itself.

In [20]:
SetEquiv(A, B).conclude_as_folded(assumptions=[Forall(x, Equals(InSet(x, A), InSet(x, B)))])
 ⊢  
In [21]:
SetEquiv(Set(one, two , three), Set(a, b, c)).conclude_as_folded(
        assumptions=[Forall(x, Equals(InSet(x, Set(one, two, three)), InSet(x, Set(a, b, c))))])
 ⊢  
In [22]:
# We can use standard pre-defined sets as well
SetEquiv(A, Real).conclude_as_folded(assumptions=[Forall(x, Equals(InSet(x, A), InSet(x, Real)))])
 ⊢  
In [23]:
# We must already know or assume that the membership claims are equal
try:
    SetEquiv(Set(one, two , three), Set(a, b, c)).conclude_as_folded()
    assert False, "Should not make it this far!"
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: Proof step failed:
Attempting to instantiate |- forall_{A, B | forall_{x} ((x in A) = (x in B))} (A equiv B) with {A: {1, 2, 3}, B: {a, b, c}}:
Unsatisfied condition: forall_{x} ((x in {1, 2, 3}) = (x in {a, b, c})). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Testing the SetEquiv.unfold() method

The unfold() method has the following format:

unfold(**defaults_config)

and from A setequiv B attempts to derive $\forall{x} [ (x \in A) = (x \in B)]$.

In [24]:
SetEquiv(A, B).unfold(assumptions=[SetEquiv(A, B)])
 ⊢  
In [25]:
SetEquiv(Set(one, two , three), Set(a, b, c)).unfold(
        assumptions=[SetEquiv(Set(one, two , three), Set(a, b, c))])
 ⊢  
In [26]:
# We can use standard pre-defined sets as well
SetEquiv(A, Real).unfold(assumptions=[SetEquiv(A, Real)])
 ⊢  
In [27]:
# We must already know or assume that the SetEquiv holds in one direction
try:
    SetEquiv(Set(one, two , three), Set(a, b, c)).unfold()
    assert False, "Should not make it this far!"
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: Proof step failed:
Attempting to instantiate |- forall_{A, B | A equiv B} [forall_{x} ((x in A) = (x in B))] with {A: {1, 2, 3}, B: {a, b, c}}:
Unsatisfied condition: {1, 2, 3} equiv {a, b, c}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Testing the SetEquiv.derive_reversed() method

The derive_reversed() method has the following format:

derive_reversed(**defaults_config)

and from A set_equiv B attempts to derive B set_equiv A. This derivation is also an automatic side-effect.

In [28]:
SetEquiv(A, B).derive_reversed(assumptions=[SetEquiv(A, B)])
 ⊢  
In [29]:
SetEquiv(Set(one, two , three), Set(a, b, c)).derive_reversed(
        assumptions=[SetEquiv(Set(one, two , three), Set(a, b, c))])
 ⊢  
In [30]:
# We can use standard pre-defined sets as well
SetEquiv(A, Real).derive_reversed(assumptions=[SetEquiv(A, Real)])
 ⊢  
In [31]:
# We must already know or assume that the SetEquiv holds in one direction
try:
    SetEquiv(Set(one, two , three), Set(a, b, c)).derive_reversed()
    assert False, "Should not make it this far!"
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: Proof step failed:
Attempting to instantiate |- forall_{A, B | A equiv B} (B equiv A) with {A: {1, 2, 3}, B: {a, b, c}}:
Unsatisfied condition: {1, 2, 3} equiv {a, b, c}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Testing the SetEquiv.deduce_not_equiv() method

The deduce_not_equiv() method has the following format:

deduce_not_equiv(**defaults_config)

and attempts to deduce A not_equiv B assuming not(A equiv B), but where self is (A equiv B). This can be a bit confusing …

In [32]:
SetEquiv(A, B).deduce_not_equiv(assumptions=[Not(SetEquiv(A, B))])
 ⊢  
In [33]:
SetEquiv(Set(one, two, three), Set(a, b, c)).deduce_not_equiv(assumptions=[Not(SetEquiv(Set(one, two, three), Set(a, b, c)))])
 ⊢  
In [34]:
# despite the apparent disconnect between the 'self' SetEquiv, that SetEquiv must
# use the same sets being used in the conclusion
try:
    SetEquiv(Set(one, two, four), Set(a, b, c)).deduce_not_equiv(
            assumptions=[Not(SetEquiv(Set(one, two, three), Set(a, b, c)))])
    assert False, "Should not make it this far!"
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: Proof step failed assuming {[not]({1, 2, 3} equiv {a, b, c})}:
Attempting to instantiate |- forall_{A, B | [not](A equiv B)} (A not_equiv B) with {A: {1, 2, 4}, B: {a, b, c}}:
Unsatisfied condition: [not]({1, 2, 4} equiv {a, b, c}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Testing the SetEquiv.apply_transitivity() method

The apply_transitivity() method has the following format:

apply_transitivity(other, **defaults_config)

From A set_equiv B (self) and B set_equiv C (other) attempt to derive and return A set_equiv C. If "other" is not a SetEquiv, reverse roles and call 'apply_transitivity' from the "other" side.

In [35]:
SetEquiv(Set(one, two, three), Set(two, three, one)).apply_transitivity(
    SetEquiv(Set(two, three, one), Set(b, c, a)),
    assumptions=[SetEquiv(Set(one, two, three), Set(two, three, one)),
                 SetEquiv(Set(two, three, one), Set(b, c, a))])
,  ⊢  
In [36]:
SetEquiv(A, B).apply_transitivity(
    SetEquiv(B, C), assumptions=[SetEquiv(A, B), SetEquiv(B, C)])
,  ⊢  

Testing the SetEquiv.deduce_in_bool() method

The deduce_in_bool() method has the following format:

deduce_in_bool(**defaults_config):

and attempts to deduce and return that this SetEquiv claim is in the Boolean set.

In [37]:
SetEquiv(Set(one, two, three), Set(two, three, one)).deduce_in_bool()
 ⊢  
In [38]:
SetEquiv(Set(one, two, three), Set(four, five)).deduce_in_bool()
 ⊢  
In [39]:
SetEquiv(Set(one, two, three), Set(two, three, a)).deduce_in_bool(assumptions=[Equals(a, one)])
 ⊢  

Testing the SetNotEquiv.derive_reversed() method

The derive_reversed() method has the following format:

derive_reversed(**defaults_config)

and from A not_equiv B attempts to derive B not_equiv A. This derivation is also an automatic side-effect in the side_effects() method.

In [40]:
SetNotEquiv(A, B).derive_reversed(assumptions=[SetNotEquiv(A, B)])
 ⊢  
In [41]:
SetNotEquiv(Set(one, two , three), Set(a, b, c)).derive_reversed(
        assumptions=[SetNotEquiv(Set(one, two , three), Set(a, b, c))])
 ⊢  
In [42]:
# We can use standard pre-defined sets as well
SetNotEquiv(A, Real).derive_reversed(assumptions=[SetNotEquiv(A, Real)])
 ⊢  
In [43]:
# We must already know or assume that the SetNotEquiv holds in one direction
try:
    SetNotEquiv(Set(one, two , three), Set(a, b, c)).derive_reversed()
    assert False, "Should not make it this far!"
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: Proof step failed:
Attempting to instantiate |- forall_{A, B | A not_equiv B} (B not_equiv A) with {A: {1, 2, 3}, B: {a, b, c}}:
Unsatisfied condition: {1, 2, 3} not_equiv {a, b, c}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Testing the SetNotEquiv.definition() method

The definition() method has the following format:

definition(**defaults_config):

and returns (A not_equiv B) = Not(A equiv B) starting with self (A not_equiv B).

In [44]:
SetNotEquiv(A, B).definition()
 ⊢  
In [45]:
# Notice the definition does not depend on the Truth of the SetNotEquiv claim:
SetNotEquiv(Set(one, two, three), Set(one, two, three)).definition()
 ⊢  
In [46]:
# Notice the definition does not depend on the Truth of the SetNotEquiv claim,
# nor on any assumptions supplied:
SetNotEquiv(Set(one, two, three), Set(a, b, c)).definition(assumptions=[Equals(a, one)])
 ⊢  

Testing the SetNotEquiv.unfold() method

The unfold() method has the following format:

unfold(**defaults_config):

and attempts to derive and return Not(SetEquiv(A, B)) from known or assumed SetNotEquiv(A, B).

In [47]:
SetNotEquiv(A, B).unfold(assumptions=[SetNotEquiv(A, B)])
 ⊢  
In [48]:
SetNotEquiv(Set(one, two , three), Set(a, b, c)).unfold(
        assumptions=[SetNotEquiv(Set(one, two , three), Set(a, b, c))])
 ⊢  
In [49]:
# We can use standard pre-defined sets as well
SetNotEquiv(B, Real).unfold(assumptions=[SetNotEquiv(B, Real)])
 ⊢  
In [50]:
# We must already know or assume that the SetNotEquiv holds in one direction
try:
    SetNotEquiv(Set(one, two , three), Set(a, b, c)).unfold()
    assert False, "Should not make it this far!"
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: Proof step failed:
Attempting to instantiate |- forall_{A, B | A not_equiv B} [not](A equiv B) with {A: {1, 2, 3}, B: {a, b, c}}:
Unsatisfied condition: {1, 2, 3} not_equiv {a, b, c}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Testing the SetNotEquiv.conclude_as_folded() method

The conclude_as_folded() method has the following format:

conclude_as_folded(**defaults_config):

and attempts to conclude the NotSetEquiv(A, B) from the known or assumed Not(SetEquiv(A, B)).

In [51]:
SetNotEquiv(A, B).conclude_as_folded(assumptions=[Not(SetEquiv(A, B))])
 ⊢  
In [52]:
SetNotEquiv(Set(one, two, three), Set(two, three, a)).conclude_as_folded(
        assumptions=[Not(SetEquiv(Set(one, two, three), Set(two, three, a)))])
 ⊢  

Testing the SetNotEquiv.derive_contradiction() method

The derive_contradiction() method has the following format:

derive_contradiction(**defaults_config):

and from A not_equiv B, and assuming (A equiv B), derives and returns FALSE.

In [53]:
SetNotEquiv(A, B).derive_contradiction(assumptions=[SetEquiv(A, B), SetNotEquiv(A, B)])
,  ⊢  
In [54]:
SetNotEquiv(Set(one, two, three), Set(two, three, a)).derive_contradiction(
        assumptions=[SetNotEquiv(Set(one, two, three), Set(two, three, a)),
                     SetEquiv(Set(one, two, three), Set(two, three, a))])
,  ⊢  

Testing the SetNotEquiv.deduce_in_bool() method

The deduce_in_bool() method has the following format:

deduce_in_bool(**defaults_config):

and attempts to deduce and return that this SetNotEquiv claim is in the Boolean set.

In [55]:
SetNotEquiv(Set(one, two, three), Set(two, three, one)).deduce_in_bool()
 ⊢  
In [56]:
SetNotEquiv(Set(one, two, three), Set(four, five)).deduce_in_bool()
 ⊢  
In [57]:
SetNotEquiv(Set(one, two, three), Set(two, three, a)).deduce_in_bool(assumptions=[Equals(a, one)])
 ⊢  
In [58]:
%end demonstrations