Library Equations.DepElim


Tactics related to (dependent) equality and proof irrelevance.

Require Import Coq.Program.Tactics.
Require Export Equations.Init.
Require Import Equations.Signature.
Require Import Equations.EqDec.
Require Equations.HSets.

Ltac is_ground_goal :=
  match goal with
    |- ?T => is_ground T
  end.

Try to find a contradiction.


We will use the block definition to separate the goal from the equalities generated by the tactic.

Definition block := tt.

Ltac intros_until_block :=
  match goal with
    |- let _ := block in _ => intros _
  | |- _ => try (intro; intros_until_block)
  end.

Ltac block_goal :=
  match goal with
    | [ |- ?T ] => change (let _ := block in T)
  end.

Ltac unblock_goal := unfold block in *; cbv zeta.

Notation for the single element of x = x.

Arguments eq_refl {A} {x}.

FIXME should not polute users
Global Set Keyed Unification.

A tactic that tries to remove trivial equality guards in induction hypotheses coming from dependent induction/generalize_eqs invocations.

Ltac simplify_IH_hyps := repeat
  match goal with
    | [ hyp : _ |- _ ] => simpl in hyp; eqns_specialize_eqs hyp; simpl in hyp
  end.

Support for the Equations command. These tactics implement the necessary machinery to solve goals produced by the Equations command relative to dependent pattern-matching. It is inspired from the "Eliminating Dependent Pattern-Matching" paper by Goguen, McBride and McKinna.
The NoConfusionPackage class provides a method for making progress on proving a property P implied by an equality on an inductive type I. The type of noConfusion for a given P should be of the form Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y , where NoConfusion P x y for constructor-headed x and y will give a formula ending in P. This gives a general method for simplifying by discrimination or injectivity of constructors.
Some actual instances are defined later in the file using the more primitive discriminate and injection tactics on which we can always fall back.

Class NoConfusionPackage (A : Type) := {
  NoConfusion : A -> A -> Prop;
  noConfusion : forall {a b}, a = b -> NoConfusion a b;
  noConfusion_inv : forall {a b}, NoConfusion a b -> a = b;
  noConfusion_is_equiv : forall {a b} (e : a = b), noConfusion_inv (noConfusion e) = e;
}.

Polymorphic Class NoConfusionIdPackage (A : Type) := {
  NoConfusionId : A -> A -> Type;
  noConfusionId : forall {a b}, Id a b -> NoConfusionId a b;
  noConfusionId_inv : forall {a b}, NoConfusionId a b -> Id a b;
  noConfusionId_is_equiv : forall {a b} (e : Id a b), Id (noConfusionId_inv (noConfusionId e)) e;
}.

Lemma apply_noConfusion {A} {noconf : NoConfusionPackage A}
      (p q : A) {B : p = q -> Type} :
  (forall H : NoConfusion p q, B (noConfusion_inv H)) -> (forall H : p = q, B H).
Proof.
  intros. generalize (noConfusion_is_equiv H).
  intros e. destruct e. apply X.
Defined.
Extraction Inline apply_noConfusion.

Polymorphic
Lemma apply_noConfusionId {A} {noconf : NoConfusionIdPackage A}
      (p q : A) {B : Id p q -> Type} :
  (forall e : NoConfusionId p q, B (noConfusionId_inv e)) -> (forall e : Id p q, B e).
Proof.
  intros. generalize (noConfusionId_is_equiv e). destruct e.
  intros <-. apply X.
Defined.
Extraction Inline apply_noConfusionId.

Apply noConfusion on a given hypothsis.

Ltac noconf_ref H :=
  match type of H with
    @eq ?A ?X ?Y =>
      let H' := fresh in assert (H':=noConfusion (A:=A) (a:=X) (b:=Y) H) ;
      clear H; hnf in H';
      match type of H' with
      | True => clear H'
      | False => elim H'
      | @eq _ _ _ => revert dependent H'
      | _ => fail
      end
  end.

Lemma False_rect_dep (P : False -> Type) : forall e : False, P e.
Proof. intros e. destruct e. Defined.

Lemma True_rect_dep (P : True -> Type) (m : P I) : forall e : True, P e.
Proof. intros e. destruct e. exact m. Defined.

Ltac blocked t := block_goal ; t ; unblock_goal.

The DependentEliminationPackage provides the default dependent elimination principle to be used by the equations resolver. It is especially useful to register the dependent elimination principles for things in Prop which are not automatically generated.

Polymorphic
Class DependentEliminationPackage (A : Type) :=
  { elim_type : Type ; elim : elim_type }.

A higher-order tactic to apply a registered eliminator.

Ltac elim_tac tac p :=
  let ty := type of p in
  let eliminator := eval simpl in (elim (A:=ty)) in
    tac p eliminator.

Specialization to do case analysis or induction. Note: the equations tactic tries case before elim_case: there is no need to register generated induction principles.

Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p.
Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.

Lemmas used by the simplifier, mainly rephrasings of eq_rect, eq_ind.

Lemma solution_left : forall {A} {B : A -> Type} (t : A), B t -> (forall x, x = t -> B x).
Proof. intros A B t H x eq. symmetry in eq. destruct eq. apply H. Defined.

Polymorphic
Lemma Id_solution_left : forall {A} {B : A -> Type} (t : A), B t -> (forall x, Id x t -> B x).
Proof. intros A B t H x eq. destruct eq. apply H. Defined.

Scheme eq_rect_dep := Induction for eq Sort Type.

Lemma eq_rect_dep_r {A} (x : A) (P : forall a, a = x -> Type) (p : P x eq_refl)
      (y : A) (e : y = x) : P y e.
Proof. destruct e. apply p. Defined.

Polymorphic
Definition Id_rect (A : Type) (x : A) (P : A -> Type) : P x -> forall y : A, Id x y -> P y.
Proof. intros Px y e. destruct e. exact Px. Defined.

Polymorphic
Definition Id_rect_r (A : Type) (x : A) (P : A -> Type) : P x -> forall y : A, Id y x -> P y.
Proof. intros Px y e. eapply (Id_rect _ x _ Px y (id_sym e)). Defined.

Polymorphic
Lemma Id_rect_dep_r {A} (x : A) (P : forall a, Id a x -> Type) (p : P x id_refl)
      (y : A) (e : Id y x) : P y e.
Proof. destruct e. apply p. Defined.

