Mercurial > cpdt > repo

comparison src/MoreDep.v @ 426:5f25705a10ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 18:10:26 -0400
parents 6ed5ee4845e4
children 8077352044b2
comparison
equal deleted inserted replaced
425:6ed5ee4845e4 426:5f25705a10ea
1209 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s) 1209 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
1210 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s 1210 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
1211 | Star _ r => dec_star _ _ _ 1211 | Star _ r => dec_star _ _ _
1212 end); crush; 1212 end); crush;
1213 match goal with 1213 match goal with
1214 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _)) 1214 | [ H : _ |- _ ] => generalize (H _ _ (eq_refl _))
1215 end; tauto. 1215 end; tauto.
1216 Defined. 1216 Defined.
1217 1217
1218 (** It is interesting to pause briefly to consider alternate implementations of [matches]. Dependent types give us much latitude in how specific correctness properties may be encoded with types. For instance, we could have made [regexp] a non-indexed inductive type, along the lines of what is possible in traditional ML and Haskell. We could then have implemented a recursive function to map [regexp]s to their intended meanings, much as we have done with types and programs in other examples. That style is compatible with the [refine]-based approach that we have used here, and it might be an interesting exercise to redo the code from this subsection in that alternate style or some further encoding of the reader's choice. The main advantage of indexed inductive types is that they generally lead to the smallest amount of code. *) 1218 (** It is interesting to pause briefly to consider alternate implementations of [matches]. Dependent types give us much latitude in how specific correctness properties may be encoded with types. For instance, we could have made [regexp] a non-indexed inductive type, along the lines of what is possible in traditional ML and Haskell. We could then have implemented a recursive function to map [regexp]s to their intended meanings, much as we have done with types and programs in other examples. That style is compatible with the [refine]-based approach that we have used here, and it might be an interesting exercise to redo the code from this subsection in that alternate style or some further encoding of the reader's choice. The main advantage of indexed inductive types is that they generally lead to the smallest amount of code. *)
1219 1219