deniok

У него там неонка дджин внутри. Тактика tauto доказывает пропозициональные тавтологии, монтируя лямбда-терм подходящего типа

Coq < Variables A B C : Prop.
A is assumed
B is assumed
C is assumed

Coq < Lemma he_he : (B -> C) -> (A -> B) -> A -> C.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (B -> C) -> (A -> B) -> A -> C

he_he < tauto.
Proof completed.

he_he < Qed.
 tauto.
he_he is defined

Coq < Print he_he.
he_he =
fun (H : B -> C) (H0 : A -> B) (H1 : A) =>
let H2 := H0 H1 in let H3 := H H2 in H3
     : (B -> C) -> (A -> B) -> A -> C

Здесь fun вместо лямбды и типизация связанных в лямбда-терме переменных явная, чёрчевская.

Но можно и примитивными тактиками intros; apply H; apply H0; assumption:( Read more... )Всякому видно, что при ручной работе и терм-композитор выходит кратким и выразительным, не то что эти вложенные let'ы ;-)