adamc@78
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@78
|
2 *
|
adamc@78
|
3 * This work is licensed under a
|
adamc@78
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@78
|
5 * Unported License.
|
adamc@78
|
6 * The license text is available at:
|
adamc@78
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@78
|
8 *)
|
adamc@78
|
9
|
adamc@78
|
10 (* Types and notations presented in Chapter 6 *)
|
adamc@78
|
11
|
adamc@78
|
12 Set Implicit Arguments.
|
adamc@78
|
13
|
adamc@78
|
14
|
adamc@78
|
15 Notation "!" := (False_rec _ _) : specif_scope.
|
adamc@78
|
16 Notation "[ e ]" := (exist _ e _) : specif_scope.
|
adamc@78
|
17 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
|
adamc@78
|
18 (right associativity, at level 60) : specif_scope.
|
adamc@78
|
19
|
adamc@221
|
20 Local Open Scope specif_scope.
|
adamc@78
|
21 Delimit Scope specif_scope with specif.
|
adamc@78
|
22
|
adamc@78
|
23 Notation "'Yes'" := (left _ _) : specif_scope.
|
adamc@78
|
24 Notation "'No'" := (right _ _) : specif_scope.
|
adamc@78
|
25 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
|
adamc@78
|
26
|
adamc@86
|
27 Notation "x || y" := (if x then Yes else Reduce y) (at level 50, left associativity) : specif_scope.
|
adamc@86
|
28
|
adamc@86
|
29 Section sumbool_and.
|
adamc@86
|
30 Variables P1 Q1 P2 Q2 : Prop.
|
adamc@86
|
31
|
adamc@86
|
32 Variable x1 : {P1} + {Q1}.
|
adamc@86
|
33 Variable x2 : {P2} + {Q2}.
|
adamc@86
|
34
|
adamc@86
|
35 Definition sumbool_and : {P1 /\ P2} + {Q1 \/ Q2} :=
|
adamc@86
|
36 match x1 with
|
adamc@86
|
37 | left HP1 =>
|
adamc@86
|
38 match x2 with
|
adamc@86
|
39 | left HP2 => left _ (conj HP1 HP2)
|
adamc@86
|
40 | right HQ2 => right _ (or_intror _ HQ2)
|
adamc@86
|
41 end
|
adamc@86
|
42 | right HQ1 => right _ (or_introl _ HQ1)
|
adamc@86
|
43 end.
|
adamc@86
|
44 End sumbool_and.
|
adamc@86
|
45
|
adamc@86
|
46 Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope.
|
adamc@78
|
47
|
adamc@89
|
48 Inductive maybe (A : Set) (P : A -> Prop) : Set :=
|
adamc@78
|
49 | Unknown : maybe P
|
adamc@78
|
50 | Found : forall x : A, P x -> maybe P.
|
adamc@78
|
51
|
adamc@78
|
52 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
|
adamc@78
|
53 Notation "??" := (Unknown _) : specif_scope.
|
adamc@78
|
54 Notation "[[ x ]]" := (Found _ x _) : specif_scope.
|
adamc@78
|
55
|
adamc@78
|
56 Notation "x <- e1 ; e2" := (match e1 with
|
adamc@78
|
57 | Unknown => ??
|
adamc@78
|
58 | Found x _ => e2
|
adamc@78
|
59 end)
|
adamc@78
|
60 (right associativity, at level 60) : specif_scope.
|
adamc@78
|
61
|
adamc@79
|
62 Notation "!!" := (inright _ _) : specif_scope.
|
adamc@79
|
63 Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope.
|
adamc@79
|
64
|
adamc@78
|
65 Notation "x <-- e1 ; e2" := (match e1 with
|
adamc@78
|
66 | inright _ => !!
|
adamc@78
|
67 | inleft (exist x _) => e2
|
adamc@78
|
68 end)
|
adamc@78
|
69 (right associativity, at level 60) : specif_scope.
|
adamc@78
|
70
|
adamc@78
|
71 Notation "e1 ;; e2" := (if e1 then e2 else ??)
|
adamc@78
|
72 (right associativity, at level 60) : specif_scope.
|
adamc@78
|
73
|
adamc@78
|
74 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
|
adamc@78
|
75 (right associativity, at level 60) : specif_scope.
|
adamc@142
|
76
|
adamc@142
|
77
|
adamc@142
|
78 Section partial.
|
adamc@142
|
79 Variable P : Prop.
|
adamc@142
|
80
|
adamc@142
|
81 Inductive partial : Set :=
|
adamc@142
|
82 | Proved : P -> partial
|
adamc@142
|
83 | Uncertain : partial.
|
adamc@142
|
84 End partial.
|
adamc@142
|
85
|
adamc@142
|
86 Notation "[ P ]" := (partial P) : type_scope.
|
adamc@142
|
87
|
adamc@142
|
88 Notation "'Yes'" := (Proved _) : partial_scope.
|
adamc@142
|
89 Notation "'No'" := (Uncertain _) : partial_scope.
|
adamc@142
|
90
|
adamc@221
|
91 Local Open Scope partial_scope.
|
adamc@142
|
92 Delimit Scope partial_scope with partial.
|
adamc@142
|
93
|
adamc@142
|
94 Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.
|
adamc@144
|
95 Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
|
adamc@144
|
96 Notation "x && y" := (if x then Reduce y else No) : partial_scope.
|