Assumption derivation steps going from iteration to iteration instance

[wwitzel]

In helping Jamie with the disjunction closure theorem, we ran across an issue that I hadn’t previously appreciated. Dealing with iterations as assumptions brings in some new situations that need to be thought through carefully. I think I know how we’ll want to deal with these issues, but wanted to solicit feedback for reassurance or redirection.

Consider the following as an assumption: A1 in Booleans, …, A{m+1} in Booleans

This seems straightforward. But let’s say that, as it so happens in our case with the disjunction closure proof, what we really need for the desired chain of logic is to split this into

A1 in Booleans, …, A{m} in Booleans

and

A_{m+1} in Booleans

That is, we have proven the things that we need under these assumptions, and we need to prove those assumptions (with our first assumption, say) to eliminate them. Well, it seems sensible to be able to prove

{m in Naturals, A1 in Booleans, …, A{m+1} in Booleans} |- A1 in Booleans, …, A{m} in Booleans

for example. But this is a little bit odd. On the right side is an iteration, not a single truth. It is a single Iter expression but that Iter expression represents a range of things. Perhaps, when our truth is an Iter, we display it wrapped in curly braces:

{m in Naturals, A1 in Booleans, …, A{m+1} in Booleans} |- {A1 in Booleans, …, A{m} in Booleans}

That should be easy to do and maybe that is best. Now, we need a mechanism to prove this. I’m thinking that we extend the capabilities of the “Assumption” derivation step to enable this sort of thing as well as

{m in Naturals, A1 in Booleans, …, A{m+1} in Booleans} |- A_{m+1} in Booleans

The “Assumption” derivation step should allow us to trivially prove

{A1 in Booleans, …, A{m+1} in Booleans} |- {A1 in Booleans, …, A{m+1} in Booleans}

But I’m thinking that we add the capability to derive a subset of these assumptions by simply specifying an index or index range.

I think I see a clear path, as described above, that is consistent with “The Prove-It Way”. Let me know if you have any objections.

[wwitzel]

Taking a step back, it would be generally useful to equate different forms of iterations, split or merged, and substitute these in where possible. This also comes up in the latest comment in Issue #6 where I mentioned using such equivalences in the requirements when substituting iterations into iterations and it must be split. It might make sense to have the following axiom: \forall_{n \in Naturals} \forall_{A} A_1, ..., A_{n+1} = A_1, ..., A_n, A_{n+1} However, this doesn't quite work. The left side is just a single iteration. The right side is two items which would have to be place inside an ExprTuple. So properly, we'd want to wrap both sides in an ExprTuple to give \forall_{n \in Naturals} \forall_{A} (A_1, ..., A_{n+1}) = (A_1, ..., A_n, A_{n+1}) But then, this isn't so useful. It doesn't allow substitution within an ExprTuple containing other items. We could allow that with a statement like

\forall_{i,j,k \in Naturals} \forall_{A,B,C} 
    (A_1, ..., A_i, B_1, ..., B_{j+1}, C_1, ..., C_k)
     = (A_1, ..., A_i, B_1, ..., B_j, B_{j+1}, C_1, ..., C_k) 

But that is a bit cumbersome.

Instead, we could do something like \forall_{n \in Naturals} \forall_{A} ...,A_1, ..., A_{n+1}, ... = ..., A_1, ..., A_n, A_{n+1}, ... This would require a new type of Expression wrapping the left and right sides separately. Maybe we could call it PartialTuple. When a PartialTuple is substituted into an ExprTuple, it would embed its contents into the containing ExprTuple and the PartialTuple wrapper would be eliminated.

So that might be a good approach, but I have not yet addressed what we do with iteration assumptions. I will post this comment for now and start another comment to try to address the iteration assumption question.

[wwitzel]

Here's one idea. We could add the following axiom: \forall_{n \in NaturalPos} \forall_{A | A_1, ..., A_n} A_1 and ... and A_n as well as \forall_{n \in NaturalPos} \forall_{A | A_1 and ... and A_n} A_1, ... , A_n that would allow us to go back and forth between the conjunctive form and the list form. In the conjunctive form, it is really embedded in an ExprTuple within And. That is, A_1 and ... and A_n is really And[ExprTuple[A1, ..., An]]. So, in that form we can use the substitutions described above via PartialTuple. Then we could do the following steps:

|- \forall_{n \in NaturalPos} \forall_{A | A_1, ..., A_n} A_1 and ... and A_n
{(m+1) in NaturalsPos, A_1, ..., A_{m+1}} |- A_1 and ... and A_{m+1}
|- \forall_{n \in Naturals} \forall_{A} ...,A_1, ..., A_{n+1}, ... = ..., A_1, ..., A_n, A_{n+1}, ...
{(m+1) in NaturalsPos, A_1, ..., A_{m+1}} |- A_1 and ... and A_m and A_{m+1}
{(m+1) in NaturalsPos, A_1, ..., A_{m+1}} |- (A_1 and ... and A_m) and A_{m+1}
{(m+1) in NaturalsPos, A_1, ..., A_{m+1}} |- A_1 and ... and A_m
{(m+1) in NaturalsPos, A_1, ..., A_{m+1}} |- A_{m+1}
{(m+1) in NaturalsPos, A_1, ..., A_{m+1}} |- A_1, ..., A_m

