Mercurial > cpdt > repo

comparison src/Reflection.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 17d01e51256c
children 0650420c127b
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
56 The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina. 56 The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.
57 57
58 For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *) 58 For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *)
59 59
60 (* begin hide *) 60 (* begin hide *)
61 (* begin thide *)
61 Definition paartial := partial. 62 Definition paartial := partial.
63 (* end thide *)
62 (* end hide *) 64 (* end hide *)
63 65
64 Print partial. 66 Print partial.
65 (** %\vspace{-.15in}% [[ 67 (** %\vspace{-.15in}% [[
66 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P] 68 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P]
159 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))). 161 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
160 tauto. 162 tauto.
161 Qed. 163 Qed.
162 164
163 (* begin hide *) 165 (* begin hide *)
166 (* begin thide *)
164 Definition tg := (and_ind, or_introl). 167 Definition tg := (and_ind, or_introl).
168 (* end thide *)
165 (* end hide *) 169 (* end hide *)
166 170
167 Print true_galore. 171 Print true_galore.
168 (** %\vspace{-.15in}% [[ 172 (** %\vspace{-.15in}% [[
169 true_galore = 173 true_galore =
558 Theorem mt2 : forall x y : nat, x = y --> x = y. 562 Theorem mt2 : forall x y : nat, x = y --> x = y.
559 my_tauto. 563 my_tauto.
560 Qed. 564 Qed.
561 565
562 (* begin hide *) 566 (* begin hide *)
567 (* begin thide *)
563 Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx). 568 Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx).
569 (* end thide *)
564 (* end hide *) 570 (* end hide *)
565 571
566 Print mt2. 572 Print mt2.
567 (** %\vspace{-.15in}% [[ 573 (** %\vspace{-.15in}% [[
568 mt2 = 574 mt2 =
622 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False. 628 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
623 tauto. 629 tauto.
624 Qed. 630 Qed.
625 631
626 (* begin hide *) 632 (* begin hide *)
633 (* begin thide *)
627 Definition fi := False_ind. 634 Definition fi := False_ind.
635 (* end thide *)
628 (* end hide *) 636 (* end hide *)
629 637
630 Print mt4'. 638 Print mt4'.
631 (** %\vspace{-.15in}% [[ 639 (** %\vspace{-.15in}% [[
632 mt4' = 640 mt4' =