Wie man eine Hypothese in Coq dupliziert?

Question

Während eines Beweises stieß ich auf eine Hypothese H. Ich habe Lemmata: H -> A und H -> B. Wie kann ich H duplizieren, um zwei Hypothesen A und B abzuleiten?

bearbeitet: Genauer gesagt, ich habe:

lemma l1: X -> A. 
lemma l2: X -> B. 

1 subgoals, subgoal 1 (ID: 42) 
H: X 
========= 
Y 

Aber, ich will bekommen:

1 subgoals, subgoal 1 (ID: 42) 
H1: A 
H2: B 
========= 
Y 

Answer 1

Wenn Sie unbedingt eine Annahme verwenden müssen, um mehrere Male, wie Sie vorgeschlagen, Sie voraus Argumentation Taktik wie assert verwenden können, um dies zu tun, ohne es aus dem Kontext zu löschen, z.B.

assert (HA := l1 H). 
assert (HB := l2 H). 

Sie können auch etwas tun, wie assert (H' := H). explizit H in H' kopieren, obwohl Sie in der Regel auf einen direkteren Weg zurückgreifen kann für das bekommen, was Sie wollen.

Answer 2

Warum denken Sie, dass Sie die Hypothese duplizieren müssen? Wenn Sie es in einem Proof verwenden, wird es nicht verfügbar. Sehen Sie folgendes Beispiel:

Parameter A B H : Type. 
Parameter lemma1 : H -> A. 
Parameter lemma2 : H -> B. 

Goal H -> A * B. 
intro; split; [apply lemma1 | apply lemma2]; assumption. 
Qed.