Something like that.

[wwitzel]

I've also been thinking about the 2D version of PartialTensor -- PartialArray. I think the best way is to treat a single axis at a time. That way, we'd maintain a rectilinear grid for the ExprArray's. So then each PartialArray would have a specified axis and have axioms like

\forall_{m, n in Naturals} \forall_{A}

    ... A_{1,1} ... A_{1,n+1} ...           ... A_{1,1} ... A_{1,n} A_{1,n+1} ...
           :             :           =            :            :       :
    ... A_{m,1} ... A_{m,n+1} ...           ... A_{m,1} ... A_{m,n} A_{m,n+1} ...

as an example in the horizontal direction. And there would be an analogous axiom with a PartialArray in the vertical direction.

[wwitzel]

Regarding the PartialTuple idea above, it is somewhat flawed. To illustrate the problem, you should be able to say something like \forall_{x, y, z} |(x, y, z)| = 3 but then, substituting, say, y for a PartialTuple ..., q, r, s, ..., would result in the erroneous statement |(x, q, r, s, z)| = 3 (I had a similar realization when thinking about ways to deal with allowing conditions to be expanded).

We don't need the PartialTuple strategy. We could use the "cumbersome" version from above: \forall_{i,j,k \in Naturals} \forall_{A,B,C} (A_1, ..., A_i, B_1, ..., B_{j+1}, C_1, ..., C_k) = (A_1, ..., A_i, B_1, ..., B_j, B_{j+1}, C_1, ..., C_k) That may be best because it is explicit. If we do decide to do something like PartialTuple, it would need to work in a "handshake" kind of way -- that is, you are substituting a PartialTuple into something that is explicitly made to accept a PartialTuple. That could be a possibility if we can come up with nice notation, but right now I'm thinking the "cumbersome" way may be the right way.

[wwitzel]

Regarding 2D, I have new thoughts involving ExprTuples of ExprTuples and Iters of Iters which I will expound upon in Issue #6 .

[wwitzel]

Here's another way to do what the PartialTuple was meant to accomplish. Have an iterReplacement axiom: forall{i, j, k in Naturals} [forall{a_1,...,a_i, c_1,...,ck} [forall{b, d} (((b_1 , ... , b_j) = (d_1 , ... , d_j)) => ((a_1 , ... , a_i , b_1 , ... , b_j , c_1 , ... , c_k) = (a_1 , ... , a_i , d_1 , ... , d_j , c_1 , ... , c_k))) ]]

Then we can make the simple (less cumbersome) tuple equations and then use this axiom, or theorems derived from it, to make replacements within an ExprTuple.

[wwitzel]

iteration_axioms.pdf This is a first attempt at some iteration axioms.

[wwitzel]

Actually, rather than adding the iterReplacement, I'm thinking we can use multiSubstitution. Something like: \forall{n \in N+} \forall{f, x, y | |x|=|y|=n, x=y} f(x_1, ..., x_n) = f(y_1, ..., y_n) We had a long discussion on this last July and concluded that we could just do it as regular substitution of a tuple. But it is not the same! This kind of substitution should allow the substituted a portion of an ExprTuple like what iterReplacement is trying to accomplish. But it would be done without adding an axiom and would be more powerful. It would be utilizing operation substitution using a multi-parameter lambda expression (which probably has not been tested). So, in principle, you could perform the substitution within different kinds of tuples simultaneously. For example, f : x_1, ..., x_n |-> (a + x_1 + ... + x_n) / (x_1 ... x_n b) and transform this to (a + y_1 + ... + y_n) / (y_1 ... y_n b)

Anyway, this is getting off-topic relative to "iteration assumptions", so I've started Issue #102, reiterating this latest comment. I'll continue the discussion pertaining more specifically to "iteration assumptions" below.

[wwitzel]

I am realizing a potential issue with the proposed "iterTruthDef" in iteration_axioms.pdf that was attached a couple of comments ago. For the same reason, I also object to allowing an assumption derivation step applied to an iteration: {A_1, ..., A_n} |- A_1, ..., A_n Specifically, by allowing an iteration to be a "truth", you can prove that the iteration is equal to TRUE which means that it can be substitution with TRUE: {A_1, ..., A_n} |- A_1, ..., A_n = TRUE But that is not right and could lead to problems. Instead, I'm thinking that the right approach is to internally use a conjunction as the assumption when you have an iteration but display it as a list for convenience. That is, "A_1 and ... and A_n" is the actual assumption but we use "A_1, ..., A_n" as the shorthand. This is similar to the idea proposed for conditions in Issue #32.

But to be more precise, we will still have a list of assumptions for convenience, but when an iteration is included in the list it will be encapsulated in a conjunction. For example, {A_1, ..., A_n, B} |- A_1 and ... and A_n and B would be internally treated as having two assumptions: {A_1 and ... and A_n, B} |- A_1 and ... and A_n and B but appear as the former.

[wwitzel]

Handled with significant-core-updates merger.