Library NonUniform

This file shows how big non-uniform parameters can be encoded as an index without changing the universe of the definition.

Lemma trans_refl_l A (x y:A) (e:x =y) : eq_trans eq_refl e = e.

Big universe of the parameter

Definition T2 := Type.

Universe of the inductive definition

Definition T1:T2:=Type.

Module NoPayload.

The parameter type

Parameter P : T2.

The arity of the W-type. To simplify, we did not consider the payload

Parameter B : P -> T1.

The parameter update

Parameter f : ∀ p:P, B p -> P.

Encoding as an index. W is not in T1

Inductive W : P -> T2 :=
| C : ∀ p, (∀ i: B p, W (f p i)) -> W p.

We need functional extensionality

Axiom fext : ∀ (A:Type)(B:A->Type)(f g:∀ x:A, B x),
(∀ x, f x = g x) -> f = g.

Encoding parameters as paths

Type of paths from the initial value of the parameter to subterms

Fixpoint path (p:P) (n:nat) : T1 :=
  match n with
  | 0 => unit
  | S k => {i:B p & path (f p i) k }
  end.

Fixpoint decn p n : path p n -> P :=
  match n return path p n -> P with
  | 0 => fun _ => p
  | S k => fun q => let (i,l') := q in decn (f p i) k l'
  end.

Fixpoint extpath p n : ∀ l:path p n, B(decn p n l) -> path p (S n) :=
  match n return ∀ l:path p n, B(decn p n l) -> path p (S n) with
  | 0 => fun _ i => existT _ i tt
  | S k => fun l =>
      match l return B (decn p (S k) l) -> path p (S (S k)) with
      | existT i' l' => fun i => existT _ i' (extpath _ k l' i)
      end
  end.

The encoded type. p is the initial value of the parameter. (m,l) is the path to the current value of the parameter.

Inductive W2 (p:P) : ∀ n, path p n -> T1 :=
  C2 : ∀ m l, (∀ i:B (decn p m l), W2 p (S m) (extpath _ _ l i)) -> W2 p m l.

Record P' :T2:= mkP' {
  _p : P;
  _m : nat;
  _l : path _p _m
}.

Definition i0 (p:P) : P' := mkP' p 0 tt.

Definition d (p:P') : P := decn (_p p) (_m p) (_l p).
Definition f3 (p:P') (i:B(d p)) : P' := mkP' (_p p) (S (_m p)) (extpath _ _ (_l p) i).
Definition W3 (p:P') : T1 := W2 (_p p) (_m p) (_l p).
Definition C3 (p:P') (g:∀ i:B(d p), W3 (f3 p i)) : W3 p :=
  C2 (_p p) (_m p) (_l p) g.
Definition unC3 (p:P') (w:W3 p) : ∀ i:B(d p), W3 (f3 p i) :=
  match w in W2 _ n l return ∀ i, W3 (mkP' _ _ (extpath _ _ l i)) with
  | C2 m l' g => g
  end.

Definition W3_case (p:P') (Q : W3 p -> Type)
  (h:∀ (g : ∀ i : B(d p), W3 (f3 p i)), Q (C3 p g)) (w:W3 p) : Q w.
Defined.

Definition W3_elim (Q : ∀ p : P', W3 p -> Type)
  (h:∀ p (g : ∀ i : B(d p), W3 (f3 p i)),
     (∀ i:B(d p), Q (f3 p i) (g i)) -> Q p (C3 p g)) : ∀ (p:P') (w:W3 p), Q p w.
Defined.

Lemma eq_ext p p' (i:B(d p')) (e:d p =d p') :
  d(f3 p (eq_rect_r B i e)) = d(f3 p' i).

Lemma eq_ext_refl p (i:B(d p)) :
  eq_ext p p i eq_refl = eq_refl.

Lemma extpath_trans_prf p p' p'' i (e:d p =d p') (e':d p'=d p'') :
  f3 p (eq_rect_r B i (eq_trans e e')) =
  f3 p (eq_rect_r B (eq_rect_r B i e') e).

Lemma tr_ext_trans p p' p'' i (e:d p =d p') (e':d p'=d p'') :
  eq_ext p p'' i (eq_trans e e') =
  eq_trans (f_equal d (extpath_trans_prf p p' p'' i e e'))
    (eq_trans (eq_ext p p' (eq_rect_r B i e') e) (eq_ext p' p'' i e')).
Opaque eq_ext.

Fixpoint tr p (w:W3 p) p' (e:d p =d p'): W3 p' :=
  C3 p' (fun i : B (d p') =>
     tr _ (unC3 p w (eq_rect_r B i e)) (f3 p' i) (eq_ext p p' i e)).

Lemma tr_id : ∀ p w, tr p w p eq_refl = w.
Lemma tr_comm p p0 p' (e:d p = d p') (e':d p0 = d p')
  (w:W3 p) (w':W3 p0) (h:p0 =p):
  w' = eq_rect_r W3 w h ->
  e' = eq_trans (f_equal d h) e ->
  tr _ w _ e = tr _ w' _ e'.

Applying two equality proofs is equivalent to applying the composition of these proofs

Lemma tr_comp p w p' e p'' e' :
tr p' (tr p w p' e) p'' e' = tr p w p'' (eq_trans e e').

Definition W' p : T1 := W3 (i0 p).

The constructor

Definition C' (p:P) (g:∀ i, W' (f p i)) : W' p :=
C3 (i0 p) (fun i : B p => tr (i0(f p i)) (g i) (f3 (i0 p) i) eq_refl).

The projection

Definition unC' p (w : W' p) (i:B p) : W' (f p i) :=
  tr (f3 (i0 p) i) (unC3 (i0 p) w i) (i0 (f p i)) eq_refl.

Lemma W'_surj p (w:W' p) : w = C' _ (unC' p w).

Definition W'_case p (w:W' p) (Q:W' p -> Type)
  (h:∀ g:∀ i:B p,W' (f p i), Q (C' p g)) : Q w.
Defined.

Definition W'_elim0 p (w:W' p) (Q:∀ p, W' p -> Type)
  (h : ∀ p (g:∀ i,W' (f p i)), (∀ i, Q (f p i) (g i)) -> Q p (C' p g)) :
  ∀ p' (e:d(i0 p)=p'), Q p' (tr _ w (i0 p') e).
Defined.

Definition W'_elim p (w:W' p) (Q:∀ p, W' p -> Type)
  (h : ∀ p (g:∀ i,W' (f p i)),
       (∀ i, Q _ (g i)) -> Q _ (C' p g)) : Q p w.
Defined.

Lemma w_eta p g : unC' p (C' p g) = g.

Proving the reduction is correct (non-dep!)

Lemma W'_case_nodep_eqn p Q g h : W'_case p (C' p g) (fun _=>Q) h = h g.

Lemma eqp_f p p' (e:p =p') (i:B p):
  f p i = f p' (eq_rect_r B i (eq_sym e)).

Lemma W'_elim0_nodep_eqn p Q g h p' e :
  W'_elim0 p (C' p g) (fun p _=>Q p) h p' e =
  eq_rect_r Q (h p g (fun i:B p => W'_elim0 (f p i) (g i) (fun p _=>Q p) h (f p i) eq_refl)) (eq_sym e).
Opaque W'_surj.

Lemma W'_elim_nodep_eqn p Q g h :
  W'_elim p (C' p g) (fun _ _=>Q) h =
  h p g (fun i => W'_elim _ (g i) (fun _ _=>Q) h).

Lemma W'_case_eqn p Q g h : W'_case p (C' p g) Q h = h g.

End NoPayload.