Mercurial > cpdt > repo

annotate src/MoreSpecif.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents ed829eaa91b2
children
rev   line source
adam@534 1 (* Copyright (c) 2008, 2011, 2015, 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
adam@353 10 (* Types and notations presented in Chapter 6 *)
adamc@78 11
adamc@78 12 Set Implicit Arguments.
adam@534 13 Set Asymmetric Patterns.
adamc@78 14
adamc@78 15
adamc@78 16 Notation "!" := (False_rec _ _) : specif_scope.
adamc@78 17 Notation "[ e ]" := (exist _ e _) : specif_scope.
adamc@78 18 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
adamc@78 19 (right associativity, at level 60) : specif_scope.
adamc@78 20
adamc@221 21 Local Open Scope specif_scope.
adamc@78 22 Delimit Scope specif_scope with specif.
adamc@78 23
adamc@78 24 Notation "'Yes'" := (left _ _) : specif_scope.
adamc@78 25 Notation "'No'" := (right _ _) : specif_scope.
adamc@78 26 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
adamc@78 27
adamc@86 28 Notation "x || y" := (if x then Yes else Reduce y) (at level 50, left associativity) : specif_scope.
adamc@86 29
adamc@86 30 Section sumbool_and.
adamc@86 31 Variables P1 Q1 P2 Q2 : Prop.
adamc@86 32
adamc@86 33 Variable x1 : {P1} + {Q1}.
adamc@86 34 Variable x2 : {P2} + {Q2}.
adamc@86 35
adamc@86 36 Definition sumbool_and : {P1 /\ P2} + {Q1 \/ Q2} :=
adamc@86 37 match x1 with
adamc@86 38 | left HP1 =>
adamc@86 39 match x2 with
adamc@86 40 | left HP2 => left _ (conj HP1 HP2)
adamc@86 41 | right HQ2 => right _ (or_intror _ HQ2)
adamc@86 42 end
adamc@86 43 | right HQ1 => right _ (or_introl _ HQ1)
adamc@86 44 end.
adamc@86 45 End sumbool_and.
adamc@86 46
adamc@86 47 Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope.
adamc@78 48
adamc@89 49 Inductive maybe (A : Set) (P : A -> Prop) : Set :=
adamc@78 50 | Unknown : maybe P
adamc@78 51 | Found : forall x : A, P x -> maybe P.
adamc@78 52
adamc@78 53 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
adamc@78 54 Notation "??" := (Unknown _) : specif_scope.
adam@335 55 Notation "[| x |]" := (Found _ x _) : specif_scope.
adamc@78 56
adamc@78 57 Notation "x <- e1 ; e2" := (match e1 with
adamc@78 58 | Unknown => ??
adamc@78 59 | Found x _ => e2
adamc@78 60 end)
adamc@78 61 (right associativity, at level 60) : specif_scope.
adamc@78 62
adamc@79 63 Notation "!!" := (inright _ _) : specif_scope.
adam@335 64 Notation "[|| x ||]" := (inleft _ [x]) : specif_scope.
adamc@79 65
adamc@78 66 Notation "x <-- e1 ; e2" := (match e1 with
adamc@78 67 | inright _ => !!
adamc@78 68 | inleft (exist x _) => e2
adamc@78 69 end)
adamc@78 70 (right associativity, at level 60) : specif_scope.
adamc@78 71
adamc@78 72 Notation "e1 ;; e2" := (if e1 then e2 else ??)
adamc@78 73 (right associativity, at level 60) : specif_scope.
adamc@78 74
adamc@78 75 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
adamc@78 76 (right associativity, at level 60) : specif_scope.
adamc@142 77
adamc@142 78
adamc@142 79 Section partial.
adamc@142 80 Variable P : Prop.
adamc@142 81
adamc@142 82 Inductive partial : Set :=
adamc@142 83 | Proved : P -> partial
adamc@142 84 | Uncertain : partial.
adamc@142 85 End partial.
adamc@142 86
adamc@142 87 Notation "[ P ]" := (partial P) : type_scope.
adamc@142 88
adamc@142 89 Notation "'Yes'" := (Proved _) : partial_scope.
adamc@142 90 Notation "'No'" := (Uncertain _) : partial_scope.
adamc@142 91
adamc@221 92 Local Open Scope partial_scope.
adamc@142 93 Delimit Scope partial_scope with partial.
adamc@142 94
adamc@142 95 Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.
adamc@144 96 Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
adamc@144 97 Notation "x && y" := (if x then Reduce y else No) : partial_scope.