Lemma eq_sym_invol {A} (x y : A) (e : x = y) : eq_sym (eq_sym e) = e.
Proof. destruct e. reflexivity. Defined.

Lemma eq_symmetry_dep {A} {t : A} {B : forall (x : A), x = t -> Type} :
  (forall (x : A) (eq : t = x), B x (eq_sym eq)) ->
  (forall (x : A) (eq : x = t), B x eq).
Proof.
  intros. rewrite <- eq_sym_invol.
  generalize (eq_sym eq). apply X.
Defined.

Lemma solution_left_dep : forall {A} (t : A) {B : forall (x : A), (x = t -> Type)},
    B t eq_refl -> (forall x (Heq : x = t), B x Heq).
Proof.
  intros A t B H x eq. apply eq_symmetry_dep. clear eq. intros.
  destruct eq. exact H.
Defined.

Polymorphic
Lemma Id_solution_left_dep : forall {A} (t : A) {B : forall (x : A), (Id x t -> Type)},
    B t id_refl -> (forall x (Heq : Id x t), B x Heq).
Proof. intros A t B H x eq. destruct eq. apply H. Defined.

Lemma solution_right : forall {A} {B : A -> Type} (t : A), B t -> (forall x, t = x -> B x).
Proof. intros A B t H x eq. destruct eq. apply H. Defined.

Polymorphic
Lemma Id_solution_right : forall {A} {B : A -> Type} (t : A), B t -> (forall x, Id t x -> B x).
Proof. intros A B t H x eq. destruct eq. apply H. Defined.

Lemma solution_right_dep : forall {A} (t : A) {B : forall (x : A), (t = x -> Type)},
    B t eq_refl -> (forall x (Heq : t = x), B x Heq).
Proof. intros A t B H x eq. destruct eq. apply H. Defined.

Polymorphic
Lemma Id_solution_right_dep : forall {A} (t : A) {B : forall (x : A), (Id t x -> Type)},
    B t id_refl -> (forall x (Heq : Id t x), B x Heq).
Proof. intros A t B H x eq. destruct eq. apply H. Defined.

Lemma solution_left_let : forall {A} {B : A -> Type} (b : A) (t : A),
  (b = t -> B t) -> (let x := b in x = t -> B x).
Proof. intros A B b t H x eq. subst x. destruct eq. apply H. reflexivity. Defined.

Lemma solution_right_let : forall {A} {B : A -> Type} (b t : A),
  (t = b -> B t) -> (let x := b in t = x -> B x).
Proof. intros A B b t H x eq. subst x. destruct eq. apply H. reflexivity. Defined.

Polymorphic
Lemma Id_solution_left_let : forall {A} {B : A -> Type} (b : A) (t : A),
  (Id b t -> B t) -> (let x := b in Id x t -> B x).
Proof. intros A B b t H x eq. subst x. destruct eq. apply H. reflexivity. Defined.

Polymorphic
Lemma Id_solution_right_let : forall {A} {B : A -> Type} (b t : A),
  (Id t b -> B t) -> (let x := b in Id t x -> B x).
Proof. intros A B b t H x eq. subst x. destruct eq. apply H. reflexivity. Defined.

Lemma deletion : forall {A B} (t : A), B -> (t = t -> B).
Proof. intros; assumption. Defined.

Polymorphic
Lemma Id_deletion : forall {A B} (t : A), B -> (Id t t -> B).
Proof. intros; assumption. Defined.

If we have decidable equality on A we use this version which is axiom-free!

Polymorphic Lemma simplification_sigma2_dec@{i j} : forall {A : Type@{i}} `{EqDec A} {P : A -> Type@{i}}
                                                           {B : Type@{j}}
    (p : A) (x y : P p),
    (x = y -> B) -> (sigmaI P p x = sigmaI P p y -> B).
Proof. intros. apply X. apply inj_right_sigma in H0. assumption. Defined.

Polymorphic Lemma simplification_sigma2_dec_refl@{i j} :
  forall {A : Type@{i}} {eqdec:EqDec A} {P : A -> Type@{i}} {B : Type@{j}}
    (p : A) (x : P p) (G : x = x -> B),
      @simplification_sigma2_dec A eqdec P B p x x G eq_refl = G eq_refl.
Proof.
  intros. unfold simplification_sigma2_dec.
  rewrite inj_right_sigma_refl. reflexivity.
Defined.
Arguments simplification_sigma2_dec : simpl never.

Polymorphic Lemma simplification_sigma2_dec_point :
  forall {A : Type} (p : A) `{EqDecPoint A p} {P : A -> Type} {B : Type}
    (x y : P p),
    (x = y -> B) -> (sigmaI P p x = sigmaI P p y -> B).
Proof. intros. apply X. apply inj_right_sigma_point in H0. assumption. Defined.

Polymorphic Lemma simplification_sigma2_dec_point_refl@{i +} :
  forall {A} (p : A) `{eqdec:EqDecPoint A p} {P : A -> Type} {B}
    (x : P p) (G : x = x -> B),
      @simplification_sigma2_dec_point A p eqdec P B x x G eq_refl = G eq_refl.
Proof.
  intros. unfold simplification_sigma2_dec_point.
  rewrite inj_right_sigma_refl_point. reflexivity.
Defined.
Arguments simplification_sigma2_dec_point : simpl never.

Polymorphic Lemma Id_simplification_sigma2@{i j} :
  forall {A : Type@{i}} `{HSets.HSet A} {P : A -> Type@{i}} {B : Type@{j}}
         (p : A) (x y : P p),
  (Id x y -> B) -> (Id (sigmaI P p x) (sigmaI P p y) -> B).
Proof. intros. apply X. apply HSets.inj_sigma_r. exact X0. Defined.

