В Isabelle2015 упрощающий знает ряд правил для исключения экзистенциально связанных переменных, определяемых равенством. Для вашего случая актуальны simp_thms(36-40):
(∃x. ?P) ⟷ ?P∃x. x = ?t∃x. ?t = x(∃x. x = ?t ∧ ?P x) ⟷ ?P ?t(∃x. ?t = x ∧ ?P x) ⟷ ?P ?t
Кроме того, ex_simps(1-2) подталкивает экзистенциалы к конъюнктам, если одна сторона не упоминает связанную переменную:
(∃x. ?P x ∧ ?Q) ⟷ (∃x. ?P x) ∧ ?Q(∃x. ?P ∧ ?Q x) ⟷ ?P ∧ (∃x. ?Q x)
Во многих случаях этих правил достаточно, чтобы исключить квантор существования. В вашем случае, однако, есть дополнительные кванторы существования для xs и ys между ними. В принципе, приведенных выше правил и ex_comm, т. е. (∃x y. ?P x y) ⟷ (∃y x. ?P x y) (и ассоциативности op &, но это в любом случае простое правило по умолчанию), достаточно, чтобы доказать вашу лемму, переписав ее. Однако нужно было бы вытащить экзистенциалы из конъюнктов, а затем переставить кванторы так, чтобы x было связано самым внутренним образом. Ни один из этих шагов не является желательным в общем случае. Более того, коммутативность подчиняется порядку терминов Изабель, поэтому упрощающий может даже не применять ее предполагаемым образом.
Таким образом, эта проблема не может быть решена в общем случае конечным набором правил перезаписи, поскольку вложений кванторов может быть сколь угодно много. Однако это может быть решено с помощью simproc, который срабатывает по кванторам существования и ищет в квантифицированном предикатном термине равенство связанной переменной. Если равенство оказывается в таком положении, что экзистенциальное может быть устранено, то оно должно тут же создать соответствующее правило перезаписи (для этого могут быть полезны преобразования).
Тем не менее, simproc должен убедиться, что он не слишком сильно нарушает структуру цели. Некоторые из таких нарушений уже можно увидеть в вашем примере. В левой части предикат Q не входит в область действия внутренних кванторов, но он находится в правой части.
Это означает, что неясно, желательно ли это преобразование во всех случаях. Например, в левой части классическое рассуждение, используемое auto, fastforce и т. д., может пройтись по одному квантору существования, а затем использовать классическое рассуждение, чтобы найти конкретизацию для x путем анализа Q. Это может привести к дальнейшему упрощению равенства x = f xs ys, что может привести к дополнительным конкретизациям. Напротив, в правой части рассудок сначала должен ввести две схематические переменные для кванторов существования, прежде чем он сможет даже начать смотреть на Q.
Таким образом, я рекомендую вам проанализировать вашу установку, чтобы увидеть, почему эта форма вложения квантификаторов вообще возникла в целевом состоянии. Может быть, вы можете настроить его так, чтобы все работало с существующим набором правил.
person
Andreas Lochbihler
schedule
15.10.2015
