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:

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' < intros.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : B -> C
  H0 : A -> B
  H1 : A
  ============================
   C

he_he' < apply H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : B -> C
  H0 : A -> B
  H1 : A
  ============================
   B

he_he' < apply H0.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : B -> C
  H0 : A -> B
  H1 : A
  ============================
   A

he_he' < assumption.
Proof completed.

he_he' < Save.
intros.
apply H.
apply H0.
assumption.
he_he' is defined

Coq < Print he_he'.
he_he' =
fun (H : B -> C) (H0 : A -> B) (H1 : A) => H (H0 H1)
     : (B -> C) -> (A -> B) -> A -> C

Всякому видно, что при ручной работе и терм-композитор выходит кратким и выразительным, не то что эти вложенные let'ы ;-)