Library Equations.DepElimDec

From Equations Require Import Init Signature DepElim EqDec HSetInstances.

Alternative implementation of generalization using sigma types only, allowing to use K on decidable domains.

Ltac simplify_one_dep_elim' :=
match goal with

| |- let _ := block in _ => fail 1
| |- _ => simplify ?

| |- ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
| |- Id (?f ?x) (?g ?y) -> _ => let H := fresh in progress (intros H ; inversion H ; clear H)
| |- ?t = ?u -> _ => let hyp := fresh in
  intros hyp ; elimtype False ; discriminate
| |- Id ?t ?u -> _ => let hyp := fresh in
  intros hyp ; elimtype False ; solve [inversion hyp]
| |- ?x = ?y -> _ => let hyp := fresh in
  intros hyp ; (try (clear hyp ; fail 1)) ;
    case hyp
| |- Id _ ?x ?y -> _ => let hyp := fresh in
  intros hyp ; (try (clear hyp ; fail 1)) ;
    case hyp
| |- _ -> ?B => let ty := type of B in
  intro || (let H := fresh in intro H)
| |- forall x, _ =>
  let H := fresh x in intro H
| |- _ => intro
end.