Coq auto tacit c не работает

Question

У меня есть следующая программа Coq, которая пытается доказать n <= 2^n с помощью auto:

(***********)
(* imports *)
(***********)
Require Import Nat.

(************************)
(* exponential function *)
(************************)
Definition f (a : nat) : nat := 2^a.

Hint Resolve plus_n_O.
Hint Resolve plus_n_Sm.

(**********************)
(* inequality theorem *)
(**********************)
Theorem a_leq_pow_2_a: forall a, a <= f(a).
Proof.
  auto with *.
Qed.

Я ожидал, что Coq либо преуспеет, либо застрянет, пытаясь сделать это. Но тут же возвращается. Что я делаю не так?

EDIT Я добавил Hint Unfold f. и увеличил привязку до 100, но я не вижу разворачивания, выполненного с помощью debug auto 100:

(* debug auto: *)
* assumption. (*fail*)
* intro. (*success*)
* assumption. (*fail*)
* intro. (*fail*)
* simple apply le_n (in core). (*fail*)
* simple apply le_S (in core). (*fail*)

РЕДАКТИРОВАТЬ 2 Я добавляю ручное доказательство, чтобы продемонстрировать его сложность:

(**********************)
(* inequality theorem *)
(**********************)
Theorem a_leq_pow_2_a: forall a, a <= f(a).
Proof.
  induction a as[|a' IHa].
  - apply le_0_n.
  - unfold f.
    rewrite Nat.pow_succ_r.
    * rewrite Nat.mul_comm.
      rewrite Nat.mul_succ_r.
      rewrite Nat.mul_1_r.
      unfold f in IHa.
      rewrite Nat.add_le_mono with (n:=1) (m:=2^a') (p:=a') (q:=2^a').
      -- reflexivity.
      -- apply Nat.pow_le_mono_r with (a:=2) (b:=0) (c:=a').
         auto. apply le_0_n.
      -- apply IHa.
    * apply le_0_n.
Qed.

Answer 1

Выполненное вами ручное доказательство объясняет, почему auto не может этого сделать. Вы провели доказательство по индукции, а затем несколько раз переписали. auto tacti c не позволяет себе такой шаг.

tacti c auto предназначен для поиска доказательства, если для ручного доказательства используется только apply с ограниченным набором теорем. Здесь ограниченный набор теорем взят из базы подсказок core. Для краткости предположим, что эта база данных содержит только le_S, le_n, plus_n_O и plus_n_Sm.

Для упрощения предположим, что мы работаем с целью a <= 2 ^ a. Главный предикат этого утверждения - _ <= _, поэтому tacti c будет рассматривать только теоремы, основное утверждение которых выражено с помощью _ <= _. Это исключает plus_n_O и plus_n_Sm. Ваша инициатива по их добавлению идет насмарку.

Если мы посмотрим на le_n, выражение будет forall n : nat, n <= n. Если мы заменим универсальную количественную оценку переменной шаблона , этот шаблон будет ?1 < ?1. Объединяется ли это с a <= 2 ^ a? Ответ - нет. поэтому эта теорема не будет использоваться auto. Теперь, если мы посмотрим на le_S, образец главного оператора будет ?1 <= S ?2. Если объединить этот шаблон с a <= 2 ^ a, это потребует, чтобы ?1 было a. Каким может быть значение ?2? Нам нужно символически сравнить выражения 2 ^ a и S ?2. С левой стороны символ функции - _ ^ _ или 2 ^ _, в зависимости от того, как вы sh смотрите на него, но в любом случае это не S. Итак, auto распознает, что эти функции не совпадают, лемма неприменима. auto терпит неудачу.

Я повторяю: когда ставится цель, auto сначала смотрит только на главный символ цели и выбирает из своей базы данных теоремы, которые позволяют получить доказательства для этого главного символа. В вашем примере символ головы - _ <= _. Затем он смотрит только на заключение этих теорем и проверяет, соответствует ли заключение синтаксически поставленной цели. Если он действительно совпадает, то это должно предоставить значения для универсально определяемых количественных переменных теоремы, а предпосылки теоремы - это новые цели, которые следует решать на более низком уровне. Как было упомянуто @Elazar, глубина по умолчанию ограничена 5.

Директива Hint unfold будет полезна, только если вы сделали определение следующей формы:

Definition myle (x y : nat) := x <= y.

Тогда Hint Unfold myle : core. было бы полезно убедиться, что теоремы базы данных для _ <= _ также используются для доказанных экземпляров myle, как в следующем примере (он не работает, если у нас есть 4 вхождения S, из-за ограничение глубины).

Lemma myle3 (x : nat) : myle x (S (S (S x))).
Proof. auto with core.  Qed.

Обратите внимание, что следующее утверждение логически эквивалентно (согласно определению сложения), но не доказуемо с помощью auto. Даже если вы добавите Hint unfold plus : core. в качестве директивы, это не поможет, потому что plus не является главным символом цели.

Lemma myleplus3 (x : nat) : myle x (3 + x).
Proof.
auto. (* the goal is unchanged. *)
simpl. auto.
Qed.

Я часто использую автоматические c тактики от Coq, для instance lia, но я всегда так делаю, потому что могу предсказать, является ли цель частью предполагаемой области действия tacti c.

Answer 2

Из документации :

Этот tacti c реализует процедуру разрешения, подобную Prolog, для решения текущей цели. Сначала он пытается решить цель, используя предположение tacti c, затем сводит цель к цели atomi c с помощью вступлений и вводит вновь сгенерированные гипотезы в качестве подсказок. Затем он просматривает список тактик, связанных с главным символом цели, и пытается применить одну из них (начиная с тактики с меньшими затратами). Этот процесс рекурсивно применяется к сгенерированным подцелям.

Также см. Предупреждение:

auto использует более слабую версию apply, которая ближе к простому применению поэтому ожидается, что иногда автоматическая функция не работает, даже если применение одной из подсказок будет успешным.

И, наконец, глубина поиска по умолчанию ограничена 5; вы можете управлять им, используя auto num.

. Таким образом, если в любой момент ни одна из «тактик, связанных с символом головы» текущей цели не добьется никакого прогресса, auto не удастся. И если auto достигнет максимальной глубины, это не удастся.

Обратите внимание, что auto не применяет автоматически unfold tacti c. Невозможно решить a <= f(a), если f непрозрачно, без дополнительных предположений. Если хотите, можете использовать Hint Unfold f или Hint Transparent f.