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
56
57
58
59
60
61
62
63
64
65
66
|
Goal False /\ True.
Proof.
split.
idtac.
idtac.
exact I.
idtac.
idtac.
exact I.
Qed.
Lemma baz : (exists n, n = 3 /\ n = 3) /\ True.
Proof.
split. { eexists. split. par: trivial. }
trivial.
Qed.
Lemma baz1 : (True /\ False) /\ True.
Proof.
split. { split. par: trivial. }
trivial.
Qed.
Lemma foo : (exists n, n = 3 /\ n = 3) /\ True.
Proof.
split.
{ idtac.
unshelve eexists.
{ apply 3. }
{ split.
{ idtac. trivialx. }
{ reflexivity. } } }
trivial.
Qed.
Lemma foo1 : False /\ True.
Proof.
split.
{ exact I. }
{ exact I. }
Qed.
Definition banana := true + 4.
Check banana.
Lemma bar : (exists n, n = 3 /\ n = 3) /\ True.
Proof.
split.
- idtac.
unshelve eexists.
+ apply 3.
+ split.
* idtacx. trivial.
* reflexivity.
- trivial.
Qed.
Lemma baz2 : ((1=0 /\ False) /\ True) /\ False.
Proof.
split. split. split.
- solve [ auto ].
- solve [ trivial ].
- solve [ trivial ].
- exact 6.
Qed.
|
