Как влияет следующая тактика на цель и предположения?Я знаю, что делает индукция по переменным и названная гипотеза, но неясно, что индукция по числу.
Induction 1
Из справочного руководства Coq: https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.induction
(...) induction num ведет себя как intros until num, за которым следует induction, примененное к последней введенной гипотезе.
induction num
intros until num
induction
И для intros until num: https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacv.intros
intros until num: повторяется введение до num -го независимого продукта. Пример На подцеле forall x y : nat, x = y -> y = x тактика intros until 1 эквивалентна intros x y H, поскольку x = y -> y = x является первым независимым продуктом. На подцели forall x y z : nat, x = y -> y = x тактика intros until 1 эквивалентно intros x y z, так как продукт на z можно переписать как независимый продукт: forall x y : nat, nat -> x = y -> y = x.
intros until num: повторяется введение до num -го независимого продукта.
num
На подцеле forall x y : nat, x = y -> y = x тактика intros until 1 эквивалентна intros x y H, поскольку x = y -> y = x является первым независимым продуктом.
forall x y : nat, x = y -> y = x
intros until 1
intros x y H
x = y -> y = x
На подцели forall x y z : nat, x = y -> y = x тактика intros until 1 эквивалентно intros x y z, так как продукт на z можно переписать как независимый продукт: forall x y : nat, nat -> x = y -> y = x.
forall x y z : nat, x = y -> y = x
intros x y z
z
forall x y : nat, nat -> x = y -> y = x
Для справки в индексе есть стандартная тактика.Руководство, в котором их легко найти: https://coq.inria.fr/distrib/current/refman/coq-tacindex.html
(там есть и другие индексы, которые могут вас заинтересовать).