Доказательство импликации (a -> c) из (b -> c) данного отношения между a и b

Question

Я хочу доказать, что если одно из значений истинно (b --> c), то из этого следует, что некоторое другое значение также верно (a --> c), учитывая, что между a и * 1004 существует соответствующая связь *.

Вот конкретный пример с игрушкой, который я пытаюсь доказать:

theory Prop imports Main
begin

lemma 
  fixes func1 :: "'a => 'a"
    and func2 :: "'a => 'a"
    and func3 :: "'a => 'a"
  assumes "∀ x y. func1 x = func1 y --> func3 x = func3 y"
      and "∀ x. func1 x = func2 x"
  shows "∀ x y. func2 x = func2 y --> func3 x = func3 y"
proof -
  from assms show ?thesis by auto
qed

end

Доказательство не выполнено, Изабель 2018 продолжает работать, а часть "на авто" окрашена в фиолетовый цвет. Как мне доказать этот вид лемм?

Answer 1

Кажется, что ваша проблема делает цикл упрощения (который является частью auto). Я не понимаю почему, но такие вещи случаются время от времени.

Когда это происходит, иногда может помочь запустить try0 (который просто пробует пару распространенных автоматических методов проверки и возвращает те, которые успешны) или sledgehammer (который пытается перевести проблему в более простую форму и дать это сторонним проверяющим; если они могут доказать это, он затем пытается перевести доказательство обратно Изабель).

В этом случае и try0, и sledgehammer обнаруживают, что простой apply metis может выполнить эту работу. Такие методы, как auto и simp, делают много вещей, в том числе, в частности, «глупое» переписывание с заранее заданным набором правил. metis немного умнее того, что он делает, но вам нужно вручную указать ему каждый факт, который он должен использовать, и он менее адаптирован к Изабель / HOL.

Однако, поскольку эта проблема представляет собой простую логику первого порядка, metis может легко решить их самостоятельно без явных данных фактов, и ему удается избежать любой ловушки, вызывающей расхождение auto и simp.