Polymorphic
Lemma Id_simplification_sigma2_refl {A} `{HSets.HSet A} {P : A -> Type} {B}
(p : A) (x : P p) (e : Id x x -> B) :
  Id_simplification_sigma2 p x x e id_refl = e id_refl.
Proof.
  intros. unfold Id_simplification_sigma2.
  now rewrite HSets.inj_sigma_r_refl.
Defined.

Lemma simplification_existT1 : forall {A} {P : A -> Type} {B} (p q : A) (x : P p) (y : P q),
  (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
Proof.
  intros. refine (X _ H).
  change (projT1 (existT P p x) = projT1 (existT P q y)).
  now destruct H.
 Defined.

Local Open Scope equations_scope.
Import Sigma_Notations.

Polymorphic Lemma simplification_sigma1@{i j} : forall {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}} (p q : A) (x : P p) (y : P q),
  (p = q -> sigmaI P p x = sigmaI P q y -> B) -> (sigmaI P p x = sigmaI P q y -> B).
Proof.
  intros. refine (X _ H).
  change (pr1 &(p & x) = pr1 &(q & y)).
  now destruct H.
Defined.

Polymorphic Lemma Id_simplification_sigma1@{i j} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{i}}
            (p q : A) (x : P p) (y : P q) :
  (Id p q -> Id (sigmaI P p x) (sigmaI P q y) -> B) -> (Id (sigmaI P p x) (sigmaI P q y) -> B).
Proof.
  intros. refine (X _ X0).
  change (Id (pr1 &(p & x)) (pr1 &(q & y))).
  now destruct X0.
Defined.

Scheme Id_rew := Minimality for Id Sort Type.

Polymorphic Lemma eq_simplification_sigma1@{i j} {A : Type@{i}} {P : Type@{i}} {B : Type@{j}}
  (p q : A) (x : P) (y : P) :
  (p = q -> x = y -> B) ->
  (sigmaI (fun _ => P) p x = sigmaI (fun _ => P) q y -> B).
Proof.
  intros. revert X.
  change p with (pr1 &(p & x)).
  change q with (pr1 &(q & y)).
  change x with (pr2 &(p & x)) at 2.
  change y with (pr2 &(q & y)) at 2.
  destruct H.
  intros X. eapply (X eq_refl). apply eq_refl.
Defined.

Polymorphic Lemma Id_simplification_sigma1_nondep {A} {P : Type} {B}
  (p q : A) (x : P) (y : P) :
  (Id p q -> Id x y -> B) ->
  Id (sigmaI (fun _ => P) p x) (sigmaI (fun _ => P) q y) -> B.
Proof.
  intros. revert X.
  change p with (pr1 &(p & x)).
  change q with (pr1 &(q & y)).
  change x with (pr2 &(p & x)) at 2.
  change y with (pr2 &(q & y)) at 2.
  destruct X0.
  intros X. eapply (X id_refl). apply id_refl.
Defined.

Polymorphic Lemma eq_simplification_sigma1_dep@{i j} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}}
  (p q : A) (x : P p) (y : P q) :
  (forall e : p = q, (@eq_rect A p P x q e) = y -> B) ->
  (sigmaI P p x = sigmaI P q y -> B).
Proof.
  intros. revert X.
  change p with (pr1 &(p& x)).
  change q with (pr1 &(q & y)).
  change x with (pr2 &(p& x)) at 3.
  change y with (pr2 &(q & y)) at 4.
  destruct H.
  intros X. eapply (X eq_refl). apply eq_refl.
Defined.

Polymorphic Lemma Id_simplification_sigma1_dep {A} {P : A -> Type} {B}
  (p q : A) (x : P p) (y : P q) :
  (forall e : Id p q, Id (@Id_rect A p P x q e) y -> B) ->
  (Id (sigmaI P p x) (sigmaI P q y) -> B).
Proof.
  intros. revert X.
  change p with (pr1 &(p& x)).
  change q with (pr1 &(q & y)).
  change x with (pr2 &(p& x)) at 3.
  change y with (pr2 &(q & y)) at 4.
  destruct X0.
  intros X. eapply (X id_refl). apply id_refl.
Defined.

Polymorphic Definition pack_sigma_eq@{i} {A : Type@{i}} {P : A -> Type@{i}} {p q : A} {x : P p} {y : P q}
  (e' : p = q) (e : @eq_rect A p P x q e' = y) : &(p& x) = &(q & y).
Proof. destruct e'. simpl in e. destruct e. apply eq_refl. Defined.

Polymorphic Lemma eq_simplification_sigma1_dep_dep@{i j} {A : Type@{i}} {P : A -> Type@{i}}
  (p q : A) (x : P p) (y : P q) {B : &(p& x) = &(q & y) -> Type@{j}} :
  (forall e' : p = q, forall e : @eq_rect A p P x q e' = y, B (pack_sigma_eq e' e)) ->
  (forall e : sigmaI P p x = sigmaI P q y, B e).
Proof.
  intros. revert X.
  change p with (pr1 &(p & x)).
  change q with (pr1 &(q & y)).
  change x with (pr2 &(p & x)) at 3 5.
  change y with (pr2 &(q & y)) at 4 6.
  destruct e.
  intros X. simpl in *.
  apply (X eq_refl eq_refl).
Defined.

Polymorphic Definition pack_sigma_Id {A} {P : A -> Type} {p q : A} {x : P p} {y : P q}
  (e' : Id p q) (e : Id (@Id_rect A p P x q e') y) : Id &(p& x) &(q & y).
Proof. destruct e'. simpl in e. destruct e. apply id_refl. Defined.

Polymorphic Lemma Id_simplification_sigma1_dep_dep {A} {P : A -> Type}
  (p q : A) (x : P p) (y : P q) {B : Id &(p& x) &(q & y) -> Type} :
  (forall e' : Id p q, forall e : Id (@Id_rect A p P x q e') y, B (pack_sigma_Id e' e)) ->
  (forall e : Id (sigmaI P p x) (sigmaI P q y), B e).
Proof.
  intros. revert X.
  change p with (pr1 &(p & x)).
  change q with (pr1 &(q & y)).
  change x with (pr2 &(p & x)) at 3 5.
  change y with (pr2 &(q & y)) at 4 6.
  destruct e.
  intros X. simpl in *.
  apply (X id_refl id_refl).
Defined.

Polymorphic Lemma Id_simplification_sigma1'@{i j} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}} (p q : A) (x : P p) (y : P q) :
  (forall e : Id p q, Id (Id_rew A p P x q e) y -> B) ->
  (Id (sigmaI P p x) (sigmaI P q y) -> B).
Proof.
  intros. revert X.
  change p with (pr1 &(p & x)).
  change q with (pr1 &(q & y)).
  change x with (pr2 &(p & x)) at 3.
  change y with (pr2 &(q & y)) at 4.
  destruct X0.
  intros X. eapply (X id_refl). apply id_refl.
Defined.

Lemma simplification_K_dec : forall {A} `{EqDec A} (x : A) {B : x = x -> Type},
  B eq_refl -> (forall p : x = x, B p).
Proof. intros. apply K_dec. assumption. Defined.
Arguments simplification_K_dec : simpl never.

