Ich habe Schwierigkeiten, eine Taktik zu definieren, Hypothesen in einem Beweiskontext rekursiv umzukehren. Nehmen wir zum Beispiel an, dass ich einen Beweiskontext habe, der eine Hypothese wie folgt enthält:
%Vor%und möchte die Hypothese wiederholt invertieren, um einen Beweiskontext zu erhalten, der die Hypothesen enthält
%Vor%Natürlich ist es einfach, diesen Beweiskontext zu erhalten, indem man die Inversionstaktik wiederholt anwendet. Manchmal werden jedoch bei der Umkehrung einer Hypothese verschiedene Hypothesen in verschiedene Teilziele eingefügt, und ob die Invertierung jeweils von der Art der Information abhängt, die durch Inversion bereitgestellt wird.
Das offensichtliche Problem besteht darin, dass unterschiedsloses Mustervergleich mit dem Beweiskontext zu einer Nicht-Beendigung führt. Zum Beispiel funktioniert das Folgende nicht, wenn man die ursprünglichen Hypothesen nach dem Invertieren behalten möchte:
%Vor%Gibt es einen einfachen Weg, dies zu tun? Die naheliegende Lösung wäre, einen Stapel bereits invertierter Hypothesen zu behalten. Eine andere Lösung besteht darin, Hypothesen nur bis zu einer bestimmten Tiefe zu invertieren, was rekursive Aufrufe in Ltac entfernen würde.
Wenn das wirklich das ist, was Sie tun wollen, dann vermute ich, dass Sie zuerst einen Helfer Fixpoint subtreelist (st : searchtree): list (...) beweisen wollen, der eine Liste all dieser Unterbäume zurückgibt, und dann eine Taktik, die subtreelist und rekursiv destruct s die Liste aufruft bis Sie alle zusätzlichen Hypothesen haben, die Sie wollen.
Viel Glück damit!