shortest path algorithm to find derivation

[wwitzel]

trafficstars

Prove-It currently fails in the following example (a simplified version of something we encountered during a meeting to help Jamie prove proveit.number.sets.integer.successiveNats, if I remember correctly):

In [1]: from proveit.common import A, B, C, D from proveit.logic import Implies, Equals AeqB, CeqD, BimplC = Equals(A, B), Equals(C, D), Implies(B, C)

Out [1]: AeqB : A = B CeqD : C = D BimplC : B => C

In [2]: C.prove([B, BimplC])

Out [2]: {B, B => C} |- C

In [3]: CeqD.deriveRightViaEquivalence([B, BimplC, CeqD])

Out [3]: {B, B => C, C = D} |- D

In [4]: AeqB.deriveRightViaEquivalence([A, AeqB])

Out [4]: {A, A = B} |- B

In [5]: D.prove([A, AeqB, BimplC, CeqD])

Out[5]: ProofFailure

All the pieces are there, but Prove-It is not currently designed to automatically put them together. We can fix this manually by revisiting the "In [3]" step with different assumptions:

In [6]: CeqD.deriveRightViaEquivalence([A, Aeq, BimplC, CeqD])

Out [6]: {A, A = B, B => C, C = D} |- D

In [7]: D.prove([A, AeqB, BimplC, CeqD])

Out [7]: {A, A = B, B => C, C = D} |- D