If a definition has only "positive" clauses, meaning that the body of the definition consists of /\, \/, exists, =, and atoms, then there needs to be a tactic reduce that unfolds the definition eagerly on the left. This may loop if there is no fixed point, but that is fine. This would be roughly "level 0" of the Level 0/1 system.
Example: if we have
H : member F (a :: b :: nil)
then running reduce H should produce two subgoals, with F united with a in one and with b in the other. In case of a loop, we could bound reduce like with search: the invocation reduce 5 H would unfold the definition of member at most 5 times.
This is related to but different from #21.
The name reduce may not be the best option. A less contentious choice might be "async".
chaudhuri
commented
5 years ago
If a definition has only "positive" clauses, meaning that the body of the definition consists of
/\,\/,exists,=, and atoms, then there needs to be a tacticreducethat unfolds the definition eagerly on the left. This may loop if there is no fixed point, but that is fine. This would be roughly "level 0" of the Level 0/1 system.Example: if we have
then running
reduce Hshould produce two subgoals, withFunited withain one and withbin the other. In case of a loop, we could boundreducelike withsearch: the invocationreduce 5 Hwould unfold the definition ofmemberat most 5 times.This is related to but different from #21.
The name
reducemay not be the best option. A less contentious choice might be "async".Briefly discussed with @ThatDaleMiller.