{предположение, применить интро} достаточно для минимального реквизита логики

Question

Я прочитал, что множество {assumption, apply, intro} тактики от Ltac достаточно, чтобы доказать любую тавтологию в минимальной конструктивной логике.

Я полагаю, что пера и бумага доказательства этого утверждения делается индукцией по синтаксису тавтологии, показывая, что 3 тактика может строить постепенно термин, который представляет тавтологию.

Мне интересно узнать, возможно ли альтернативное доказательство внутри Возможно использование Coq с использованием Ltac или другого метаязыка.

Это означало бы, что Ltac или альтернативный метаязык могут отражать то, что действительно делают эти тактики, и могут манипулировать ими как переменные.

Меня очень интересует положительный ответ в этом направлении, даже если он немного надуман.

Answer 1

Собственно, всего apply достаточно. Просто примените доказательство с правильным типом. Или быть очень худыми, не используйте Ltac вообще, просто назначить пробный член с

Определения имени: < предложения>: = < доказательством термина>.

Пример:

Lemma has_next : forall n, exists n', S n = n'. 
Proof. 
    intro n. 
    exists (S n). 
    reflexivity. 
Qed. 

может быть "доказано", давая доказательство термин непосредственно.

Definition has_next : forall n, exists n', S n = n' := fun n => ex_intro _ (S n) eq_refl. 

Вы знаете, нет ничего магического о Ltac команд. Это всего лишь инструменты, которые позволяют постепенно создавать термин «доказательство», но вы можете предоставить весь срок действия в один конец, если вы хотите использовать как можно меньше тактики.

«Доказательство» проистекает из того факта, что вы показали, что действительно существует доказательство с требуемым типом (предложение). И тип Coq - проверяет этот термин для вас, чтобы убедиться, что этот термин действительно имеет этот тип.

Coq даже не заботится о том, как этот термин был построен - по божественному прозрению или от частично багги-программы, если проверка типа термина.