Lemma simplification_K_dec_refl : forall {A} `{EqDec A} (x : A) {B : x = x -> Type}
                                    (p : B eq_refl),
  simplification_K_dec x p eq_refl = p.
Proof.
  intros.
  unfold simplification_K_dec, K_dec.
  set (pf := eq_proofs_unicity eq_refl eq_refl).
  destruct (eq_proofs_unicity eq_refl pf).
  reflexivity.
Defined.

Polymorphic
Lemma Id_simplification_K : forall {A} `{HSets.HSet A} (x : A) {B : Id x x -> Type},
  B id_refl -> (forall p : Id x x, B p).
Proof. intros. apply HSets.K. assumption. Defined.

Polymorphic
Lemma Id_simplification_K_refl : forall {A} `{HSets.HSet A} (x : A) {B : Id x x -> Type}
  (b : B id_refl), Id_simplification_K x b id_refl = b.
Proof.
  intros. pose HSets.K.
  unfold Id_simplification_K.
  unfold HSets.K. rewrite HSets.is_hset_refl. constructor.
Defined.

Polymorphic
Definition ind_pack_eq@{i} {A : Type@{i}} {B : A -> Type@{i}} {x : A} {p q : B x} (e : p = q) :
  @eq (sigma A (fun x => B x)) &(x & p) &(x & q).
Proof. destruct e. reflexivity. Defined.

Polymorphic
Definition ind_pack_eq_inv@{i} {A : Type@{i}} {eqdec : EqDec A}
           {B : A -> Type@{i}} (x : A) (p q : B x) (e : @eq (sigma A (fun x => B x)) &(x & p) &(x & q)) : p = q.
Proof. revert e. apply simplification_sigma2_dec@{i i}. apply id. Defined.

Polymorphic
Definition ind_pack_eq_inv_refl@{i} {A : Type@{i}} {eqdec : EqDec A}
           {B : A -> Type@{i}} {x : A} (p : B x) :
  ind_pack_eq_inv _ _ _ (@eq_refl _ &(x & p)) = eq_refl.
Proof.
  unfold ind_pack_eq_inv. simpl. unfold simplification_sigma2_dec.
  unfold id. apply inj_right_sigma_refl.
Defined.

Polymorphic
Definition ind_pack_eq_inv_equiv@{i} {A : Type@{i}} {eqdec : EqDec A}
           {B : A -> Type@{i}} {x : A} (p q : B x) (e : p = q) :
  ind_pack_eq_inv _ _ _ (ind_pack_eq e) = e.
Proof.
  destruct e. apply ind_pack_eq_inv_refl.
Defined.

Polymorphic
Definition opaque_ind_pack_eq_inv@{i j} {A : Type@{i}} {eqdec : EqDec A}
  {B : A -> Type@{i}} {x : A} {p q : B x} (G : p = q -> Type@{j}) (e : &(x & p) = &(x & q)) :=
  let e' := @ind_pack_eq_inv A eqdec B x p q e in G e'.
Arguments opaque_ind_pack_eq_inv : simpl never.

Polymorphic
Lemma simplify_ind_pack@{i j} {A : Type@{i}} {eqdec : EqDec A}
      (B : A -> Type@{i}) (x : A) (p q : B x) (G : p = q -> Type@{j}) :
      (forall e : &(x & p) = &(x & q), opaque_ind_pack_eq_inv G e) ->
  (forall e : p = q, G e).
Proof.
  intros H. intros e.
  specialize (H (ind_pack_eq e)). unfold opaque_ind_pack_eq_inv in H.
  rewrite ind_pack_eq_inv_equiv in H. apply H.
Defined.
Arguments simplify_ind_pack : simpl never.

Polymorphic
Lemma simplify_ind_pack_inv@{i j} {A : Type@{i}} {eqdec : EqDec A}
      (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j}) :
  G eq_refl -> opaque_ind_pack_eq_inv G eq_refl.
Proof.
  intros H. unfold opaque_ind_pack_eq_inv.
  rewrite ind_pack_eq_inv_refl. apply H.
Defined.
Arguments simplify_ind_pack_inv : simpl never.

Polymorphic
Definition simplified_ind_pack@{i j} {A : Type@{i}} {eqdec : EqDec A}
  (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j})
  (t : opaque_ind_pack_eq_inv G eq_refl) :=
  eq_rect _ G t _ (@ind_pack_eq_inv_refl A eqdec B x p).
Arguments simplified_ind_pack : simpl never.

Polymorphic
Lemma simplify_ind_pack_refl@{i j} {A : Type@{i}} {eqdec : EqDec A}
(B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j})
(t : forall (e : &(x & p) = &(x & p)), opaque_ind_pack_eq_inv G e) :
  simplify_ind_pack B x p p G t eq_refl =
  simplified_ind_pack B x p G (t eq_refl).
Proof. reflexivity. Qed.

Polymorphic
Lemma simplify_ind_pack_elim@{i j} {A : Type@{i}} {eqdec : EqDec A}
  (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j})
  (t : G eq_refl) :
  simplified_ind_pack B x p G (simplify_ind_pack_inv B x p G t) = t.
Proof.
  unfold simplified_ind_pack, simplify_ind_pack_inv.
  destruct (ind_pack_eq_inv_refl p). reflexivity.
Qed.

For the Id equality type

Polymorphic
Definition ind_pack_Id {A : Type} {B : A -> Type} {x : A} {p q : B x} (e : Id p q) :
  @Id (sigma A (fun x => B x)) &(x & p) &(x & q).
Proof. destruct e. reflexivity. Defined.

Polymorphic
Definition ind_pack_Id_inv {A : Type} {eqdec : HSets.HSet A}
           {B : A -> Type} (x : A) (p q : B x) (e : @Id (sigma A (fun x => B x)) &(x & p) &(x & q)) : Id p q.
Proof. revert e. apply Id_simplification_sigma2. apply id. Defined.

Polymorphic
Definition ind_pack_Id_inv_refl {A : Type} {eqdec : HSets.HSet A}
           {B : A -> Type} {x : A} (p : B x) :
  Id (ind_pack_Id_inv _ _ _ (@id_refl _ &(x & p))) id_refl.
Proof.
  unfold ind_pack_Id_inv. simpl. unfold Id_simplification_sigma2.
  unfold id. apply HSets.inj_sigma_r_refl.
Defined.

Polymorphic
Definition ind_pack_Id_inv_equiv {A : Type} {eqdec : HSets.HSet A}
           {B : A -> Type} {x : A} (p q : B x) (e : Id p q) :
  Id (ind_pack_Id_inv _ _ _ (ind_pack_Id e)) e.
Proof.
  destruct e. apply ind_pack_Id_inv_refl.
Defined.

Polymorphic
Definition opaque_ind_pack_Id_inv {A : Type} {eqdec : HSets.HSet A}
  {B : A -> Type} {x : A} {p q : B x} (G : Id p q -> Type) (e : Id &(x & p) &(x & q)) :=
  let e' := @ind_pack_Id_inv A eqdec B x p q e in G e'.
Arguments opaque_ind_pack_Id_inv : simpl never.

Polymorphic
Lemma Id_simplify_ind_pack {A : Type} {eqdec : HSets.HSet A}
      (B : A -> Type) (x : A) (p q : B x) (G : Id p q -> Type) :
      (forall e : Id &(x & p) &(x & q), opaque_ind_pack_Id_inv G e) ->
  (forall e : Id p q, G e).
Proof.
  intros H. intros e.
  specialize (H (ind_pack_Id e)). unfold opaque_ind_pack_Id_inv in H.
  rewrite ind_pack_Id_inv_equiv in H. apply H.
Defined.
Arguments Id_simplify_ind_pack : simpl never.

Polymorphic
Lemma Id_simplify_ind_pack_inv {A : Type} {eqdec : HSets.HSet A}
      (B : A -> Type) (x : A) (p : B x) (G : Id p p -> Type) :
  G id_refl -> opaque_ind_pack_Id_inv G id_refl.
Proof.
  intros H. unfold opaque_ind_pack_Id_inv.
  rewrite ind_pack_Id_inv_refl. apply H.
Defined.
Arguments Id_simplify_ind_pack_inv : simpl never.

All the simplification rules involving axioms are treated as opaque when proving lemmas about definitions. To actually compute with these inside Coq, one has to make them transparent again.

Global Opaque simplification_sigma2_dec
       simplification_sigma2_dec_point
       simplification_K_dec
       simplify_ind_pack simplified_ind_pack Id_simplification_sigma2.
Global Opaque opaque_ind_pack_eq_inv.

Ltac rewrite_sigma2_refl_noK :=
  match goal with
  | |- context [@inj_right_sigma ?A ?H ?x ?P ?y ?y' _] =>
    rewrite (@inj_right_sigma_refl A H x P y)

  | |- context [@Id_simplification_sigma2 ?A ?H ?P ?B ?p ?x ?y ?X id_refl] =>
    rewrite (@Id_simplification_sigma2_refl A H P B p x X); simpl

  | |- context [@simplification_sigma2_dec ?A ?H ?P ?B ?p ?x ?y ?X eq_refl] =>
    rewrite (@simplification_sigma2_dec_refl A H P B p x X); simpl

  | |- context [@simplification_sigma2_dec_point ?A ?p ?H ?P ?B ?x ?y ?X eq_refl] =>
    rewrite (@simplification_sigma2_dec_point_refl A p H P B x X); simpl

  | |- context [@simplification_K_dec ?A ?dec ?x ?B ?p eq_refl] =>
    rewrite (@simplification_K_dec_refl A dec x B p); simpl eq_rect

  | |- context [@Id_simplification_K ?A ?dec ?x ?B ?p id_refl] =>
    rewrite (@Id_simplification_K_refl A dec x B p); simpl Id_rect

  | |- context [@HSets.inj_sigma_r ?A ?H ?P ?x ?y ?y' _] =>
    rewrite (@HSets.inj_sigma_r_refl A H P x y)

  | |- context [@simplify_ind_pack ?A ?eqdec ?B ?x ?p _ ?G _ eq_refl] =>
    rewrite (@simplify_ind_pack_refl A eqdec B x p G _)

  | |- context [@simplified_ind_pack ?A ?eqdec ?B ?x ?p ?G
        (simplify_ind_pack_inv _ _ _ _ ?t)] =>
    rewrite (@simplify_ind_pack_elim A eqdec B x p G t)
  end.

Ltac rewrite_sigma2_refl := rewrite_sigma2_refl_noK.

This hint database and the following tactic can be used with autounfold to unfold everything to eq_rects.

Hint Unfold solution_left solution_right
  eq_sym_invol eq_symmetry_dep
  solution_left_dep solution_right_dep deletion
  simplification_existT1 simplification_sigma1
  eq_simplification_sigma1 eq_simplification_sigma1_dep
  Id_solution_left Id_solution_right Id_deletion
  Id_solution_left_dep Id_solution_right_dep
  Id_solution_right_let Id_solution_left_let
  Id_simplification_sigma1
  apply_noConfusion apply_noConfusionId
  eq_rect_r eq_rec eq_ind eq_ind_r
  Id_rect_r : equations.

Makes these definitions disappear at extraction time
Extraction Inline solution_right_dep solution_right solution_left solution_left_dep.
Extraction Inline eq_sym_invol eq_symmetry_dep.
Extraction Inline solution_right_let solution_left_let deletion.
Extraction Inline simplification_existT1.
Extraction Inline simplification_sigma1 simplification_sigma2_dec.
Extraction Inline simplification_K_dec.
Extraction Inline Id_solution_right_dep Id_solution_right Id_solution_left Id_solution_left_dep.
Extraction Inline Id_solution_right_let Id_solution_left_let Id_deletion.
Extraction Inline eq_simplification_sigma1 eq_simplification_sigma1_dep.
Extraction Inline Id_simplification_sigma1 Id_simplification_sigma2 Id_simplification_K.

Simply unfold as much as possible.

Ltac unfold_equations := repeat progress autounfold with equations.
Ltac unfold_equations_in H := repeat progress autounfold with equations in H.

Ltac rewrite_refl_id :=
  repeat (progress (autorewrite with refl_id) || (try rewrite_sigma2_refl)).

Ltac simplify_equations_in e :=
  repeat progress (autounfold with equations in e ; simpl in e).

Using these we can make a simplifier that will perform the unification steps needed to put the goal in normalised form (provided there are only constructor forms). Compare with the lemma 16 of the paper. We don't have a noCycle procedure yet.

Ltac block_equality id :=
  match type of id with
    | @eq ?A ?t ?u => change (let _ := block in (@eq A t u)) in id
    | _ => idtac
  end.

Ltac revert_blocking_until id :=
  Tactics.on_last_hyp ltac:(fun id' =>
    match id' with
      | id => idtac
      | _ => block_equality id' ; revert id' ; revert_blocking_until id
    end).

Ltac not_var x := try (is_var x; fail 1).

These two tactics are dangerous as they can try to reduce terms to head-normal-form and take ages to fail.
Ltac try_discriminate := discriminate.
Ltac try_injection H := injection H.

Ltac simplify_one_dep_elim :=
  match goal with
    | [ |- context [eq_rect_r _ _ eq_refl]] => simpl eq_rect_r
    | [ |- context [eq_rect _ _ _ _ eq_refl]] => simpl eq_rect
    | [ |- context [@eq_rect_dep_r _ _ _ _ _ eq_refl]] => simpl eq_rect_dep_r
    | [ |- context [@Id_rect_dep_r _ _ _ _ _ id_refl]] => simpl Id_rect_dep_r
    | [ |- context [noConfusion_inv _]] => simpl noConfusion_inv
    | [ |- @opaque_ind_pack_eq_inv ?A ?eqdec ?B ?x ?p _ ?G eq_refl] =>
            apply (@simplify_ind_pack_inv A eqdec B x p G)
    | [ |- let _ := block in _ ] => fail 1
    | [ |- _ ] => (simplify * || simplify ?); cbv beta
    | [ |- _ -> ?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.

Repeat until no progress is possible. By construction, it should leave the goal with no remaining equalities generated by the generalize_eqs tactic.

Ltac simplify_dep_elim := repeat simplify_one_dep_elim.

Ltac Equations.Init.noconf H ::= blocked ltac:(noconf_ref H ; simplify_dep_elim).

Reverse and simplify.

Ltac simpdep := reverse; simplify_dep_elim.

Decompose existential packages.

Ltac decompose_exists id id' := hnf in id ;
  match type of id with
    | @sigma _ _ => let xn := fresh id "'" in
      destruct id as [xn id]; decompose_exists xn id;
        cbv beta delta [ pr1 pr2 ] iota in id, id';
          decompose_exists id id'
    | _ => cbv beta delta [ pr1 pr2 ] iota in id, id'
  end.

Dependent generalization using existentials only.

Ltac generalize_sig_gen id cont :=
  let id' := fresh id in
  get_signature_pack id id';
  hnf in (value of id'); hnf in (type of id');
  lazymatch goal with
  | id' := ?v |- context[ id ] =>
    generalize (@eq_refl _ id' : v = id') ;
    clearbody id'; simpl in id';
    cont id id' id v
  | id' := ?v |- _ =>
    let id'1 := fresh id' in let id'2 := fresh id' in
    set (id'2 := pr2 id'); set (id'1 := pr1 id') in id'2;
    hnf in (value of id'1), (value of id'2);
    try red in (type of id'2);
    match goal with
      [ id'1 := ?t |- _ ] =>
      generalize (@eq_refl _ id'1 : t = id'1);
        clearbody id'2 id'1; clear id' id;
        try unfold signature in id'2; hnf in id'2; simpl in id'2;
        rename id'2 into id; cont id id id'1 t
    end
  end.

Ltac generalize_sig id cont :=
  generalize_sig_gen id
    ltac:(fun id id' id'1 t =>
            try rename id into id', id' into id;
          cont id'1 id).

Ltac generalize_sig_vars id cont :=
  generalize_sig_gen id
    ltac:(fun id id' id'1 t => move_after_deps id' t; revert_until id';
          rename id' into id; cont id'1 id).

Ltac Id_generalize_sig_gen id cont :=
  let id' := fresh id in
  get_signature_pack id id';
  hnf in (value of id'); hnf in (type of id');
  lazymatch goal with
  | id' := ?v |- context[ id ] =>
    generalize (@id_refl _ id' : Id id' id') ;
    unfold id' at 1;
    clearbody id'; simpl in id';
    cont id id' id' v
  | id' := ?v |- _ =>
    let id'1 := fresh id' in let id'2 := fresh id' in
    set (id'2 := pr2 id'); set (id'1 := pr1 id') in id'2;
    hnf in (value of id'1), (value of id'2);
    match goal with
    | [ id'1 := ?t |- _ ] =>
      generalize (@id_refl _ id'1 : Id t id'1);
        clearbody id'2 id'1;
        clear id' id; compute in id'2;
        rename id'2 into id; cont id id id'1 v
    end
  end.

Ltac Id_generalize_sig id cont :=
  Id_generalize_sig_gen id
    ltac:(fun id id' id'1 t =>
            try rename id into id', id' into id;
          cont id'1 id).

Ltac Id_generalize_sig_vars id cont :=
  Id_generalize_sig_gen id
    ltac:(fun id id' id'1 t => move_after_deps id' t; revert_until id';
          rename id' into id; cont id'1 id).

Ltac generalize_sig_dest id :=
  generalize_sig id ltac:(fun id id' => decompose_exists id id').

Ltac generalize_sig_vars_dest id :=
  generalize_sig_vars id ltac:(fun id id' => decompose_exists id id').

Ltac generalize_eqs_sig id :=
  (needs_generalization id ; generalize_sig_dest id)
    || idtac.

Ltac generalize_eqs_vars_sig id :=
  (needs_generalization id ; generalize_sig_vars_dest id)
    || idtac.

The default implementation of generalization using sigma types.

Ltac generalize_by_eqs id := generalize_eqs_sig id.
Ltac generalize_by_eqs_vars id := generalize_eqs_vars_sig id.

Do dependent elimination of the last hypothesis, but not simplifying yet (used internally).

Ltac destruct_last :=
  on_last_hyp ltac:(fun id => simpl in id ; generalize_by_eqs id ; destruct id).

The rest is support tactics for the Equations command.
Notation for inaccessible patterns.

Definition inaccessible_pattern {A : Type} (t : A) := t.

Module Inaccessible_Notations.

  Notation "?( t )" := (inaccessible_pattern t) (format "?( t )") : equations_scope.

End Inaccessible_Notations.

Import Inaccessible_Notations.

Definition hide_pattern {A : Type} (t : A) := t.

Definition add_pattern {B} (A : Type) (b : B) := A.

To handle sections, we need to separate the context in two parts: variables introduced by the section and the rest. We introduce a dummy variable between them to indicate that.

CoInductive end_of_section := the_end_of_the_section.

Ltac set_eos := let eos := fresh "eos" in
  assert (eos:=the_end_of_the_section).

Ltac with_eos_aux tac :=
  match goal with
   [ H : end_of_section |- _ ] => tac H
  end.

Ltac with_eos tac orelse :=
  with_eos_aux tac + orelse.

Ltac clear_nonsection :=
  repeat match goal with
    [ H : ?T |- _ ] =>
    match T with
      end_of_section => idtac
    | _ => clear H
    end
  end.

We have a specialized reverse_local tactic to reverse the goal until the begining of the section variables

Ltac reverse_local :=
  match goal with
    | [ H : ?T |- _ ] =>
      match T with
        | end_of_section => idtac
        | _ => revert H ; reverse_local
      end
    | _ => idtac
  end.

Ltac clear_local :=
  match goal with
    | [ H : ?T |- _ ] =>
      match T with
        | end_of_section => idtac
        | _ => clear H ; clear_local
      end
    | _ => idtac
  end.

Do as much as possible to apply a method, trying to get the arguments right. !!Unsafe!! We use auto for the _nocomp variant of Equations, in which case some non-dependent arguments of the method can remain after apply.

Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m).

Hopefully the first branch suffices.

Ltac try_intros m :=
  solve [ (intros_until_block ; refine m || (unfold block ; apply m)) ; auto ] ||
  solve [ unfold block ; simpl_intros m ] ||
  solve [ unfold block ; intros ; rapply m ; eauto ].

To solve a goal by inversion on a particular target.

Ltac do_empty id :=
  elimtype False ; simpl in id ;
  solve [ generalize_by_eqs id ; destruct id ; simplify_dep_elim
    | apply id ; eauto with Below ].

Ltac solve_empty target :=
  do_nat target intro ; on_last_hyp ltac:(do_empty).

Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local.

Ltac clear_fix_protos n tac :=
  match goal with
    | [ |- (let _ := fixproto in _) -> _ ] => intros _ ;
      match n with
        | O => fail 2 "clear_fix_proto: tactic would apply on prototype"
        | S ?n => clear_fix_protos n tac
      end
    | [ |- let _ := block in _ ] => reverse_local ; tac n
    | _ => reverse_local ; tac n
  end.

Solving a method call: we can solve it by splitting on an empty family member or we must refine the goal until the body can be applied.

Ltac solve_method rec :=
  match goal with
    | [ H := ?body : nat |- _ ] => subst H ; clear ; clear_fix_protos body
      ltac:(fun n => abstract (simplify_method idtac ; solve_empty n))
    | [ H := ?body : ?T |- _ ] =>
      (revert_until H; clear H);
      simplify_method ltac:(exact body) ; rec ;
      try (exact (body : T)) ; try_intros (body:T)
  end.

Impossible cases, by splitting on a given target.

Ltac solve_split :=
  match goal with
    | [ |- let split := ?x in _ ] => intros _ ;
      clear_fix_protos x ltac:(fun n => clear ; abstract (solve_empty n))
  end.

If defining recursive functions, the prototypes come first.

Ltac introduce p := first [
  match p with _ =>
    generalize dependent p ; intros p
  end
  | intros until p | intros until 1 | intros ].

Ltac do_case p := introduce p ; (elim_case p || destruct p || (case p ; clear p)).
Ltac do_ind p := introduce p ; (elim_ind p || induction p).

Ltac case_last := block_goal ;
  on_last_hyp ltac:(fun p => simpl in p ; try simplify_equations_in p ; generalize_by_eqs p ; do_case p).

Ltac nonrec_equations :=
  solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ]
    || fail "Unnexpected equations goal".

Ltac recursive_equations :=
  solve [solve_equations (case_last) (solve_method ltac:(intro))] || solve [ solve_split ]
    || fail "Unnexpected recursive equations goal".

The equations tactic is the toplevel tactic for solving goals generated by Equations.

Ltac equations := set_eos ;
  match goal with
    | [ |- forall x : _, _ ] => intro ; recursive_equations
    | [ |- let x := _ in ?T ] => intro x ; exact x
    | _ => nonrec_equations
  end.

The following tactics allow to do induction on an already instantiated inductive predicate by first generalizing it and adding the proper equalities to the context, in a maner similar to the BasicElim tactic of "Elimination with a motive" by Conor McBride.
The do_depelim higher-order tactic takes an elimination tactic as argument and an hypothesis and starts a dependent elimination using this tactic.

Ltac is_introduced H :=
  match goal with
    | [ H' : _ |- _ ] => match H' with H => idtac end
  end.

Tactic Notation "intro_block" hyp(H) :=
  (is_introduced H ; block_goal ; revert_until H ; block_goal) ||
    (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).

Tactic Notation "intro_block_id" ident(H) :=
  (is_introduced H ; block_goal ; revert_until H ; block_goal) ||
    (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).

Ltac unblock_dep_elim :=
  match goal with
    | |- let _ := block in ?T =>
      match T with context [ block ] =>
        change T ; intros_until_block
      end
    | _ => unblock_goal
  end.

Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_dep_elim.

Ltac do_intros H :=
  (try intros until H) ; (intro_block_id H || intro_block H) ;
  (try simpl in H ; simplify_equations_in H).

Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_by_eqs H ; tac H.

Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim; unblock_goal.

Ltac do_depind tac H :=
  (try intros until H) ; intro_block H ; (try simpl in H ; simplify_equations_in H) ;
  generalize_by_eqs_vars H ; tac H ; simpl_dep_elim; unblock_goal.

To dependent elimination on some hyp.

Ltac Equations.Init.depelim id ::= do_depelim ltac:(fun hyp => do_case hyp) id.

Ltac depelim_term c :=
  let H := fresh "term" in
    set (H:=c) in *; clearbody H ; depelim H.

Used internally.

Ltac depelim_nosimpl id := do_depelim_nosimpl ltac:(fun hyp => do_case hyp) id.

To dependent induction on some hyp.

Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.

A variant where generalized variables should be given by the user.

Ltac do_depelim' tac H :=
  (try intros until H) ; block_goal ; generalize_by_eqs H ; tac H ; simplify_dep_elim ;
    simplify_IH_hyps ; unblock_goal.

Calls destruct on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices.

Tactic Notation "dependent" "destruction" ident(H) :=
  do_depelim' ltac:(fun hyp => do_case hyp) H.

Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) :=
  do_depelim' ltac:(fun hyp => destruct hyp using c) H.

This tactic also generalizes the goal by the given variables before the elimination.

Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) :=
  do_depelim' ltac:(fun hyp => revert l ; do_case hyp) H.

Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
  do_depelim' ltac:(fun hyp => revert l ; destruct hyp using c) H.

Then we have wrappers for usual calls to induction. One can customize the induction tactic by writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before calling induction.

Tactic Notation "dependent" "induction" ident(H) :=
  do_depind ltac:(fun hyp => do_ind hyp) H.

Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
  do_depind ltac:(fun hyp => induction hyp using c) H.

This tactic also generalizes the goal by the given variables before the induction.

Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :=
  do_depelim' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.

Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
  do_depelim' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.

For treating impossible cases. Equations corresponding to impossible calls form instances of ImpossibleCall (f args).

Class ImpossibleCall {A : Type} (a : A) : Type :=
  is_impossible_call : False.

We have a trivial elimination operator for impossible calls.

Definition elim_impossible_call {A} (a : A) {imp : ImpossibleCall a} (P : A -> Type) : P a :=
  match is_impossible_call with end.

The tactic tries to find a call of f and eliminate it.

Ltac impossible_call f := on_call f ltac:(fun t => apply (elim_impossible_call t)).

solve_equation is used to prove the equation lemmas for an existing definition.

Ltac find_empty := simpl in * ; elimtype False ;
  match goal with
    | [ H : _ |- _ ] => solve [ clear_except H ; depelim H | eqns_specialize_eqs H ; assumption ]
    | [ H : _ <> _ |- _ ] => solve [ red in H ; eqns_specialize_eqs H ; assumption ]
  end.

Ltac make_simplify_goal :=
  match goal with
    [ |- @eq ?A ?T ?U ] => let eqP := fresh "eqP" in
      set (eqP := fun x : A => x = U) ; change (eqP T)
  | [ |- @Id ?A ?T ?U ] => let eqP := fresh "eqP" in
      set (eqP := fun x : A => @Id A x U) ; change (eqP T)
  end.

Ltac hnf_gl :=
  match goal with
    [ |- ?P ?T ] => let T' := eval hnf in T in
      convert_concl_no_check (P T')
  end.

Ltac hnf_eq :=
  match goal with
    |- ?x = ?y =>
      let x' := eval hnf in x in
      let y' := eval hnf in y in
        convert_concl_no_check (x' = y')
  | |- Id ?x ?y =>
    let x' := eval hnf in x in
    let y' := eval hnf in y in
        convert_concl_no_check (Id x' y')
  end.

Ltac red_eq :=
  match goal with
    |- ?x = ?y =>
    let rec reduce_eq x y :=
      let x' := eval red in x in
      let y' := eval red in y in
          reduce_eq x' y' || convert_concl_no_check (x' = y')
      in reduce_eq x y
  | |- Id ?x ?y =>
    let x' := eval hnf in x in
    let y' := eval hnf in y in
        convert_concl_no_check (Id x' y')
  end.

Ltac red_gl :=
  match goal with
    |- ?P ?x =>
    let rec reduce x :=
      let x' := eval red in x in
        reduce x' || convert_concl_no_check (P x')
      in reduce x
  end.

Ltac rewrite_sigma2_rule_noK c :=
  match c with
  | @inj_right_sigma ?A ?H ?x ?P ?y ?y' _ =>
    rewrite (@inj_right_sigma_refl A H x P y)
  | @simplify_ind_pack ?A ?eqdec ?B ?x ?p _ ?G _ eq_refl=>
    rewrite (@simplify_ind_pack_refl A eqdec B x p G _)
  | @Id_simplification_sigma2 ?A ?H ?P ?B ?p ?x ?y ?X id_refl=>
    rewrite (@Id_simplification_sigma2_refl A H P B p x X); simpl
  | @simplification_sigma2_dec ?A ?H ?P ?B ?p ?x ?y ?X eq_refl=>
    rewrite (@simplification_sigma2_dec_refl A H P B p x X); simpl
  | @simplification_sigma2_dec_point ?A ?p ?H ?P ?B ?x ?y ?X eq_refl=>
    rewrite (@simplification_sigma2_dec_point_refl A p H P B x X); simpl
  | @simplification_K_dec ?A ?dec ?x ?B ?p eq_refl=>
    rewrite (@simplification_K_dec_refl A dec x B p); simpl eq_rect
  | @HSets.inj_sigma_r ?A ?H ?P ?x ?y ?y' _=>
    rewrite (@HSets.inj_sigma_r_refl A H P x y)
  end.

Ltac rewrite_sigma2_rule c :=
  rewrite_sigma2_rule_noK c.

Ltac rewrite_sigma2_term x :=
  match x with
   | ?f _ _ _ _ _ _ _ _ _ => rewrite_sigma2_rule f
   | ?f _ _ _ _ _ _ _ _ => rewrite_sigma2_rule f
   | ?f _ _ _ _ _ _ _ => rewrite_sigma2_rule f
   | ?f _ _ _ _ _ _ => rewrite_sigma2_rule f
   | ?f _ _ _ _ _ => rewrite_sigma2_rule f
   | ?f _ _ _ _ => rewrite_sigma2_rule f
   | ?f _ _ _ => rewrite_sigma2_rule f
   | ?f _ _ => rewrite_sigma2_rule f
   | ?f _ => rewrite_sigma2_rule f
   | ?f => rewrite_sigma2_rule f
  end.

Ltac rewrite_sigma2_refl_eq :=
  match goal with
    |- ?x = ?y => rewrite_sigma2_term x || rewrite_sigma2_term y
  end.

Ltac rewrite_sigma2_refl_goal :=
  match goal with
  | |- ?P ?x => rewrite_sigma2_term x
  end.



Ltac simpl_equations :=
  repeat (repeat (simpl; hnf_eq; rewrite_refl_id);
          try progress autounfold with equations).

Ltac simpl_equation_impl :=
  repeat (unfold_equations; rewrite_refl_id).

Ltac simplify_equation c :=
  make_simplify_goal; simpl;
  repeat (try autounfold_ref c;
          progress (simpl; unfold_equations) ||
          (progress (autorewrite with refl_id)) ||
          reflexivity ||
          (progress (rewrite_sigma2_refl))).

Ltac solve_equation c :=
  intros ; try simplify_equation c ; try
    (match goal with
       | [ |- ImpossibleCall _ ] => elimtype False ; find_empty
       | _ => try red; try (reflexivity || discriminates)
     end).