Что это значит, когда Coq расширяет функцию как часть цели? - PullRequest
Новая
       7

Что это значит, когда Coq расширяет функцию как часть цели?

0 голосов
/ 24 января 2019

Я пытался решить следующую теорему и застрял на последнем simpl.: 

Lemma nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  intros l1 l2. induction l1 as [| n' l' IHl'].
  -simpl. reflexivity.
  -simpl. 
Qed.

в этот момент Coq меняет цель с: 

1 subgoal (ID 170)

  n' : nat
  l', l2 : natlist
  IHl' : nonzeros (l' ++ l2) = nonzeros l' ++ nonzeros l2
  ============================
  nonzeros ((n' :: l') ++ l2) = nonzeros (n' :: l') ++ nonzeros l2

до: 

1 subgoal (ID 185)

  n' : nat
  l', l2 : natlist
  IHl' : nonzeros (l' ++ l2) = nonzeros l' ++ nonzeros l2
  ============================
  match n' with
  | 0 => nonzeros (l' ++ l2)
  | S _ => n' :: nonzeros (l' ++ l2)
  end =
  match n' with
  | 0 => nonzeros l'
  | S _ => n' :: nonzeros l'
  end ++ nonzeros l2

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

Контекст вопроса:

Кто-то сказал мне, что решение: 

Lemma nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  intros l1 l2. induction l1.
  - simpl. reflexivity.
  - simpl. { induction n.
             - ...
             - ... }
Qed.

, что заставило меня захотеть понять, почему они используют индукцию на n, поскольку мне кажется, что никогда не пришло бы в голову использовать индукцию там. Поэтому я спрашиваю, почему? Но я понял, что прежде чем я мог спросить, почему я даже не понимал состояние доказательства до этого, поскольку казалось, что он просто копирует, вставляет функцию в состояние проверки (что для меня не имеет смысла). Поэтому, прежде чем я спросил, зачем использовать индукцию там, я должен спросить, что говорит до этого доказательство, может быть, это поможет понять, почему индукция на n.

1 Ответ

0 голосов
/ 29 января 2019

Я предполагаю, что вы определили nonzeros следующим образом (или аналогично): 

Require Import List.
Import ListNotations.


Definition natlist := list nat.

Fixpoint nonzeros (l : natlist) :=
  match l with
  | [] => []
  | 0 :: xs => nonzeros xs
  | x :: xs => x :: nonzeros xs
  end.

Так что nonzeros рекурсивно со структурным уменьшением на l. Тактика Coq simpl использует эвристику, в которой она раскрывает определения точек фиксации, если они применяются к термину, в котором в качестве символа головы используется конструктор. В вашем случае, например, nonzeros (n' :: l'), за константой nonzeros следует термин, образованный конструктором, Cons (= ::). Coq выполняет так называемое «дельта-сокращение», заменяя вхождение nonzero его определением. Поскольку это определение match, вы получите match в качестве нового термина. Дальнейшие замены немного упрощают это, но не могут устранить два случая: один для нулевой головки и один для ненулевой головки.

То же самое происходит с вхождением nonzeros ((n' :: l') ++ l2), которое сначала упрощается до nonzeros (n' :: (l' ++ l2)), так что снова аргументом является аргумент Cons.

Если вы хотите избежать предоставления выражений match при упрощении, вы можете поместить следующую директиву после определения nonzeros: 

Arguments nonzeros l : simpl nomatch.

Это конкретно говорит simpl, чтобы не расширять термин, если это в конечном итоге выставит match в месте изменения.

Что касается induction, используемого вашим другом здесь: оно применяется для принудительного разделения случая на n', так что каждый случай (n' = 0, n' = S _) может обрабатываться отдельно. Действительно, индукция здесь не нужна. Простое разделение регистра (case n') сделает то же самое.

...