Coq Notes on Dependent Types
Here are some references and notes on Coq, especially on dependent types and how to reason about them.
What is eq_rect and where is it defined in Coq?
CPDT, More Dependent Types: Dependent Pattern Matching, convoy pattern, etc.
CPDT, Reasoning About Equality Proofs
Eqdep in Coq stdlib: These axioms are equivalent: Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
Eqdep_dec in Coq stdlib: UIP holds on decidable types (without any additional axioms)
inversion_sigma tactic: useful for reasoning about equality of dependent pairs