Как автоматически использовать гипотезы вида x <> y? - PullRequest
Новая
       23

Как автоматически использовать гипотезы вида x <> y?

0 голосов
/ 07 апреля 2019 
Goal forall (w x y z: string), w <> x -> (if (eqb_string w x) then y else z) = z.
Proof.
  intros.
  rewrite false_eqb_string by trivial.
  reflexivity.
Qed.

false_eqb_string - довольно тривиальный принцип доказательства.Я хотел бы использовать его неявно, через autorewrite или подобное.К сожалению, если я добавлю Hint Rewrite false_eqb_string, то любая подтерма формы eqb_string _ _ будет переписана, а допущение _ <> _ добавлено к целям, даже если это нецелесообразно.

Как я могу это сделать?заставить rewrite false_eqb_string by trivial произойти автоматически, не упоминая его по имени?

Ответы [ 2 ]

2 голосов
/ 09 апреля 2019

Я считаю, что конструкция, которую вы ищете, это 

Hint Rewrite false_eqb_string using solve [ trivial ].

Это задокументировано в справочном руководстве .В отличие от rewrite ... by ..., Hint Rewrite ... using ... не отменяет переписывание, если тактика не полностью решает побочные условия, поэтому вы должны обернуть ее в solve [ ... ], чтобы получить этот эффект.

2 голосов
/ 08 апреля 2019

Одна довольно общая конструкция - match goal with, позволяющая вам соответствовать шаблону, ну, в общем, вашей цели.Таким образом, вы можете искать несоответствия в своих гипотезах с соответствующими логическими сравнениями в цели (или другими гипотезами, если хотите) (context _ [ _ ] - это особый шаблон, который позволяет сопоставить любые подтермы с шаблоном в скобках), и переписать, используяправильная лемма.Затем вы можете дать этой match тактике имя, чтобы вам не нужно было помнить, как на самом деле называется лемма.Как и следовало ожидать, match также поддерживает множество предложений (со странным поведением обратного отслеживания, о котором следует знать), поэтому вы можете расширить эту тактику в своей собственной базе данных переписывания бедного человека. 

From Coq Require Import Arith.

Ltac rewrite_eqb :=
  match goal with
  | [ H : ?u <> ?v |- context E [ ?u =? ?v ] ] =>
    rewrite (proj2 (Nat.eqb_neq u v) H)
  end.

Goal forall (w x y z: nat), w <> x -> (if (Nat.eqb w x) then y else z) = z.
Proof.
  intros.
  rewrite_eqb.
  reflexivity.
Qed.

См. Также:

...