Skip to content

Latest commit

 

History

History
26 lines (18 loc) · 1.1 KB

README.md

File metadata and controls

26 lines (18 loc) · 1.1 KB
Raw

deptacs

Dependent decide equality and other dependent tactics for Coq

A first attempt at a dependent version of the decide equality (and its sibling compare) tactic that can handle dependent types. Written entirely in Ltac. Tested in Coq version 8.5pl2.

Some features are:

  • Users can choose whether or not to use axioms (proof_irrelevance, eq_rect_eq).
  • Can interface with typeclasses.
  • Can handle cases of "green slime": non-injective function-based type index arguments.
  • Can handle both eqdec ({a=b} + {a≠b}) and eqem (a=b ∨ a≠b) goals.
  • also: sigT_generalize_eqs tactic.
  • also: dep_destruct tactic (see examples2.v)

What it won't handle:

  • Proofs that need decidable equality on universes.
  • Proofs that need decidable equality on function types.
  • Probably other things as well.

What it needs:

  • More&better tests (examples.v).
  • A built-into-Coq way to segregate type indexes from non-index parameters (to avoid the hacks in paramth.v).
  • A better way to detect which of Eqdep|Eqdep_dec|Eqdec_em are Required by the user, as well as whether proof-irrelevance is Required.