MoreSpecif.v 2.93 KB
Newer Older
1
(* Copyright (c) 2008, 2011, 2015, Adam Chlipala
Adam Chlipala's avatar
Adam Chlipala committed
2 3 4 5 6 7 8 9
 * 
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)

10
(* Types and notations presented in Chapter 6 *)
Adam Chlipala's avatar
Adam Chlipala committed
11 12

Set Implicit Arguments.
13
Set Asymmetric Patterns.
Adam Chlipala's avatar
Adam Chlipala committed
14 15 16 17 18 19 20


Notation "!" := (False_rec _ _) : specif_scope.
Notation "[ e ]" := (exist _ e _) : specif_scope.
Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
(right associativity, at level 60) : specif_scope.

Adam Chlipala's avatar
Adam Chlipala committed
21
Local Open Scope specif_scope.
Adam Chlipala's avatar
Adam Chlipala committed
22 23 24 25 26 27
Delimit Scope specif_scope with specif.

Notation "'Yes'" := (left _ _) : specif_scope.
Notation "'No'" := (right _ _) : specif_scope.
Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.

28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
Notation "x || y" := (if x then Yes else Reduce y) (at level 50, left associativity) : specif_scope.

Section sumbool_and.
  Variables P1 Q1 P2 Q2 : Prop.

  Variable x1 : {P1} + {Q1}.
  Variable x2 : {P2} + {Q2}.

  Definition sumbool_and : {P1 /\ P2} + {Q1 \/ Q2} :=
    match x1 with
      | left HP1 =>
        match x2 with
          | left HP2 => left _ (conj HP1 HP2)
          | right HQ2 => right _ (or_intror _ HQ2)
        end
      | right HQ1 => right _ (or_introl _ HQ1)
    end.
End sumbool_and.

Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope.
Adam Chlipala's avatar
Adam Chlipala committed
48

49
Inductive maybe (A : Set) (P : A -> Prop) : Set :=
Adam Chlipala's avatar
Adam Chlipala committed
50 51 52 53 54
| Unknown : maybe P
| Found : forall x : A, P x -> maybe P.

Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
Notation "??" := (Unknown _) : specif_scope.
Adam Chlipala's avatar
Adam Chlipala committed
55
Notation "[| x |]" := (Found _ x _) : specif_scope.
Adam Chlipala's avatar
Adam Chlipala committed
56 57 58 59 60 61 62

Notation "x <- e1 ; e2" := (match e1 with
                             | Unknown => ??
                             | Found x _ => e2
                           end)
(right associativity, at level 60) : specif_scope.

Adam Chlipala's avatar
Adam Chlipala committed
63
Notation "!!" := (inright _ _) : specif_scope.
Adam Chlipala's avatar
Adam Chlipala committed
64
Notation "[|| x ||]" := (inleft _ [x]) : specif_scope.
Adam Chlipala's avatar
Adam Chlipala committed
65

Adam Chlipala's avatar
Adam Chlipala committed
66 67 68 69 70 71 72 73 74 75 76
Notation "x <-- e1 ; e2" := (match e1 with
                               | inright _ => !!
                               | inleft (exist x _) => e2
                             end)
(right associativity, at level 60) : specif_scope.

Notation "e1 ;; e2" := (if e1 then e2 else ??)
  (right associativity, at level 60) : specif_scope.

Notation "e1 ;;; e2" := (if e1 then e2 else !!)
  (right associativity, at level 60) : specif_scope.
Adam Chlipala's avatar
Adam Chlipala committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91


Section partial.
  Variable P : Prop.

  Inductive partial : Set :=
  | Proved : P -> partial
  | Uncertain : partial.
End partial.

Notation "[ P ]" := (partial P) : type_scope.

Notation "'Yes'" := (Proved _) : partial_scope.
Notation "'No'" := (Uncertain _) : partial_scope.

Adam Chlipala's avatar
Adam Chlipala committed
92
Local Open Scope partial_scope.
Adam Chlipala's avatar
Adam Chlipala committed
93 94 95
Delimit Scope partial_scope with partial.

Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.
Adam Chlipala's avatar
Adam Chlipala committed
96 97
Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
Notation "x && y" := (if x then Reduce y else No) : partial_scope.