Proof of proveit.logic.sets.inclusion.subset_eq_is_bool theorem

import proveit
from proveit import ExprTuple, IndexedVar, Function, Variable
from proveit import a, k, l, n, x, y, z, A, B, P, Q, Px, Qx
# from proveit.logic import iter_q1k_x_iter1l, x_iter1l
from proveit.numbers import zero, one, two, Natural, NaturalPos
from proveit.logic import And, Equals, Forall, InSet, TRUE, FALSE, Or, Boolean
from proveit.core_expr_types import x_1_to_n
from proveit.logic.sets.inclusion  import subset_eq_def
from proveit.logic.booleans.quantification.universality  import forall_in_bool
theory = proveit.Theory() # the theorem's theory

%proving subset_eq_is_bool

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
subset_eq_is_bool:
(see dependencies)

subset_eq_def

 ⊢  

subset_eq_def_inst = subset_eq_def.instantiate()

subset_eq_def_inst:  ⊢  

subset_eq_def_inst_rhs = subset_eq_def_inst.rhs

subset_eq_def_inst_rhs:

# this somehow loses the domain A for x
#subset_eq_def_inst_rhs.deduce_in_bool()

# addition 20200730 by wdc
InSet(Forall(x, InSet(x, B), domain=A), Boolean)

# addition 20200730 by wdc
# still loses the domain A for x
#Forall(x, InSet(x, B), domain=A).deduce_in_bool()

# subset_eq_def_spec_r_h_s.deduce_in_bool()

forall_in_bool

 ⊢  

forall_in_bool_inst = forall_in_bool.instantiate(
        {n:one, Px:InSet(x, B), x:ExprTuple(x)})

forall_in_bool_inst:  ⊢  

# from the original, kept here temporarily to guide update
# forall_in_bool_spec = forall_in_bool.instantiate({k:one, l:one, Px:InSet(x, B), QQ:[Q]}, relabel_map={xx:[x]})

# in proof.py we would likely use the same check_param_var method used in lambda_expr.py

forall_piece = forall_in_bool_inst.operands[0]

forall_piece:

x_1 = IndexedVar(x, one)

x_1:

# updated/adapted from original; not clear why this is being done
forall_piece.instantiate({x_1:ExprTuple(x)}, assumptions=[forall_piece])

 ⊢  

# recall:
forall_in_bool_inst

 ⊢  

# updated this from original; not clear why this is being done
the_inner_expr = forall_in_bool_inst.inner_expr()

the_inner_expr:

forall_in_bool_inst_expr = forall_in_bool_inst.expr

forall_in_bool_inst_expr:

# from original, but this no longer works:
# the_inner_expr.operands[1]

# from original, but no longer works:
# forall_in_bool_spec_expr.expr_info()

forall_in_bool_inst_expr.expr_info()

	core type	sub-expressions	expression
0	Operation	operator: 9 operands: 1
1	ExprTuple	2, 3
2	Operation	operator: 4 operand: 6
3	Literal
4	Literal
5	ExprTuple	6
6	Lambda	parameter: 11 body: 8
7	ExprTuple	11
8	Operation	operator: 9 operands: 10
9	Literal
10	ExprTuple	11, 12
11	Variable
12	Variable

# original
# Q1 = Variable('Q1');
# Q2 = Variable('Q2');
# forall_in_bool_spec_testing = forall_in_bool.instantiate({k:one, l:one, Px:InSet(x, B), QQ:[Q1]})

forall_in_bool

 ⊢  

# new version?
Q1 = Variable('Q1');
Q2 = Variable('Q2');
forall_in_bool_spec_testing = forall_in_bool.instantiate({n:one, Px:InSet(x, B), x:(Q1)})

forall_in_bool_spec_testing:  ⊢  

# original; can't seem to relabel now in this way? Even using
# a defined IndexedVar(Q1, one)
# forall_in_bool_spec_testing.relabel({Q1:Q2})

# forall_in_bool_spec_spec = forall_in_bool_spec.instantiate({xx:[x]})

# forall_in_bool_spec_spec_spec = forall_in_bool_spec_spec.instantiate({x_iter1l:[x]})

# original
# subset_eq_def_spec_r_h_s

# new
subset_eq_def_inst_rhs

# original
# subset_eq_def_spec_r_h_s.all_instance_vars()

# new
subset_eq_def_inst_rhs.all_instance_vars()

# original
# PxNew = Operation(P, [y, *subset_eq_def_spec_r_h_s.all_instance_vars(), z])

# new
PxNew = Function(P, [y, *subset_eq_def_inst_rhs.all_instance_vars(), z])

PxNew:

# original
# subset_eq_def_spec_r_h_s.instance_expr

# new
subset_eq_def_inst_rhs.instance_expr

# subset_eq_def_spec_r_h_s.deduce_in_bool()

#subset_eq_def_inst_rhs.deduce_in_bool()

# %qed