У Галлины дыры как в Агде? - PullRequest
Новая
       5

У Галлины дыры как в Агде?

4 голосов
/ 13 марта 2020

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

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

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

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

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

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

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

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

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

Так как мне это сделать? У Coq есть такая особенность?

Ответы [ 2 ]

2 голосов
/ 13 марта 2020

Вы можете использовать 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.

2 голосов
/ 13 марта 2020

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

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 *)
...