blob: 09ec9de170fc4f34da2087faefd681a1b4b2364e (
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
Fixpoint fib n := match n with
| O => 1
| S m => match m with
| O => 1
| S o => fib o + fib m end end.
Ltac sleep n :=
try (cut (fib n = S (fib n)); reflexivity).
Let time := 15.
(* BEGIN MINI DEMO *)
(* JUMP TO "JUMP HERE" *)
Lemma a : True.
Proof.
sleep time.
idtac.
sleep time.
exact (I I).
Qed.
Lemma b : True.
Proof.
sleep time.
idtac.
(* change in semantics: Print a. *)
sleep time.
exact a.
Qed. (* JUMP HERE *)
Lemma work_here : True.
Proof.
cut True.
Abort.
(* END MINI DEMO *)
Require Import Unicode.Utf8.
Notation "a ⊃ b" := (a → b) (at level 91, left associativity).
Definition untrue := False.
Section Ex.
Variable P Q : Prop.
Implicit Types X Y : Prop.
Hypothesis CL : forall X Y, (X → ¬Y → untrue) → (¬X ∨ Y).
Lemma Peirce : P ⊃ Q ⊃ P ⊃ P.
Proof (* using P Q CL. *). (* Uncomment -> more readable *)
intro pqp.
Remark EM : ¬P ∨ P.
Proof using P CL.
intros; apply CL; intros p np.
Fail progress auto. (* Missing hint *)
(* Try commenting this out *)
Hint Extern 0 => match goal with
p : P, np : ¬P |- _ => case (np p)
end.
auto. (* This line requires the hint above *)
Qed.
case EM; auto. (* This line requires the hint above *)
Qed.
End Ex.
Check EM. (* Print EM. *)
Axiom exM : forall P, P \/ ~P.
Lemma CPeirce (P Q : Prop) : P ⊃ Q ⊃ P ⊃ P.
Proof.
apply Peirce.
intros.
case (exM X); auto.
intro; right.
case (exM Y); auto; intro.
case H; auto.
Qed.
Require Import Recdef.
Definition m (n : nat) := n.
Function f (n : nat) {measure m n} : bool :=
match n with
| O => true
| S x => f (x + 0)
end.
Proof.
intros x y _. unfold m.
rewrite <- plus_n_O. auto.
Qed.
|
