Library NonUniform
This file shows how big non-uniform parameters can be encoded
as an index without changing the universe of the definition.
Big universe of the parameter
Universe of the inductive definition
The parameter type
The arity of the W-type. To simplify, we did not
consider the payload
The parameter update
Encoding as an index. W is not in T1
We need functional extensionality
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.
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'.
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).
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).
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.
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.
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.