adamc@78: (* Copyright (c) 2008, Adam Chlipala
adamc@78:  * 
adamc@78:  * This work is licensed under a
adamc@78:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@78:  * Unported License.
adamc@78:  * The license text is available at:
adamc@78:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@78:  *)
adamc@78: 
adamc@78: (* Types and notations presented in Chapter 6 *)
adamc@78: 
adamc@78: Set Implicit Arguments.
adamc@78: 
adamc@78: 
adamc@78: Notation "!" := (False_rec _ _) : specif_scope.
adamc@78: Notation "[ e ]" := (exist _ e _) : specif_scope.
adamc@78: Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
adamc@78: (right associativity, at level 60) : specif_scope.
adamc@78: 
adamc@221: Local Open Scope specif_scope.
adamc@78: Delimit Scope specif_scope with specif.
adamc@78: 
adamc@78: Notation "'Yes'" := (left _ _) : specif_scope.
adamc@78: Notation "'No'" := (right _ _) : specif_scope.
adamc@78: Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
adamc@78: 
adamc@86: Notation "x || y" := (if x then Yes else Reduce y) (at level 50, left associativity) : specif_scope.
adamc@86: 
adamc@86: Section sumbool_and.
adamc@86:   Variables P1 Q1 P2 Q2 : Prop.
adamc@86: 
adamc@86:   Variable x1 : {P1} + {Q1}.
adamc@86:   Variable x2 : {P2} + {Q2}.
adamc@86: 
adamc@86:   Definition sumbool_and : {P1 /\ P2} + {Q1 \/ Q2} :=
adamc@86:     match x1 with
adamc@86:       | left HP1 =>
adamc@86:         match x2 with
adamc@86:           | left HP2 => left _ (conj HP1 HP2)
adamc@86:           | right HQ2 => right _ (or_intror _ HQ2)
adamc@86:         end
adamc@86:       | right HQ1 => right _ (or_introl _ HQ1)
adamc@86:     end.
adamc@86: End sumbool_and.
adamc@86: 
adamc@86: Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope.
adamc@78: 
adamc@89: Inductive maybe (A : Set) (P : A -> Prop) : Set :=
adamc@78: | Unknown : maybe P
adamc@78: | Found : forall x : A, P x -> maybe P.
adamc@78: 
adamc@78: Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
adamc@78: Notation "??" := (Unknown _) : specif_scope.
adamc@78: Notation "[[ x ]]" := (Found _ x _) : specif_scope.
adamc@78: 
adamc@78: Notation "x <- e1 ; e2" := (match e1 with
adamc@78:                              | Unknown => ??
adamc@78:                              | Found x _ => e2
adamc@78:                            end)
adamc@78: (right associativity, at level 60) : specif_scope.
adamc@78: 
adamc@79: Notation "!!" := (inright _ _) : specif_scope.
adamc@79: Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope.
adamc@79: 
adamc@78: Notation "x <-- e1 ; e2" := (match e1 with
adamc@78:                                | inright _ => !!
adamc@78:                                | inleft (exist x _) => e2
adamc@78:                              end)
adamc@78: (right associativity, at level 60) : specif_scope.
adamc@78: 
adamc@78: Notation "e1 ;; e2" := (if e1 then e2 else ??)
adamc@78:   (right associativity, at level 60) : specif_scope.
adamc@78: 
adamc@78: Notation "e1 ;;; e2" := (if e1 then e2 else !!)
adamc@78:   (right associativity, at level 60) : specif_scope.
adamc@142: 
adamc@142: 
adamc@142: Section partial.
adamc@142:   Variable P : Prop.
adamc@142: 
adamc@142:   Inductive partial : Set :=
adamc@142:   | Proved : P -> partial
adamc@142:   | Uncertain : partial.
adamc@142: End partial.
adamc@142: 
adamc@142: Notation "[ P ]" := (partial P) : type_scope.
adamc@142: 
adamc@142: Notation "'Yes'" := (Proved _) : partial_scope.
adamc@142: Notation "'No'" := (Uncertain _) : partial_scope.
adamc@142: 
adamc@221: Local Open Scope partial_scope.
adamc@142: Delimit Scope partial_scope with partial.
adamc@142: 
adamc@142: Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.
adamc@144: Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
adamc@144: Notation "x && y" := (if x then Reduce y else No) : partial_scope.