Ослаблению гипотеза без разреза

Question

Я часто ловлю себя в следующей ситуации, где я доказал лемму, которая является следствием:

Lemma L1: A -> B 

где на самом деле эквивалентность A <-> B доказуемо, но смысл B -> A является тривиальный и не очень интересный результат. Затем в процессе проектирования некоторые доказательства, я в конечном итоге с гипотезой:

H : A 

, и я на самом деле хочу использовать B. Я могу использовать сокращение:

cut (B). 

и перейти оттуда, но я уверен, что есть более быстрый способ формально ослабить гипотезу H, заменив заявление A на B.

То, что я делал в последнее время, это вернуться к моей лемме и доказать обе стороны импликации.

Lemma L1 : A <-> B 

затем используйте простой rewrite L1 in H. Так что это работает для эквивалентности, но не в общем, конечно. Итак, как я могу ослабить гипотезу без cut от простой импликации?

Answer 1

Один простой способ сделать это - использовать apply L1 in H..

Variables A B : Prop. 
Lemma L1 : A -> B. Admitted. 

Theorem theorem : A -> 1 = 1. 
    intros H. 
    apply L1 in H. 

Последняя строка превращается H : A в H : B.

Answer 2

Действительно, это распространенное явление, и некоторые плагины Coq, такие как ssreflect, обеспечивают специальную поддержку для него, называемую «представлением гипотезы». ИМХО переписывание может быть не так плохо в вашем случае.

Coq 8,5 вводит экспериментальную p%term функции для выполнения «представления» на гипотезах, так что вы можете сделать:

Variables (A B C : Prop). 
Hypothesis U : A -> B. 

Lemma L1 : A -> B. 
intros h%U. 

, но обратите внимание, что эта функция может быть удалено. Конечно, если вы открыты для использования мнения языка ssreflect тактика является существенным признаком, и вы можете просто сделать:

Variables (A B C : Prop). 
Hypothesis U : A -> B. 

Lemma L1 : A -> B. 
by move=> /U. 

Просмотров в ssreflect prodive многих других вкусности, например, если у вас есть гипотеза B и lemma U : A -> B -> C, вы можете обычно применять /U и т. д. см. руководство для получения более подробной информации.