今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。
この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合、その変数や中身の式を証明することができません。そこで多くの場合には全称量化子 ∀を外してその中身にアクセスできるようにすることが証明の第一歩となります。
全称量化子 ∀がゴールの論理式に登場している場合、introタクティクを使うとその変数がラベル付きで導入されて、以降の証明で使えるようになります。
例えば前回見たcalcモードの説明の記事では偶関数と奇関数を定義して、２つの奇関数の積が偶関数になることの証明を見ました。ゴールの論理式である「積が偶関数」という命題は展開すると全称量化子が出てきます。introタクティクを使うとこの全称量化子が取れた式が新たなゴールとなり、仮定には全称量化子の対象であった変数がintroで指定した名前（普通は同じ名前を指定します）で付け加えられます。
def FnEven (f : ℝ → ℝ) : Prop :=
∀ x, f x = f (-x)example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
intro x'
…
このintro x'を入力するとゴールが以下のように変化することがわかります。
⊢ FnEven fun x => f x * g x
が以下に変化する。
⊢ (fun x => f x * g x) x' = (fun x => f x * g x) (-x')
FnEvenが展開されて、その全称量化子の変数xが展開式ではintroで指定したx'として現れています。以降の証明をこのx'を使いながら進めることができます。
導入された変数x'を含むゴールの論理式を、変数x'に関する新たな条件を導入することなく証明できれば、全てのx'について証明ができたことになります。
