Использование запоминания в индукции по высказыванию приводит к некорректной типизации ошибки в Coq.

Вот индуктивные и вычислительные определения четности натуральных чисел.

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

Definition even (n:nat) : Prop := 
  evenb n = true.

И доказательство того, что одно влечет за собой другое.

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
induction E as [ | n' E' ]. 
reflexivity. apply IHE'. Qed.

Сначала я не особо задумывался об этом доказательстве, но при более внимательном рассмотрении обнаружил, что кое-что беспокоит. Проблема в том, что после шага reflexivity я ожидаю увидеть контекст

1 subgoal
n' : nat
E : ev (S (S n'))
E' : ev n'
IHE' : ev n' -> even n'
====================================================================== (1/1)
even (S (S n'))

Но вместо этого я получаю

1 subgoal
n' : nat
E' : ev n'
IHE' : even n'
====================================================================== (1/1)
even (S (S n'))

Хотя теорема все еще доказуема как есть, тревожно видеть, как гипотезы таинственным образом исчезают. Я хотел бы знать, как получить контекст, на который я изначально рассчитывал. Из веб-поиска я понял, что это общая проблема индукции по построенным терминам в Coq. Одно из предлагаемых решений для SO предлагает использовать remember тактику для проверки гипотез. хранится. Но когда я пробую это в доказательстве,

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
remember E.
induction E as [ | n' E' ].

На шаге induction появляется следующее сообщение об ошибке.

Error: Abstracting over the term "n" leads to a term
"fun n : nat => forall e : ev n, e = E -> even n" which is ill-typed.

Что я не очень понимаю. Я думаю, что проблема в том, что E имеет свободную переменную, но в этом случае я бы застрял, поскольку невозможно ввести E, не вводя также n. (generalize dependent n обобщил бы E этим)

Есть ли способ получить изначально ожидаемый контекст?


induction coq
person user287393    schedule 28.06.2014    source источник
comment
Я не понимаю, почему вы ожидаете увидеть E : ev (S (S n')) и IHE' : ev n' -> even n'   -  person Konstantin Weitz    schedule 28.06.2014
comment
Неважно, я вижу, что вы правы и в том, и в другом.   -  person user287393    schedule 28.06.2014
comment
Если вы используете принцип индукции forall P, P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n, тогда ev будет встречаться в гипотезе индукции, как вы и ожидали. Принцип индукции для ev - ev_ind, который имеет тип forall P, P 0 -> (forall n, ev n -> P n -> P (S (S n))) -> forall n, ev n -> P n. При выполнении индукции для ev вы не должны ожидать, что ev будет предпосылкой гипотезы индукции, точно так же, как при выполнении индукции для nat вы не должны ожидать, что nat будет универсально определен количественно в гипотезе индукции.   -  person    schedule 29.06.2014

Ответы (2)


arrow_upward
2
arrow_downward

Я не понимаю, что здесь делает induction тактика. Всякий раз, когда я не понимаю, что делает тактика, я пытаюсь просто написать контрольный термин сам. Если вы примените принцип индукции вручную, вы можете сохранить исходную гипотезу:

Theorem ev__even : forall n, ev n -> even n.
  intros n E.
  refine (ev_ind even _ _ n E).
  - reflexivity.
  - intros n' E' IH.
    apply IH.
Qed.

Так выглядит контекст во втором случае индукции:

  n : nat
  E : ev n
  n' : nat
  E' : ev n'
  IH : even n'
  ============================
   even (S (S n'))

Предполагая

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.
person Konstantin Weitz    schedule 28.06.2014
comment
Вы можете η-уменьшить доказательство, используя refine (ev_ind even _ _) вместо intros и refine. - person ; 29.06.2014

arrow_upward
3
arrow_downward

Чтобы быть полезным, тактика индукции пытается обобщить все переменные, которые зависят от того, что вы делаете индукцией, и вещей, которые зависят от индексов ее типа. В вашем случае это подразумевает обобщение по n, недавно сгенерированному доказательству e : ev n и равенству e = E. Однако он не распространяется на сам E, потому что принципы индукции, которые автоматически генерируются для предложений, игнорируют аргумент доказательства. К сожалению, это означает, что это обобщение будет некорректно типизированным, и ваша интуиция верна: поскольку E не был обобщен с помощью n, в его типе будет указано другое число, что сделает равенство e = E нетипизированным.

person Arthur Azevedo De Amorim    schedule 29.06.2014