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.
revert Q h; unfold d,f3,C3,W3; simpl.
unfold W3 in w.
pattern (_m p), (_l p), w.
case w.
intros n' l' g Q h.
apply (h g).
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.
fix W3e 2.
intros p w; revert p w.
destruct p as (p,n,l); unfold W3; simpl.
intros w; case w.
intros n' l' g.
apply h.
intros i.
apply W3e.
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).
revert i e; destruct p' as (p',n',l').
revert p' l'; induction n'; simpl.
unfold f3 at 2; simpl.
unfold d at 1 3; simpl.
intros p' ? i e.
unfold d; simpl.
revert i; destruct e.
unfold eq_rect_r; simpl.
destruct p as (p,n,l); revert p l; induction n; simpl; intros.
reflexivity.
destruct l.
apply IHn.
destruct l'.
apply IHn'.
Defined.
Lemma eq_ext_refl p (i:B(d p)) :
eq_ext p p i eq_refl = eq_refl.
revert i; destruct p as (p,n,l); revert p l; induction n; simpl; intros; auto.
destruct l; intros.
apply IHn.
Qed.
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).
revert i; destruct e'; reflexivity.
Defined.
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')).
destruct p'' as (p'',n'',l''); revert p'' l'' e' i.
induction n'';[|destruct l'']; intros.
unfold d at 2 in e'; unfold d in i; simpl in e',i.
destruct e'.
unfold eq_rect_r; simpl eq_rect; simpl extpath_trans_prf.
rewrite trans_refl_l.
destruct p' as (p',n',l'); simpl in l''.
revert p' l' e i; induction n'; [|destruct l']; intros.
unfold d at 2 in e; unfold d in i; simpl in e,i.
destruct e.
destruct p as (p,n,l); simpl in l'.
revert p l i; induction n; [|destruct l]; intros.
simpl; reflexivity.
apply IHn.
apply IHn'.
apply IHn''.
Qed.
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.
apply W3_elim; simpl; intros; trivial.
apply f_equal; apply fext; intros i.
unfold eq_rect_r; simpl.
rewrite eq_ext_refl; auto.
Qed.
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'.
intros.
destruct p as (p,n,l); simpl _p in *; simpl _m in *; simpl _l in *.
subst.
apply f_equal.
symmetry; apply trans_refl_l.
Qed.
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.
revert Q h; unfold d,f3,C3,W3; simpl.
unfold W3 in w.
pattern (_m p), (_l p), w.
case w.
intros n' l' g Q h.
apply (h g).
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.
fix W3e 2.
intros p w; revert p w.
destruct p as (p,n,l); unfold W3; simpl.
intros w; case w.
intros n' l' g.
apply h.
intros i.
apply W3e.
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).
revert i e; destruct p' as (p',n',l').
revert p' l'; induction n'; simpl.
unfold f3 at 2; simpl.
unfold d at 1 3; simpl.
intros p' ? i e.
unfold d; simpl.
revert i; destruct e.
unfold eq_rect_r; simpl.
destruct p as (p,n,l); revert p l; induction n; simpl; intros.
reflexivity.
destruct l.
apply IHn.
destruct l'.
apply IHn'.
Defined.
Lemma eq_ext_refl p (i:B(d p)) :
eq_ext p p i eq_refl = eq_refl.
revert i; destruct p as (p,n,l); revert p l; induction n; simpl; intros; auto.
destruct l; intros.
apply IHn.
Qed.
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).
revert i; destruct e'; reflexivity.
Defined.
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')).
destruct p'' as (p'',n'',l''); revert p'' l'' e' i.
induction n'';[|destruct l'']; intros.
unfold d at 2 in e'; unfold d in i; simpl in e',i.
destruct e'.
unfold eq_rect_r; simpl eq_rect; simpl extpath_trans_prf.
rewrite trans_refl_l.
destruct p' as (p',n',l'); simpl in l''.
revert p' l' e i; induction n'; [|destruct l']; intros.
unfold d at 2 in e; unfold d in i; simpl in e,i.
destruct e.
destruct p as (p,n,l); simpl in l'.
revert p l i; induction n; [|destruct l]; intros.
simpl; reflexivity.
apply IHn.
apply IHn'.
apply IHn''.
Qed.
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.
apply W3_elim; simpl; intros; trivial.
apply f_equal; apply fext; intros i.
unfold eq_rect_r; simpl.
rewrite eq_ext_refl; auto.
Qed.
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'.
intros.
destruct p as (p,n,l); simpl _p in *; simpl _m in *; simpl _l in *.
subst.
apply f_equal.
symmetry; apply trans_refl_l.
Qed.
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').
revert p' e p'' e'; pattern p, w; apply W3_elim; simpl; intros.
apply f_equal.
apply fext; intro i.
rewrite H.
clear H.
apply tr_comm with (h:=extpath_trans_prf _ _ _ i e e').
unfold extpath_trans_prf.
destruct e'; reflexivity.
apply tr_ext_trans.
Qed.
Definition W' p : T1 := W3 (i0 p).
tr p' (tr p w p' e) p'' e' = tr p w p'' (eq_trans e e').
revert p' e p'' e'; pattern p, w; apply W3_elim; simpl; intros.
apply f_equal.
apply fext; intro i.
rewrite H.
clear H.
apply tr_comm with (h:=extpath_trans_prf _ _ _ i e e').
unfold extpath_trans_prf.
destruct e'; reflexivity.
apply tr_ext_trans.
Qed.
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).
pattern w; apply W3_case; simpl; intros.
unfold C', unC'; simpl.
apply f_equal; apply fext; intros i.
rewrite tr_comp.
simpl eq_trans.
symmetry; apply tr_id.
Defined.
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.
rewrite (W'_surj _ w).
apply h.
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).
unfold W' in w.
pattern (i0 p), w.
apply W3_elim; clear p w; intros.
rewrite W'_surj.
apply h.
intros.
unfold unC';simpl.
rewrite tr_comp; simpl.
apply X.
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.
rewrite <- (tr_id _ w).
apply W'_elim0; trivial.
Defined.
Lemma w_eta p g : unC' p (C' p g) = g.
unfold unC', C'; simpl.
apply fext; intros i.
rewrite tr_comp.
simpl eq_trans.
rewrite (tr_id _ (g i)); trivial.
Qed.
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).
pattern w; apply W3_case; simpl; intros.
unfold C', unC'; simpl.
apply f_equal; apply fext; intros i.
rewrite tr_comp.
simpl eq_trans.
symmetry; apply tr_id.
Defined.
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.
rewrite (W'_surj _ w).
apply h.
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).
unfold W' in w.
pattern (i0 p), w.
apply W3_elim; clear p w; intros.
rewrite W'_surj.
apply h.
intros.
unfold unC';simpl.
rewrite tr_comp; simpl.
apply X.
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.
rewrite <- (tr_id _ w).
apply W'_elim0; trivial.
Defined.
Lemma w_eta p g : unC' p (C' p g) = g.
unfold unC', C'; simpl.
apply fext; intros i.
rewrite tr_comp.
simpl eq_trans.
rewrite (tr_id _ (g i)); trivial.
Qed.
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.
unfold W'_case.
simpl in h.
unfold eq_rect_r, eq_rect.
generalize (eq_sym (W'_surj p (C' p g))).
rewrite (w_eta p g).
intro e.
change ((fun w (e':C' p g=w) =>
match e' in (@eq _ _ y) return Q with
| eq_refl => h g
end = h g) (C' p g) e).
case e; reflexivity.
Qed.
Lemma eqp_f p p' (e:p=p') (i:B p):
f p i = f p' (eq_rect_r B i (eq_sym e)).
destruct e; reflexivity.
Defined.
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).
unfold W'_elim0.
Opaque W'_surj.
simpl W3_elim.
unfold unC'.
simpl unC3.
change (mkP' p 0 tt) with (i0 p).
unfold d in e; simpl in e.
destruct e; simpl.
unfold eq_rect_r; simpl.
match goal with |- eq_rect _ _ _ _ ?h =_ => set (e':=h) end.
destruct e'.
simpl.
f_equal.
apply fext; intros i.
rewrite tr_comp.
rewrite tr_comp.
rewrite eq_ext_refl.
simpl.
rewrite tr_id.
trivial.
apply fext; intros i.
match goal with |- eq_rect _ _ _ _ ?h =_ => destruct h end.
simpl.
Admitted.
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).
unfold W'_elim at 1.
simpl in h.
unfold eq_rect_r, eq_rect.
generalize (eq_sym (W'_surj p (C' p g))).
rewrite (w_eta p g).
intro e.
Admitted.
Lemma W'_case_eqn p Q g h : W'_case p (C' p g) Q h = h g.
unfold W'_case.
unfold eq_rect_r, eq_rect.
generalize (eq_sym (W'_surj p (C' p g))).
rewrite (w_eta p g).
intro e.
generalize (h g).
Admitted.
End NoPayload.
unfold W'_case.
simpl in h.
unfold eq_rect_r, eq_rect.
generalize (eq_sym (W'_surj p (C' p g))).
rewrite (w_eta p g).
intro e.
change ((fun w (e':C' p g=w) =>
match e' in (@eq _ _ y) return Q with
| eq_refl => h g
end = h g) (C' p g) e).
case e; reflexivity.
Qed.
Lemma eqp_f p p' (e:p=p') (i:B p):
f p i = f p' (eq_rect_r B i (eq_sym e)).
destruct e; reflexivity.
Defined.
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).
unfold W'_elim0.
Opaque W'_surj.
simpl W3_elim.
unfold unC'.
simpl unC3.
change (mkP' p 0 tt) with (i0 p).
unfold d in e; simpl in e.
destruct e; simpl.
unfold eq_rect_r; simpl.
match goal with |- eq_rect _ _ _ _ ?h =_ => set (e':=h) end.
destruct e'.
simpl.
f_equal.
apply fext; intros i.
rewrite tr_comp.
rewrite tr_comp.
rewrite eq_ext_refl.
simpl.
rewrite tr_id.
trivial.
apply fext; intros i.
match goal with |- eq_rect _ _ _ _ ?h =_ => destruct h end.
simpl.
Admitted.
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).
unfold W'_elim at 1.
simpl in h.
unfold eq_rect_r, eq_rect.
generalize (eq_sym (W'_surj p (C' p g))).
rewrite (w_eta p g).
intro e.
Admitted.
Lemma W'_case_eqn p Q g h : W'_case p (C' p g) Q h = h g.
unfold W'_case.
unfold eq_rect_r, eq_rect.
generalize (eq_sym (W'_surj p (C' p g))).
rewrite (w_eta p g).
intro e.
generalize (h g).
Admitted.
End NoPayload.