Trying to use 'Equations'

Question

Examples from Chlipala's book https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html

Require Import Bool Arith List Program.
From Equations Require Import Equations.
Set Equations Transparent.
Set Keyed Unification.
Set Implicit Arguments.

Parameter A : Set.

Inductive ilist : nat -> Set :=
  | Nil : ilist 0
  | Cons : forall n, A -> ilist n -> ilist (S n).   

Equations length (ls : list A) : nat :=
  length nil := 0;
  length (cons h t) := S (length t). 

Equations inject (ls : list A) : ilist (length ls) :=
  inject nil := Nil;
  inject (cons h t) := Cons h (inject t).

Equations unject n (ls : ilist n) : list A :=
  unject Nil := nil;
  unject (Cons x ls) := cons x (unject ls).

Theorem unject_inverse : forall ls, unject (inject ls) = ls.
  Proof.
  intros.
  funelim (inject ls); simp unject; congruence.
  Qed.

Theorem length_inverse : forall n (ls : ilist n), length (unject ls) = n.
  Proof.
  intros.
  funelim (unject ls); simp length; congruence.
  Qed.

Now I want to prove

Theorem inject_inverse (n:nat) (ls : ilist n) :  inject (unject ls) = ls.

but the left and right parts are of different types. I can prove the following (without using Equations)

Theorem inject_inverse (n:nat) (ls : ilist n) (pf : length (unject ls) = n) :
ls =
match pf with
| eq_refl => inject (unject ls)
end.

Proof.
induction ls.
rewrite  (UIP_refl _ _ pf).
unfold unject.
unfold inject.
reflexivity.
unfold unject.
unfold inject.
fold unject.
fold inject.
unfold unject in pf.
unfold length in pf.
fold unject in pf.
fold length in pf.
unfold unject.
unfold inject.
fold unject.
fold inject.
injection pf; intro pf'.
rewrite (IHls pf') at 1.
generalize (inject (unject ls)).
generalize pf pf'.
unfold length.
fold length.
rewrite pf'.
intros.
rewrite  (UIP_refl _ _ pf0).
rewrite  (UIP_refl _ _ pf'0).
reflexivity.
Qed.

Can I make this shorter and better using Equations?

Answer 1

There is some inherent complexity coming from the use of dependent types. However, here is a clean-up version. The core idea is roughly the same as in your proof.

Notation "e # t" := (Logic.transport _ e t) (at level 50, only parsing).

Theorem inject_inverse (n:nat) (ls : ilist n) : ls = (length_inverse _) # inject (unject ls).
Proof.
  funelim (unject ls).
  - cbn.
    now rewrite (uip _ eq_refl).
  - cbn.
    rewrite H at 1 ; clear H.
    generalize (length_inverse ls) ; intros e.
    generalize (inject (unject ls)) (length_inverse (Cons x ls)) ; cbn ; rewrite e.
    intros ; cbn.
    now erewrite (uip _ eq_refl).
Qed.

Note in particular the following:

• use of the cbn simplification tactic instead of manual unfolding/refolding
• notation for transport to tidy up the goals
• use of uip over UIP_refl, the former does not rely on any axioms, instead it uses the fact that one can prove UIP for natural numbers