Drop przesłankę w celu zastosowania w stylu

Question

załóżmy chcę pokazać następujący lemat

lemma "⟦ A; B; C ⟧ ⟹ D" 

mam cel

1. A ⟹ B ⟹ C ⟹ D 

Jednak nie muszę B. Jak mogę przenieść mój cel na coś jak

1. A ⟹ C ⟹ D 

Nie chcę zmieniać oryginalnego lemma oświadczenie, tylko aktualny cel w zastosować styl.

Answer 1

Co chcesz to apply (thin_tac B). Jednak ostatnim razem, kiedy to zrobiłem, Peter Lammich krzyczał "O Boże, dlaczego to robisz!" w obrzydzeniu i przepisałem mój dowód, żeby pozbyć się thin_tac. Tak więc użycie tej taktyki nie wydaje się być już zachęcane.

Answer 2

Zwykle lepiej unikać niepożądanych rzeczy w stanie docelowym, zamiast usuwać je później. Sposób, w jaki formułujesz problem dowodowy, wpływa na sposób jego rozwiązania.

Jest to szczególnie ważne w przypadku dowodów strukturyzowanych: odwołać pozytywnie do tych faktów, które powinny uczestniczyć w następnym kroku dowodu, zamiast tłumienia niektóre z nich negatywnie.

E.g. tak:

from `A` and `C` have D ... 

Opowiadanie, które fakty są istotne dla dowodu, jest już początkiem czytelności.

następstwie tego stylu, początkowy problem będzie wyglądać następująco:

lemma 
    assumes A and B and C 
    shows D 
proof - 
    from `A` and `C` show D sorry 
qed 

lub jak to z ograniczonej gadatliwości, jeśli ABCD są duże propozycje:

lemma 
    assumes a: A and b: B and c: C 
    shows D 
proof - 
    from a c show ?thesis sorry 
qed