Mercurial > cpdt > repo

annotate src/MoreSpecif.v @ 150:eee4fd311f64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reflection exercise
author Adam Chlipala <adamc@hcoop.net>
date Wed, 29 Oct 2008 17:41:38 -0400
parents 5ea9a0bff8f7
children 54e8ecb5ec88
rev   line source
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@78 20 Open Local 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@142 91 Open Local 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.