Newer
Older
Armaël Guéneau
committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
From stdpp Require Import tactics.
Goal forall P1 P2 P3 P4 (P: Prop),
P1 ∨ (Is_true (P2 || P3)) ∨ P4 →
(P1 → P) →
(P2 → P) →
(P3 → P) →
(P4 → P) →
P.
Proof.
intros * HH X1 X2 X3 X4.
destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
Qed.
Goal forall P1 P2 P3 P4 (P: Prop),
P1 ∨ P2 →
P3 ∨ P4 →
(P1 → P3 → P) →
(P1 → P4 → P) →
(P2 → P3 → P) →
(P2 → P4 → P) →
P.
Proof.
intros * HH1 HH2 X1 X2 X3 X4.
destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4 (P: Prop),
id (P1 ∨ P2) →
id (P3 ∨ P4) →
(P1 → P3 → P) →
(P1 → P4 → P) →
(P2 → P3 → P) →
(P2 → P4 → P) →
P.
Proof.
intros * HH1 HH2 X1 X2 X3 X4.
Fail progress destruct_or?.
Fail progress destruct_or!.
destruct_or! HH1; destruct_or! HH2;
[ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4,
P1 ∧ (Is_true (P2 && P3)) ∧ P4 →
P1 ∧ P2 ∧ P3.
Proof.
intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
destruct_and?. Fail destruct_and!. assumption.
Qed.