blob: 86814051758771bf67d11336dbf2722af79eb125 (
plain)
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
51
52
53
54
55
|
Inductive two : bool -> Prop :=
| Zero : two false
| One : two true.
Ltac dup :=
let H := fresh in assert (forall (P : Prop), P -> P -> P) as H by (intros; trivial);
apply H; clear H.
Lemma transform : two false <-> two true.
Proof. split; intros _; constructor. Qed.
Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
Proof.
do 2 dup.
- repeat split.
2, 4-99, 100-3:idtac.
2-5:exact One.
par:exact Zero.
- repeat split.
3-6:swap 1 4.
1-5:swap 1 5.
0-4:exact One.
all:exact Zero.
- repeat split.
1, 3:exact Zero.
1, 2, 3, 4: exact One.
- repeat split.
all:apply transform.
2, 4, 6:apply transform.
all:apply transform.
1-5:apply transform.
1-6:exact One.
Qed.
Goal True -> True.
Proof.
intros y; only 1-2 : repeat idtac.
1-1:match goal with y : _ |- _ => let x := y in idtac x end.
Fail 1-1:let x := y in idtac x.
1:let x := y in idtac x.
exact I.
Qed.
Goal True /\ (True /\ True).
Proof.
dup.
- split; only 2: (split; exact I).
exact I.
- split; only 2: split; exact I.
Qed.
Goal True -> exists (x : Prop), x.
Proof.
intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
Qed.
|
