Gallery of programs
Dependent PatternMatching

Polynomials: a reflexive tactic for solving boolean tautologies (source).

HoTT_light: basics of the HoTT library implemented using a logic in
Type
(source). 
MoreDep: part of chapter 8 of Adam Chlipala’s CPDT (source).

Definitional interpreter: definitional interpreter for an impure language using wellscoped, welltyped syntax (source).

Views: using dependent patternmatching with views, to handle default cases in patternmatching (source).
Recursion

STLC: strong normalization of simplytyped lambdacalculus with products using hereditary substitutions (source).

String Matching: beginning of example by Nicky Vazou on string matching, uses wellfounded recursion (source).

Rose Trees: nested wellfounded recursion (source).

Nested mutual recursion: structural mutual and nested recursion (source).

Accumulators: defining and proving programs using accumulators, with wellfounded recursion (source).

Mutual wellfounded recursion: representing mutually recursive wellfounded definitions using dependent patternmatching (source).

General recursion: working with general recursive functions, without worrying about termination proofs (source).