introduction of `Eqdep.Eq_rect_eq.eq_rect_eq` (UIP) by the usage of `dependent destruction`

[jiangsy]

Print Assumptions rel_exp_of_typ_inversion1. (and also many other lemmas) will output

Axioms:
functional_extensionality_dep :
forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) ->
f = g
Eqdep.Eq_rect_eq.eq_rect_eq :
forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), x = eq_rect p Q x p h

By using the old inversion H5; subst instead of dependent destruction H5, Eqdep.Eq_rect_eq.eq_rect_eq will not be introduced. But many things need changing accordingly, so we probably don't want to fix all of them now.

Lemma rel_exp_of_typ_inversion1 : forall {Γ A A' i},
    {{ Γ ⊨ A ≈ A' : Type@i }} ->
    exists env_rel,
      {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }} /\
        forall ρ ρ' (equiv_ρ_ρ' : {{ Dom ρ ≈ ρ' ∈ env_rel }}),
          rel_exp A ρ A' ρ' (per_univ i).
Proof.
  intros * [env_relΓ].
  destruct_conjs.
  eexists;
  eexists; [eassumption |].
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ). 
  destruct_by_head rel_typ.
  inversion H2; subst.
  inversion H4; subst.
  progress simp per_univ_elem in H5;
  inversion  H5; subst; 
  try rewrite <- per_univ_elem_equation_1 in *.
  handle_per_univ_elem_irrel.
  eassumption.
Qed.

[Ailrun]

Does same thing happen for the main branch? I checked that (in the main branch) there's no axioms other than fun ext. Maybe some optimization caused the issue for prop-eq branch?

[jiangsy]

No, it's a new problem in ext/prop-eq. I think we can go back to this problem later. Just to mark this problem here in case we forget.

Updates: See discussions below

[Ailrun]

Oh then it's good. Once we finished a feature, we can find which dependent destructions cause the issue and replace them.

[Ailrun]

It turns out that the current main branch already uses UIP.
One can check it by running coqchk on the TypeCheck.vo or even LibTactics.vo.

[Ailrun]

Maybe coqchk only checks an existence of axiom in the dependence graph? LibTactics.vo does not define anything (other than some tactics) that uses UIP.

[jiangsy]

depedent destruction is very likely to use UIP (like the old pattern matching with K in agda), and Eqdep.Eq_rect_eq.eq_rect_eq is imported by Coq.Program.Equality, I think.

It's indeed a bit weird if coqchk outputs UIP for LibTactics.vo. I checked a few lemmas in LibTactics.v using Print Assumptions, and they all show Closed under the global context. But if you run Print Assumptions type_check_closed_complete. in TypeCheck.v in the main branch, UIP is still there.

Axioms:
functional_extensionality_dep :
forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
(forall x : A, f x = g x) -> f = g
Eqdep.Eq_rect_eq.eq_rect_eq :
forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h

[Ailrun]

We may need to replace it with dependent inversion if that helps.

[jiangsy]

I think "Maybe coqchk only checks an existence of axiom in the dependence graph" is true. If you create a file Test.v with just Require Import Coq.Program.Equality. and run coqchk on Test.vo, it outputs

* Axioms:
    Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq

[jiangsy]

We can create a new branch for this. It's a bit tedious task. I guess most dependent destruction H can be substituted by inversion H; subst (or dependent inversion but I'm not familiar with it). But there're some use cases we really make use of dependent destruction to rule out some cases in pattern matching, which could be non-trivial to find an alternative.

[Ailrun]

But there're some use cases we really make use of dependent destruction to rule out some cases in pattern matching, which could be non-trivial to find an alternative.

For such a case we can prove a lemma and use that lemma for the "destruction".

[jiangsy]

reopen when we merge ext/prop-eq (#287)

[Ailrun]

Note: we don't need to reopen this we resolved the UIP issue in the PR as well.