Как ввести новую переменную в Coq?

Мне было интересно, есть ли способ ввести совершенно новую переменную во время доказательства теоремы в Coq?

В качестве полного примера рассмотрим следующее свойство отсюда о равномерности длины списка.

Inductive ev_list {X:Type}: list X -> Prop :=
  | el_nil : ev_list []
  | el_cc  : forall x y l, ev_list l -> ev_list (x :: y :: l).

Теперь я хочу доказать, что для любого списка l, если его length четный, то ev_list l выполняется:

Lemma ev_length__ev_list': forall X (l : list X), ev (length l) -> ev_list l.
Proof.
  intros X l H.

который дает:

1 subgoals
X : Type
l : list X
H : ev (length l)
______________________________________(1/1)
ev_list l

Теперь я хотел бы определить новую свободную переменную n и гипотезу n = length l. В рукописной математике, я думаю, мы можем это сделать, а затем провести индукцию около n. Но есть ли способ сделать то же самое в Coq?

Примечание. Я спрашиваю по следующим причинам:

  1. Я не хочу вводить это n искусственно в формулировку самой теоремы, как это сделано на странице, указанной ранее, что ИМХО неестественно.

  2. Я пробовал induction H., но, похоже, не работает. Coq не смог провести анализ случая length l ev, и гипотеза индукции (IH) не была сформирована.

Спасибо.


coq coq-tactic
person tinlyx    schedule 08.10.2015    source источник

Ответы (3)


arrow_upward
12
arrow_downward

Это обычная проблема в доказательствах Coq. Вы можете использовать тактику remember:

remember (length l) as n.

Если вы также проводите индукцию по H, вам, возможно, также придется заранее обобщить l, выполнив

generalize dependent l.
induction H.
person Arthur Azevedo De Amorim    schedule 08.10.2015

arrow_upward
2
arrow_downward

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

induction (length l) eqn:H0
person eponier    schedule 08.10.2015

arrow_upward
2
arrow_downward

Согласно изоморфизму Карри-Ховарда, гипотезы в вашем контексте - это просто переменные. Вы можете определять новые переменные с помощью функции. Следующая тактика refine расширяет цель с помощью новой переменной n (которая установлена ​​в length l) и доказательства e того, что n = length l (которая установлена ​​в eq_refl).

Lemma ev_length__ev_list': forall X (l : list X), ev (length l) -> ev_list l.
Proof.
  intros X l H.
  refine ((fun n (e:n = length l) => _) (length l) eq_refl).
  (* proof *)
Admitted.
person Konstantin Weitz    schedule 08.10.2015