Есть ли у Галлины дыры, как у Агды?

При доказывании в Coq приятно иметь возможность доказывать по одному кусочку за раз, а Coq помогает отслеживать обязательства.

Theorem ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B.
Proof.
  intros A B [H1 H2].
  apply H1.

На данный момент я могу видеть состояние доказательства, чтобы знать, что требуется для завершения доказательства:

context
H2: B
------
goal: B

Но когда мы пишем Gallina, должны ли мы решать все одним махом или создавать множество маленьких вспомогательных функций? Я хотел бы иметь возможность поставить вопросительный знак, чтобы спросить Coq, что он ищет:

Definition ModusPonens' := fun (A B : Prop) (H : (A -> B) /\ A) =>
  match H with
    | conj H1 H2 => H1 {?} (* hole of type B *)
  end.

Похоже, что Coq должен уметь это делать, потому что я даже могу добавить туда ltac, и Coq найдет то, что ему нужно:

Definition ModusPonens' := fun (A B : Prop) (H : (A -> B) /\ A) =>
  match H with
    | conj H1 H2 => H1 ltac:(assumption)
  end.

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

Итак, как мне это сделать? Есть ли у Coq такая функция?


coq
person Max Heiber    schedule 12.03.2020    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Вы можете использовать refine для этого. Вы можете написать знаки подчеркивания, которые превратятся в обязательства, которые вы должны решить позже.

Definition ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B.

    refine (fun A B H =>
              match H with
                 | conj H1 H2 => H1 _ (* hole of type A *)
               end).

Теперь ваша цель — предоставить A. Это может быть выполнено с помощью exact H2. Defined.

person larsr    schedule 13.03.2020
comment
Я заметил, что могу сохранить определение прозрачным/развернутым, используя определение вместо теоремы. Могу ли я внести изменения в ваш ответ? - person Max Heiber; 14.03.2020
comment
Есть ли способ завершить доказательство/определение вычислительным, а не логическим способом? Я заметил, что после . (точка) я могу добить доказательство assumption, но есть ли способ сделать это без тактики/в Галлине? - person Max Heiber; 14.03.2020
comment
Да! Вперед, пожалуйста! - person larsr; 14.03.2020
comment
Прозрачность определения больше связана с тем, завершаете ли вы режим проверки с помощью Defined. вместо Qed., чем с тем, какое ключевое слово вы используете для запуска определения. - person Daniel Schepler; 18.03.2020

arrow_upward
2
arrow_downward

Используйте подчеркивание

Definition ModusPonens' := fun (A B : Prop) (H : (A -> B) /\ A) =>
  match H with
    | conj H1 H2 => H1 _ (* hole of type A *)
  end.

(*
Error: Cannot infer this placeholder of type
"A" in environment:
A, B : Prop
H : (A -> B) /\ A
H1 : A -> B
H2 : A
*)

или используйте Program

Require Import Program.
Obligation Tactic := idtac.  (* By default Program tries to be smart and solve simple obligations automatically. This commands disables it. *)

Program Definition ModusPonens' := fun (A B : Prop) (H : (A -> B) /\ A) =>
  match H with
    | conj H1 H2 => H1 _ (* hole of type A *)
  end.

Next Obligation. intros. (* See the type of the hole *)
person Li-yao Xia    schedule 12.03.2020
comment
Спасибо! Хотел бы я отметить оба ответа правильными, так как они оба обеспечивают тот рабочий процесс, который я ищу! - person Max Heiber; 14.03.2020