Mercurial > cpdt > repo
comparison src/Subset.v @ 271:aa3c054afce0
Some bug fixes while working on JFR version
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 19 Apr 2010 16:49:26 -0400 |
| parents | c4b1c0de7af9 |
| children | caa69851c78d |
comparison
equal
deleted
inserted
replaced
| 270:fd46d077b952 | 271:aa3c054afce0 |
|---|---|
| 69 | S n' => fun _ => n' | 69 | S n' => fun _ => n' |
| 70 end. | 70 end. |
| 71 | 71 |
| 72 (** We expand the type of [pred] to include a %\textit{%#<i>#proof#</i>#%}% that its argument [n] is greater than 0. When [n] is 0, we use the proof to derive a contradiction, which we can use to build a value of any type via a vacuous pattern match. When [n] is a successor, we have no need for the proof and just return the answer. The proof argument can be said to have a %\textit{%#<i>#dependent#</i>#%}% type, because its type depends on the %\textit{%#<i>#value#</i>#%}% of the argument [n]. | 72 (** We expand the type of [pred] to include a %\textit{%#<i>#proof#</i>#%}% that its argument [n] is greater than 0. When [n] is 0, we use the proof to derive a contradiction, which we can use to build a value of any type via a vacuous pattern match. When [n] is a successor, we have no need for the proof and just return the answer. The proof argument can be said to have a %\textit{%#<i>#dependent#</i>#%}% type, because its type depends on the %\textit{%#<i>#value#</i>#%}% of the argument [n]. |
| 73 | 73 |
| 74 One aspects in particular of the definition of [pred_strong1] that may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural. | 74 One aspect in particular of the definition of [pred_strong1] may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural. |
| 75 | 75 |
| 76 [[ | 76 [[ |
| 77 Definition pred_strong1' (n : nat) (pf : n > 0) : nat := | 77 Definition pred_strong1' (n : nat) (pf : n > 0) : nat := |
| 78 match n with | 78 match n with |
| 79 | O => match zgtz pf with end | 79 | O => match zgtz pf with end |