Proving an instance of a statement without knowing its name #20
Description
Hi @tirix , so I have this problem. Say, I want to prove this statement:
dfuni_ins $p |- U. { y | { x | ph } = { y } } = { z | E. w ( z e. w /\ w e. { y | { x | ph } = { y } } ) } $= ? $.
It looks long and complicated, but it's just an instance of df-uni. So, in Rumm it can easily be proved by just doing { apply ~df-uni }. The issue is, I don't know that the name is ~df-uni at the time I have to prove this goal.
The original idea was to use the finddf tactics to match the goal with its definition (which is unique). The issue is that Rumm seems to only find "exact matches" and not instances of those matches. Is there another way to do this that maybe I'm missing?
If I try to prove the exact statement of ~df-uni, it correctly finds it:
proof ~df-uni { finddf ! goal ! }
Proof for "df-uni":
Proving |- U. A = { x | E. y ( x e. y /\ y e. A ) }
>> Find |- U. A = { x | E. y ( x e. y /\ y e. A ) }
Found match with df-uni
Unification success
subgoal = |- U. A = { x | E. y ( x e. y /\ y e. A ) }
Proving |- U. A = { x | E. y ( x e. y /\ y e. A ) }
>> !
<< Matched subgoal!
<< Find Successful!
Success
qed::df-uni |- U. A = { x | E. y ( x e. y /\ y e. A ) }
$= ( df-uni ) ABCD $.
$)
Done.
However, if I try to prove the ~dfuni_ins showed above then it doesn't:
proof ~dfuni_ins { finddf ! goal ! }
Proof for "dfuni_ins":
Proving |- U. { y | { x | ph } = { y } } = { z | E. w ( z e. w /\ w e. { y | { x | ph } = { y } } ) }
>> Find |- U. { y | { x | ph } = { y } } = { z | E. w ( z e. w /\ w e. { y | { x | ph } = { y } } ) }
<< Find: No match found
Failure
Just for verification purposes, I tested that { apply ~df-uni } works for proving ~dfuni_ins:
proof ~dfuni_ins { apply ~df-uni }
Proof for "dfuni_ins":
Proving |- U. { y | { x | ph } = { y } } = { z | E. w ( z e. w /\ w e. { y | { x | ph } = { y } } ) }
>> Apply df-uni
Attempting apply df-uni
<< Apply Unification success
Success
qed::df-uni |- U. { y | { x | ph } = { y } } = { z | E. w ( z e. w /\ w e. { y | { x | ph } = { y } } ) }
$= ( cab cv csn wceq df-uni ) DEABFCGHICFJ $.
$)
Done.
The context
It might be useful to show in which context this feature is needed. Say, we want to prove the justification theorem of df-iota, which is iotajust:
iotajust $p |- U. { y | { x | ph } = { y } } = U. { z | { x | ph } = { z } } $= ? $.
The first step is to apply unieqi, however we might not have equality and cbv* theorems for every definition. So, say we don't have unieqi in the database, what do we do instead? The answer I came up with is: we expand the definition df-uni and check equality and cbv* theorems of a more primitive expression. The tactics sequence that I had in mind to perform such expansion is the following:
tactics expand ()
{ match goal
$ A = B $
{ finddf ! $ A = C $
{ finddf ! $ B = D $
{ apply ~3eqtr4i ? ! ! with ~cA $ C $ ~cB $ D $ }
}
}
}
proof ~iotajust { use expand }
The metavariable A captures U. { y | { x | ph } = { y } }, while the metavariable B captures U. { z | { x | ph } = { z } }. The finddf tactics would find the definition that has U. { y | { x | ph } = { y } } on the LHS and a misterious expression on the RHS captured by C. Once finddf unifies the goal with ~df-uni (restricting unification to definitions makes the match unique) then the misterious expression held by C becomes known, and therefore it can be used by the with keyword.
This is the "crucial step" that makes the justification theorem prover work in general. If it cannot find a cbv* theorem or an equality theorem for a particular syntax, it expands the definition into a more primitive syntax and check cbv* theorems or equality theorems of that more primitive syntax.