Coq просто / разворачивается только один раз. (Замените часть цели результатом одной итерации функции.)

Я преподаю в университете на курсе Системы типов языков, и профессор использовал следующий пример для индуктивных доказательств в теории типов на доске на прошлой лекции:

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

У меня есть следующий код Coq, подготовленный для реализации этого в классе:

Inductive term : Set :=
  | zero
  | suc (t : term)
.

Fixpoint greaterThan (t t' : term) {struct t} : bool :=
  match t, t' with
   | zero, _ => false
   | suc t, zero => true
   | suc t, suc t' => t > t'
  end
where "t > t'" := (greaterThan t t').

Lemma successorIsGreater : forall t : term, suc t > t = true.
Proof.
  induction t.

  (* zero *)
  - simpl.
    reflexivity.

  (* suc t *)
  -

что приводит меня к следующей цели:

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true

Я могу решить эту проблему несколькими способами, переписав, развернув и / или упростив до того, как она просто превратится в рефлексивность, но что мне действительно хотелось бы сделать, чтобы она была чище, так это применить одну итерацию больше, чем, которая просто превратит (suc (suc t) > suc t) = true в (suc t > t) = true , и я мог бы закончить доказательство с помощью exact IHt.

Есть ли способ добиться этого?

ps: Я знаю, что могу simpl in IHt, а затем использовать exact, но оно расширяется до выражения соответствия, которое намного более подробное, чем то, что здесь необходимо.

Изменить: Благодаря ответу Théo Winterhalter я понял, что могу также использовать exact сам по себе, поскольку термины можно конвертировать, но это не слишком хорошо покажет процесс студентам. (Примечание: оба случая индукции также решаются с помощью trivial, но я не думаю, что они тоже многому научились бы.: D)


induction coq proof coq-tactic
person Isti115    schedule 16.09.2019    source источник

Ответы (2)


arrow_upward
6
arrow_downward

Другая возможность - использовать Arguments местный язык, чтобы указать simpl не сводить greaterThan к выражению соответствия. Поместите Arguments greaterThan: simpl nomatch. где-нибудь после определения greaterThan. Затем, когда вы используете simpl в среде

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true

ты получаешь

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc t > t) = true

как ты хотел.

person SCappella    schedule 16.09.2019

arrow_upward
2
arrow_downward

Я не уверен, что есть способ сделать это сразу. Один из обычных способов - доказать лемму, соответствующую правилу вычислений по рефлексивности:

Lemma greaterThan_suc_suc :
  forall n m,
    suc n > suc m = n > m.
Proof.
  intros. reflexivity.
Defined.

(Я использую defined, чтобы он действительно разворачивался до eq_refl и ушел, если нужно.)

Также есть возможность сделать change замену вручную.

change (suc (suc t) > suc t) with (suc t > t).

Он проверит конвертируемость и заменит одно выражение другим в цели.

Вы можете немного автоматизировать этот процесс, написав тактику, которая упрощает его.

Ltac red_greaterThan :=
  match goal with
  | |- context [ suc ?n > suc ?m ] =>
    change (suc n > suc m) with (n > m)
  | |- context [ suc ?n > zero ] =>
    change (suc n > zero) with true
  | |- context [ zero > ?n ] =>
    change (zero > n) with false
  end.

Lemma successorIsGreater : forall t : term, suc t > t = true.
Proof.
  induction t.

  (* zero *)
  - red_greaterThan. reflexivity.

  (* suc t *)
  - red_greaterThan. assumption.
Qed.
person Théo Winterhalter    schedule 16.09.2019
comment
Хотя это не совсем то, что я искал (поскольку они конвертируемые, я мог бы использовать exact сам по себе, что не показывает процедуру для студентов), изменение все же кажется моим лучшим выбором, так что большое спасибо за упоминание такой возможности! Я отмечу ваш ответ как принятый, если не придет никто лучше. - person Isti115; 16.09.2019
comment
Я надеюсь, что кто-то знает. Я тоже был бы рад. Я дополню свой ответ чем-нибудь еще. - person Théo Winterhalter; 16.09.2019
comment
Спасибо за обновленный контент, очень ценю! Наконец, я пометил ответ SCappella как принятый, так как он кажется более подходящим для того, что я искал (требует меньше пояснений), но есть и другие замечательные вещи, о которых следует помнить как о возможностях! - person Isti115; 17.09.2019