[Coq] Coq Advent Calender : auto (2 of 25)

　Coq でよく使われる tactic の２つ目は auto です。

　Coq は簡単な証明は自動的に証明してくれる機能が幾つかありますが、auto はよく使われます。autoが何をやっているか知りたい場合は、autoの代わりにinfo autoと入力すると、autoの中で何をしてるかが判ります。Coqの初学者にはinfoは便利ですよ。

Coq < Lemma Sample_of_auto : forall A B:Prop, ((((A->B)->A)->A)->B)->B.
1 subgoal
  
  ============================
   forall A B : Prop, ((((A -> B) -> A) -> A) -> B) -> B

Sample_of_auto < auto.
Proof completed.

Sample_of_auto < Qed.
auto.

Sample_of_auto is defined

Coq <