Coq: Ltac для транзитивности импликации (он же гипотетический силлогизм)

Этот вопрос касается проекта, которым я занимаюсь, а именно кодирования Principia Mathematica на Coq. Principia разработал правила вывода, одним из которых является Syll:

∀ P Q R: Опора, P → Q, Q → R: P → R

Я пытаюсь создать сценарий Ltac, который кодирует форму вывода Syll. Следующая тактика MP из (Chlipala 2019) работает отлично:

Ltac MP H1 H2 :=
  match goal with 
    | [ H1 : ?P -> ?Q, H2 : ?P |- _ ] => specialize (H1 H2)
end.

Здесь я понимаю, что тактика справа от = ›специализируется на применении H1 к H2. Теперь коррелированная тактика Syll не работает:

Ltac Syll H1 H2 :=
  match goal with 
     | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- _ ] =>
        specialize Syll2_06 with ?P ?Q ?R;
        intros Syll2_06;
        apply Syll2_06;
        apply H1;
        apply H2
end.

Ошибка, которую я получаю при его применении (в примере ниже):

Нет подходящих предложений для match.

Я не уверен, почему возникла такая ошибка. Была импортирована классическая логика, и я доказал теорему Syll2_06, т.е. (P → Q) → ((Q → R) → (P → R)). Фактически, то, что по сути является Syll Ltac, было применено в доказательстве теоремы Trans2_16 (см. Ниже). Поэтому я не уверен, почему превращение кода в сценарий Ltac не работает.

Возможно, я неправильно понимаю, что делает Ltac match и какова должна быть тактика справа от = ›. Но на основании просмотра руководства Coq , возможно, проблема заключается в левой стороне тактики, возможно, потому, что H1 неприменим к H2.

Дальнейшие предложения, особенно те, которые объясняют Ltac и / или мою ошибку в том, как я думаю об этом, были бы очень признательны.

Theorem Syll2_06 : ∀ P Q R : Prop,
  (P → Q) → ((Q → R) → (P → R)).
    
Ltac Syll H1 H2 :=
  match goal with 
     | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- _ ] =>
        specialize Syll2_06 with ?P ?Q ?R;
        intros Syll2_06;
        apply Syll2_06;
        apply H1;
        apply H2
end. 
    
Ltac MP H1 H2 :=
  match goal with 
    | [ H1 : ?P -> ?Q, H2 : ?P |- _ ] => specialize (H1 H2)
end.

Theorem Trans2_16 : forall P Q : Prop,
  (P → Q) → (~Q → ~P).
Proof. intros P Q.
  specialize n2_12 with Q. intros n2_12a.
  specialize Syll2_05 with P Q (~~Q). intros Syll2_05a.
  specialize n2_03 with P (~Q). intros n2_03a.
  MP n2_12a Syll2_05a.
  specialize Syll2_06 with (P→Q)  (P→~~Q) (~Q→~P). intros Syll2_06a.
  apply Syll2_06a.
  apply Syll2_05a.
  apply n2_03a.
Qed.

Theorem Trans2_17 : forall P Q : Prop,
  (~Q -> ~P) -> (P -> Q).
Proof. intros P Q.
  specialize n2_03 with (~Q) P. intros n2_03a.
  specialize n2_14 with Q. intros n2_14a.
  specialize Syll2_05 with P (~~Q) Q. intros Syll2_05a.
  MP n2_14a Syll2_05a.
  Syll 2_03a Syll2_05a.
Qed.

match implication coq ltac
person Landon D. C. Elkind    schedule 14.09.2020    source источник
comment
Замените match на lazymatch. Это фиксируется на первой (единственной) соответствующей ветке без возврата. Ошибка, вероятно, в том, что вы написали справа от => (на первый взгляд это выглядит слишком сложным), но сообщение проглатывается, потому что match пытается вернуться из этой ветки в другую и не может найти это другое - то, что сообщается. При фиксации в ветке вы получите правильное сообщение об ошибке.   -  person HTNW    schedule 14.09.2020
comment
Почему вы используете specialize? (Specialize изменяет термины в вашем контексте (H1, _4 _...)) Разве вы не хотите, чтобы тактика решала цель, т.е. apply добавляя термин? И вы также можете позволить Coq найти два предположения, которые вам нужны, вместо того, чтобы указывать их, что может быть как хорошим, так и плохим. Это избавляет вас от необходимости придумывать произвольные имена для всего, но, возможно, облегчает людям поиск доказательства, читая тактику.   -  person larsr    schedule 14.09.2020

Ответы (1)


arrow_upward
0
arrow_downward

Я не уверен, как вы хотите, чтобы эта тактика работала. Если мы начнем так:

Variables P Q R S : Prop.

Goal (P -> Q) -> (S -> Q) -> (Q -> R) -> P -> R.
  intros A B C.

тогда цель:

  A : P -> Q
  B : S -> Q
  C : Q -> R
  ============================
  P -> R

Что вы хотите сделать Syll A C?

Должно ли это решить цель? Следует ли изменить C на R? Следует ли добавить в контекст новый термин (т.е. с именем D) типа P -> R?

Например, если вам нужна тактика для достижения цели, вы можете использовать apply:

Ltac Syll H1 H2 :=
  match goal with 
  | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- ?P -> ?R ] =>
    intros p; apply (H2 (H1 p))
  end.

Если вы хотите добавить новый термин в контекст, вы можете построить его, например, с помощью assert:

Ltac Syll H1 H2 N:=
  match goal with 
  | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- ?P -> ?R ] =>
    assert (N: P -> R) by (intros p; apply (H2 (H1 p)))
  end.

Также обратите внимание, что если Syll не принимает H1 и H2 в качестве аргументов, Coq сам найдет, какие предположения использовать для построения доказательства.

person larsr    schedule 14.09.2020
comment
Большое спасибо. Последний Ltac с assert был тем, что я хотел реализовать (я хотел добавить в контекст новый термин P → R). Я ценю ваш подробный ответ, несмотря на то, что в моем вопросе не ясно, что я хотел от Ltac. - person Landon D. C. Elkind; 14.09.2020
comment
P.S. У меня было одно быстрое наблюдение. Когда я дважды применяю Ltac Syll в данном доказательстве, это дает мне ту же ошибку сопоставления. Я нашел обходной путь, но не уверен, почему он работает (или почему необходимо переименовать букву H, которую вводит Ltac Syll). Например, чтобы использовать Syll H1 H2, а затем Syll N H3, мне нужно переименовать N. Почему это так? И есть ли способ автоматизировать переименование, чтобы повторить Ltac Syll в одном доказательстве? (Я попытался очистить N и переименовать N в H, но ни один из них, похоже, не работал.) - person Landon D. C. Elkind; 14.09.2020
comment
Если я сделаю Syll A C D., а затем Syll A C E., тогда я получу D, E : P -> R в контексте. (Последний аргумент - это имя, которое должен иметь новый термин.) - person larsr; 14.09.2020
comment
если вы добавите let N := fresh N in непосредственно перед match, вы можете использовать одно и то же имя для каждого вызова, и новые переменные получат новые имена, такие как D, D0, D1, если вы вызовете Syll A C D несколько раз. - person larsr; 14.09.2020