Jak duplikować hipotezę w Coq?

Question

Podczas testu napotkałem hipotezę H. Mam lematy: H -> A i H -> B.

Jak mogę zduplikować numer H, aby wyprowadzić dwie hipotezy: A i B?

edytowany: Dokładniej mam:

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

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

Ale chcę uzyskać:

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

Answer 1

Jeśli koniecznie trzeba używać założenie wiele razy, jak zasugerował, można użyć taktyki wybiegające rozumowania takich jak assert to zrobić bez usuwania go z kontekstu, np

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

Można też zrobić coś takiego assert (H' := H). jawnie skopiować H do H', chociaż zazwyczaj można uciec się do bardziej bezpośredni sposób na uzyskanie tego, co chcesz.

Answer 2

Dlaczego sądzisz, że trzeba powielać hipotezę? Jeśli używasz go w dowodzie, nie stanie się on niedostępny. Zobacz poniższy przykład:

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.