在 Coq 中，CoInductive "extensionality" 是正确的吗？它具有普遍性吗？
Is CoInductive "extensionality" sound in Coq? Is it generalizable?
我的理解是，典型的等式概念太弱，无法在可能无穷大的余反项上证明许多直觉等式。因此，有必要为所讨论的特定互归类型引入一个互归等式。
例如，我有以下关于无限关系转移序列的余归定义：
Section Paths.
Context {state : Type}.
Variable R : relation state.
CoInductive path (s: state) : Type :=
| step : forall s', R s s' -> path s' -> path s.
CoInductive path_eq : forall {s}, path s -> path s -> Prop :=
| path_eq_intro : forall x y r p p',
path_eq p p' ->
path_eq (step x y r p) (step x y r p').
然后相应地扩展我们的核心平等是非常可取的：
Axiom path_extensionality : forall s (p q: path s),
path_eq p q -> p = q.
虽然这个公理从直觉上讲是有道理的，但这种互归纳外延性原则是否通常被认为是合理的？
另外，我担心我必须为我使用的每个余归纳类型添加一个新的公理。是否有一种通用方法可以为任意余归纳类型引入外延性原则？
While this axiom makes sense intuitively, are such coinductive extensionality principles known to be sound in general?
是的。余归类型和函数类型之间存在同构。余归类型模余归外延性与函数类型同构，从它的索引类型到它的数据类型模函数外延性。因此，例如，Stream A 模 EqSt（来自 Coq.Lists.Streams）同构于 nat -> A 模函数外延性。您的数据类型模 path_extensionality 与 { st : nat -> state | forall n, R (st n) (st (S n)) } 模函数扩展性大致同构。我在这里使用您的数据类型的技巧是将其转换为参数化而不是索引的数据类型；您的数据类型在 Stream state.
上进行了道德参数化
不幸的是，没有办法一次引入所有的外延公理，除非您想放弃余导并转而使用函数（在这种情况下，您可以只使用标准库公理 Coq.Logic.FunctionalExtensionality.functional_extensionality_dep）。但是，您可以结合使用一个较弱的公理和函数扩展性：给定余归类型的较弱公理会说，如果您从余归转到相应的函数然后返回，您会回到开始时的状态。另一种表述方式是，您只能公理化同构的一个方向，而不是两个方向。这在每个互归纳外延公理都暗示相应函数类型的函数外延性的意义上较弱，但这个公理没有。
如果您需要一些代码，这里有一些代码显示了标准库流和您的类型的形式同构（适用于 Coq 8.13）：
Require Import Coq.Lists.Streams.
Require Import Coq.Setoids.Setoid.
Module StreamsExt.
Section __.
Context (A : Type).
Definition t := Stream A.
Definition index := nat.
Definition data := A.
(** inclusion, injection, section, monomorphism *)
(** From a function [nat -> A], we can build a [Stream A] *)
CoFixpoint sect (x : index -> data) : t
:= Streams.Cons (x 0) (sect (fun n => x (S n))).
(* surjection, retraction, epimorphism *)
(** From a [Stream A], we can get the nth element, building a function [nat -> A] *)
Fixpoint retr (x : t) (i : index) : data
:= match i with
| O => Streams.hd x
| S i => retr (Streams.tl x) i
end.
(** Two streams are coextensionally equal, then the corresponding functions are extensionally equal *)
Lemma iff_EqSt_pointwise_eq (s1 s2 : t) : Streams.EqSt s1 s2 <-> forall i, retr s1 i = retr s2 i.
Proof using Type.
split.
{ intros H i; revert s1 s2 H; induction i as [|i IHi]; cbn; intros s1 s2 [H1 H2]; auto. }
{ revert s1 s2; cofix CIH; intros s1 s2 H.
constructor.
{ specialize (H 0); cbn in H. assumption. }
{ specialize (fun i => H (S i)); cbn in H. auto. } }
Qed.
Lemma ext_from_funext
(funext : forall f g : index -> data, (forall x, f x = g x) -> f = g)
(axiom : forall x, sect (retr x) = x)
: forall (s1 s2 : t), EqSt s1 s2 -> s1 = s2.
Proof using Type.
intros s1 s2; rewrite iff_EqSt_pointwise_eq; intro H.
rewrite <- (axiom s1), <- (axiom s2); apply f_equal, funext, H.
Qed.
End __.
End StreamsExt.
Section Paths.
Context {state : Type}.
Variable R : relation state.
CoInductive path (s: state) : Type :=
| step : forall s', R s s' -> path s' -> path s.
CoInductive path_eq : forall {s}, path s -> path s -> Prop :=
| path_eq_intro : forall x y r p p',
path_eq p p' ->
path_eq (step x y r p) (step x y r p').
Definition next_state {s} (p : path s) : state
:= match p with
| @step _ s' _ _ => s'
end.
Definition unstep_rel {s} (p : path s) : R s (next_state p)
:= match p with
| @step _ _ r _ => r
end.
Definition unstep {s} (p : path s) : path (next_state p)
:= match p with
| @step _ _ _ p => p
end.
(* slightly nicer version of path_eq *)
Import EqNotations.
CoInductive path_eq' {s1 s2} (p1 : path s1) (p2 : path s2) (H : s1 = s2) : Prop :=
| path_eq'_intro :
forall (p : next_state p1 = next_state p2),
(rew [fun s => R s _] H in rew p in unstep_rel p1) = unstep_rel p2 ->
path_eq' (unstep p1) (unstep p2) p ->
path_eq' p1 p2 H.
CoFixpoint path_eq'_of_path_eq {s} {p1 p2 : path s}
: path_eq p1 p2 -> path_eq' p1 p2 eq_refl.
Proof using Type.
intro H; unshelve econstructor; destruct H.
{ cbn. reflexivity. }
{ cbn. reflexivity. }
{ cbn. apply path_eq'_of_path_eq, H. }
Qed.
Lemma next_state_eq_of_path_eq' {s1 s2} {p1 : path s1} {p2 : path s2} {H : s1 = s2}
: path_eq' p1 p2 H -> next_state p1 = next_state p2.
Proof using Type.
intro H'; destruct H'; assumption.
Defined.
Lemma rel_eq_of_path_eq' {s1 s2} {p1 : path s1} {p2 : path s2} {H : s1 = s2}
: forall p : path_eq' p1 p2 H, (rew [fun s => R s _] H in rew next_state_eq_of_path_eq' p in unstep_rel p1) = unstep_rel p2.
Proof using Type.
intro H'; destruct H'; cbn in *; assumption.
Defined.
CoFixpoint path_eq_of_path_eq' {s} {p1 p2 : path s}
: path_eq' p1 p2 eq_refl -> path_eq p1 p2.
Proof using Type.
intro H'; destruct p1, p2, H'; cbn in *; subst; cbn in *.
constructor; auto.
Qed.
Lemma iff_path_eq_path_eq'_eq_refl {s} (p1 p2 : path s)
: path_eq p1 p2 <-> path_eq' p1 p2 eq_refl.
Proof using Type.
split; first [ apply path_eq'_of_path_eq | apply path_eq_of_path_eq' ].
Qed.
Lemma iff_path_eq_path_eq' {s1 s2} (p1 : path s1) (p2 : path s2) (H : s1 = s2)
: path_eq (rew H in p1) p2 <-> path_eq' p1 p2 H.
Proof using Type.
subst; apply iff_path_eq_path_eq'_eq_refl.
Qed.
End Paths.
Module PathsExt.
Section __.
Context {state : Type}.
Variable R : relation state.
Definition t := { s : state & path R s }.
Definition fun_type := { st : nat -> state | forall n, R (st n) (st (S n)) }.
Definition mk_fun_type (st : nat -> state) (H : forall n, R (st n) (st (S n))) : fun_type
:= exist _ st H.
(** inclusion, injection, section, monomorphism *)
CoFixpoint sect' (x : fun_type) : path R (proj1_sig x 0)
:= step
R _ _
(proj2_sig x 0)
(sect' (mk_fun_type (fun i => proj1_sig x (S i)) (fun i => proj2_sig x (S i)))).
Definition sect (x : fun_type) : t := existT _ _ (sect' x).
(* surjection, retraction, epimorphism *)
Fixpoint retr_index (x : t) (i : nat) : state
:= match i with
| O => projT1 x
| S i => retr_index (existT _ _ (unstep _ (projT2 x))) i
end.
Fixpoint retr' (x : t) (i : nat) : R (retr_index x i) (retr_index x (S i))
:= match i with
| O => unstep_rel _ (projT2 x)
| S i => retr' (existT _ _ (unstep _ (projT2 x))) i
end.
Definition retr (x : t) : fun_type := mk_fun_type (retr_index x) (retr' x).
Import EqNotations.
(** Two paths are coextensionally equal, then the corresponding functions are extensionally equal *)
Definition t_eq (s1 s2 : t) : Prop
:= { p : projT1 s1 = projT1 s2 | path_eq' _ (projT2 s1) (projT2 s2) p }.
Definition fun_type_eq (s1 s2 : fun_type) : Prop
:= exists p : (forall i, proj1_sig s1 i = proj1_sig s2 i),
forall i, (rew [fun s => R s _] (p i) in rew (p (S i)) in proj2_sig s1 i) = proj2_sig s2 i.
Lemma iff_path_eq_pointwise_eq (s1 s2 : t) : t_eq s1 s2 <-> fun_type_eq (retr s1) (retr s2).
Proof using Type.
split; cbv [t_eq fun_type_eq].
{ intro H; unshelve eexists; intro i; revert s1 s2 H; induction i as [|i IHi]; cbn; intros [s1 s1'] [s2 s2'] [H1 H2];
cbn in *.
{ assumption. }
{ apply IHi; cbn.
unshelve eexists; destruct H2; eassumption. }
{ cbn. destruct H2; assumption. }
{ cbn in *. apply IHi. } }
{ intros [H1 H2].
exists (H1 0).
revert s1 s2 H1 H2; cofix CIH; intros.
unshelve econstructor.
{ exact (H1 1). }
{ exact (H2 O). }
{ apply (CIH _ _ (fun i => H1 (S i)) (fun i => H2 (S i))). } }
Defined.
Lemma ext_from_funext'
(funext_fun_type : forall f g, fun_type_eq f g -> f = g)
(axiom : forall x, sect (retr x) = x)
(funext_fun_type_pr : forall f g p q, f_equal (fun a => proj1_sig a 0) (funext_fun_type f g (ex_intro _ p q)) = p 0)
(axiom_pr1 : forall x, f_equal (@projT1 _ _) (axiom x) = eq_refl)
: forall (p1 p2 : t) (H : t_eq p1 p2), { pf : p1 = p2 | f_equal (@projT1 _ _) pf = proj1_sig H }.
Proof using Type.
intros p1 p2.
intro H; unshelve eexists.
{ apply iff_path_eq_pointwise_eq, funext_fun_type, (f_equal sect) in H.
etransitivity; [ | apply axiom ]; etransitivity; [ symmetry; apply axiom | ].
exact H. }
{ cbv zeta beta.
rewrite !eq_trans_map_distr, <- !eq_sym_map_distr, !axiom_pr1; cbn [eq_sym].
rewrite !eq_trans_refl_l, !eq_trans_refl_r, !f_equal_compose.
cbn [projT1 sect].
cbv [iff_path_eq_pointwise_eq]; cbn.
rewrite funext_fun_type_pr.
cbn.
destruct p1, p2, H; cbn; reflexivity. }
Qed.
Lemma f_equal_projT1_eq_sigT {A P u v p q}
: f_equal (@projT1 _ _) (@eq_sigT A P u v p q) = p.
Proof using Type. destruct u, v; cbn in *; subst; cbn; reflexivity. Qed.
Lemma ext_from_funext''
(funext_nat : forall f g : nat -> state, (forall x, f x = g x) -> f = g)
(funext_rel : forall F (f g : forall n : nat, R (F n) (F (S n))), (forall x, f x = g x) -> f = g)
(axiom : forall x, sect (retr x) = x)
(funext_nat_f_equal : forall f g p x, f_equal (fun f => f x) (funext_nat f g p) = p x)
(axiom_pr1 : forall x, f_equal (@projT1 _ _) (axiom x) = eq_refl)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
intros s p1 p2 H.
apply iff_path_eq_path_eq'_eq_refl in H.
unshelve epose proof (ext_from_funext' _ _ _ _ (existT _ _ _) (existT _ _ _) (exist _ eq_refl H)) as H'; try eassumption; revgoals.
{ destruct H' as [H0 H']; cbn in *.
induction H0 using (@eq_sigT_ind _ _ _ _); cbn [projT1 projT2] in *.
rewrite f_equal_projT1_eq_sigT in H'; subst; cbn in *.
reflexivity. }
all: revgoals.
{ cbv [fun_type_eq].
intros [f1 f2] [g1 g2] [H1 H2]; cbn in *.
apply eq_sig_uncurried; cbn.
exists (funext_nat _ _ H1).
apply funext_rel; intro n.
etransitivity; [ | apply H2 ].
transitivity (rew [fun s => R s _] f_equal (fun f => f _) (funext_nat _ _ H1) in rew [R _] f_equal (fun f => f _) (funext_nat _ _ H1) in f2 n).
{ generalize (funext_nat _ _ H1); intro; subst; reflexivity. }
{ rewrite <- (funext_nat_f_equal _ _ H1 n), <- (funext_nat_f_equal _ _ H1 (S n)); reflexivity. } }
{ intros; cbn.
destruct f, g; cbn in *.
move funext_nat at bottom.
generalize (funext_nat_f_equal _ _ p).
generalize (funext_nat _ _ p).
clear funext_nat funext_nat_f_equal.
intro; subst; cbn in *.
intro funext_nat_f_equal.
destruct funext_rel; cbn; apply funext_nat_f_equal. }
Qed.
(* quoting myself at https://github.com/HoTT/HoTT/issues/757#issue-76140493 *)
Definition good_funext_of_funext {A B}
(funext : forall f g : A -> B, (forall x, f x = g x) -> f = g)
(funext_dep : forall (f : A -> B) (F G : forall x : A, {x0 : B & f x = x0}),
(forall x, F x = G x) -> F = G)
: { funext : forall f g : A -> B, (forall x, f x = g x) -> f = g
| (forall f g p, funext f g (fun x => f_equal (fun f => f x) p) = p)
/\ (forall f g p x, f_equal (fun f => f x) (funext f g p) = p x) }.
Proof using Type.
exists (fun f g p => eq_trans (eq_sym (funext _ _ (fun _ => eq_refl))) (funext f g p)).
split.
{ intros; subst; cbn; apply eq_trans_sym_inv_l. }
{ intros f g p.
pose (fun x => existT _ (g x) (p x)) as p'.
change p with (fun x => projT2 (p' x)).
change g with (fun x => projT1 (p' x)).
clearbody p'; clear p g.
assert (H'' : forall x, existT _ (f x) eq_refl = p' x).
{ intro x.
destruct (p' x) as [? []]; reflexivity. }
intro x.
apply funext_dep in H''; subst p'; cbn.
rewrite eq_trans_sym_inv_l; reflexivity. }
Qed.
Lemma ext_from_funext_specific
(funext_nat : forall f g : nat -> state, (forall x, f x = g x) -> f = g)
(funext_nat_sig : forall (f : nat -> state) (F G : forall x : nat, {x0 : state & f x = x0}),
(forall x, F x = G x) -> F = G)
(funext_rel : forall F (f g : forall n : nat, R (F n) (F (S n))), (forall x, f x = g x) -> f = g)
(axiom : forall x, projT2 (sect (retr x)) = projT2 x)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
unshelve eapply ext_from_funext''.
{ unshelve eapply good_funext_of_funext.
{ exact funext_nat. }
{ exact funext_nat_sig. } }
{ intro x.
unshelve eapply eq_sigT.
{ reflexivity. }
{ apply axiom. } }
{ apply funext_rel. }
{ cbn; intros f g p n.
set (fs := good_funext_of_funext _ _).
destruct fs as [fs [H1 H2]].
apply H2. }
{ cbv beta.
intro; apply f_equal_projT1_eq_sigT. }
Qed.
Lemma ext_from_funext_dep
(funext_dep : forall A B (f g : forall a : A, B a), (forall x, f x = g x) -> f = g)
(axiom : forall x, projT2 (sect (retr x)) = projT2 x)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
apply ext_from_funext_specific; try first [ intros *; apply funext_dep | apply axiom ].
Qed.
Lemma f_equal_id {A x y p} : @f_equal A A id x y p = p.
Proof using Type. destruct p; reflexivity. Qed.
(** A more conceptually separated version of this is at
https://github.com/HoTT/HoTT/blob/master/theories/Metatheory/FunextVarieties.v
*)
Lemma ext_from_funext
(funext : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g)
(axiom : forall x, projT2 (sect (retr x)) = projT2 x)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
apply ext_from_funext_dep; [ | apply axiom ].
intros A B f g H.
pose (existT (fun F : A -> { x : A & { y : B x & f x = y } } => (fun x => projT1 (F x)) = id)
(fun x : A => existT _ x (existT _ (f x) eq_refl))
eq_refl) as F.
pose (existT (fun G : A -> { x : A & { y : B x & f x = y } } => (fun x => projT1 (G x)) = id)
(fun x : A => existT _ x (existT _ (g x) (H x)))
eq_refl) as G.
cut (F = G).
{ intro H'.
change ((rew [fun F => forall x, B (F x)] projT2 F in (fun x => projT1 (projT2 (projT1 F x)))) =
(rew [fun F => forall x, B (F x)] projT2 G in (fun x => projT1 (projT2 (projT1 G x))))).
clearbody F G; subst G; reflexivity. }
{ clearbody F G.
pose (fun F : A -> {x : A & {y : B x & f x = y}} => fun x => projT1 (F x)) as postcomp_projT1.
pose (fun F : A -> A
=> (fun x : A => existT (fun x : A => {y : B x & f x = y}) (F x) (existT _ _ eq_refl))) as inv.
assert (H' : forall F, inv (postcomp_projT1 F) = F).
{ clear -funext.
intro F.
apply funext; intro x.
subst inv postcomp_projT1; cbn.
destruct (F x) as [? [? []]]; cbn; reflexivity. }
simple refine (let H'' : forall F, postcomp_projT1 (inv F) = F := _ in _).
{ reflexivity. }
cut (forall Fid (F : {G : A -> {x : A & {y : B x & f x = y}} & postcomp_projT1 G = Fid}),
F = existT _ (fun x => existT _ _ (existT _ _ eq_refl)) eq_refl).
{ intro contr; etransitivity; [|symmetry]; apply contr. }
{ clear F G.
intros Fid F.
refine (eq_sym (@eq_trans _ _ (existT _ _ (H'' Fid)) _ _ (eq_sym _))).
{ apply eq_sigT_uncurried; subst inv postcomp_projT1; cbn.
exists eq_refl; cbv.
reflexivity. }
{ simple refine (let H''' : forall F, inv (postcomp_projT1 F) = F := fun F => eq_trans (eq_trans (f_equal inv (f_equal postcomp_projT1 (eq_sym (H' F)))) (f_equal inv (H'' _))) (H' F) in
_).
clearbody H''.
apply eq_sigT_uncurried; cbn.
exists (eq_trans (eq_sym (H''' _)) (f_equal inv (projT2 F))).
destruct F as [F ?]; subst.
subst H'''; cbn.
clear -funext H' H''.
clearbody inv postcomp_projT1.
clear -funext H' H''.
match goal with
| [ |- rew ?p in eq_refl = ?H ] => cut (f_equal postcomp_projT1 (eq_sym p) = H); [ generalize p | ]
end.
{ clear.
generalize (H'' (postcomp_projT1 F)).
generalize (inv (postcomp_projT1 F)).
intros; subst; cbn; reflexivity. }
rewrite !eq_sym_involutive, !eq_trans_map_distr.
cut (eq_trans
(f_equal postcomp_projT1 (f_equal inv (H'' (postcomp_projT1 F)))) (f_equal postcomp_projT1 (H' F)) =
eq_trans (f_equal postcomp_projT1 (f_equal inv (f_equal postcomp_projT1 (H' F)))) (H'' (postcomp_projT1 F))).
{ rewrite <- !eq_sym_map_distr.
intro H.
rewrite <- eq_trans_assoc, H, !eq_trans_assoc, eq_trans_sym_inv_l, eq_trans_refl_l.
reflexivity. }
generalize (f_equal postcomp_projT1 (H' F)).
generalize (postcomp_projT1 F).
cut (forall a b (e : postcomp_projT1 (inv a) = b),
eq_trans (f_equal postcomp_projT1 (f_equal inv (H'' a))) e = eq_trans (f_equal postcomp_projT1 (f_equal inv e)) (H'' b)).
{ clear; intros H ??; apply H. }
intros; subst b; cbn.
rewrite eq_trans_refl_l.
rewrite f_equal_compose.
set (F' := fun a => postcomp_projT1 (inv a)).
change (forall F, F' F = F) in H''.
change (f_equal F' (H'' a) = H'' (F' a)).
assert (Hid : F' = id) by (apply funext, H'').
clearbody F'; subst F'.
rewrite f_equal_id; reflexivity. } } }
Qed.
End __.
End PathsExt.
我的理解是，典型的等式概念太弱，无法在可能无穷大的余反项上证明许多直觉等式。因此，有必要为所讨论的特定互归类型引入一个互归等式。
例如，我有以下关于无限关系转移序列的余归定义：
Section Paths.
Context {state : Type}.
Variable R : relation state.
CoInductive path (s: state) : Type :=
| step : forall s', R s s' -> path s' -> path s.
CoInductive path_eq : forall {s}, path s -> path s -> Prop :=
| path_eq_intro : forall x y r p p',
path_eq p p' ->
path_eq (step x y r p) (step x y r p').
然后相应地扩展我们的核心平等是非常可取的：
Axiom path_extensionality : forall s (p q: path s),
path_eq p q -> p = q.
虽然这个公理从直觉上讲是有道理的，但这种互归纳外延性原则是否通常被认为是合理的？
另外，我担心我必须为我使用的每个余归纳类型添加一个新的公理。是否有一种通用方法可以为任意余归纳类型引入外延性原则？
While this axiom makes sense intuitively, are such coinductive extensionality principles known to be sound in general?
是的。余归类型和函数类型之间存在同构。余归类型模余归外延性与函数类型同构，从它的索引类型到它的数据类型模函数外延性。因此，例如，Stream A 模 EqSt（来自 Coq.Lists.Streams）同构于 nat -> A 模函数外延性。您的数据类型模 path_extensionality 与 { st : nat -> state | forall n, R (st n) (st (S n)) } 模函数扩展性大致同构。我在这里使用您的数据类型的技巧是将其转换为参数化而不是索引的数据类型；您的数据类型在 Stream state.
不幸的是，没有办法一次引入所有的外延公理，除非您想放弃余导并转而使用函数（在这种情况下，您可以只使用标准库公理 Coq.Logic.FunctionalExtensionality.functional_extensionality_dep）。但是，您可以结合使用一个较弱的公理和函数扩展性：给定余归类型的较弱公理会说，如果您从余归转到相应的函数然后返回，您会回到开始时的状态。另一种表述方式是，您只能公理化同构的一个方向，而不是两个方向。这在每个互归纳外延公理都暗示相应函数类型的函数外延性的意义上较弱，但这个公理没有。
如果您需要一些代码，这里有一些代码显示了标准库流和您的类型的形式同构（适用于 Coq 8.13）：
Require Import Coq.Lists.Streams.
Require Import Coq.Setoids.Setoid.
Module StreamsExt.
Section __.
Context (A : Type).
Definition t := Stream A.
Definition index := nat.
Definition data := A.
(** inclusion, injection, section, monomorphism *)
(** From a function [nat -> A], we can build a [Stream A] *)
CoFixpoint sect (x : index -> data) : t
:= Streams.Cons (x 0) (sect (fun n => x (S n))).
(* surjection, retraction, epimorphism *)
(** From a [Stream A], we can get the nth element, building a function [nat -> A] *)
Fixpoint retr (x : t) (i : index) : data
:= match i with
| O => Streams.hd x
| S i => retr (Streams.tl x) i
end.
(** Two streams are coextensionally equal, then the corresponding functions are extensionally equal *)
Lemma iff_EqSt_pointwise_eq (s1 s2 : t) : Streams.EqSt s1 s2 <-> forall i, retr s1 i = retr s2 i.
Proof using Type.
split.
{ intros H i; revert s1 s2 H; induction i as [|i IHi]; cbn; intros s1 s2 [H1 H2]; auto. }
{ revert s1 s2; cofix CIH; intros s1 s2 H.
constructor.
{ specialize (H 0); cbn in H. assumption. }
{ specialize (fun i => H (S i)); cbn in H. auto. } }
Qed.
Lemma ext_from_funext
(funext : forall f g : index -> data, (forall x, f x = g x) -> f = g)
(axiom : forall x, sect (retr x) = x)
: forall (s1 s2 : t), EqSt s1 s2 -> s1 = s2.
Proof using Type.
intros s1 s2; rewrite iff_EqSt_pointwise_eq; intro H.
rewrite <- (axiom s1), <- (axiom s2); apply f_equal, funext, H.
Qed.
End __.
End StreamsExt.
Section Paths.
Context {state : Type}.
Variable R : relation state.
CoInductive path (s: state) : Type :=
| step : forall s', R s s' -> path s' -> path s.
CoInductive path_eq : forall {s}, path s -> path s -> Prop :=
| path_eq_intro : forall x y r p p',
path_eq p p' ->
path_eq (step x y r p) (step x y r p').
Definition next_state {s} (p : path s) : state
:= match p with
| @step _ s' _ _ => s'
end.
Definition unstep_rel {s} (p : path s) : R s (next_state p)
:= match p with
| @step _ _ r _ => r
end.
Definition unstep {s} (p : path s) : path (next_state p)
:= match p with
| @step _ _ _ p => p
end.
(* slightly nicer version of path_eq *)
Import EqNotations.
CoInductive path_eq' {s1 s2} (p1 : path s1) (p2 : path s2) (H : s1 = s2) : Prop :=
| path_eq'_intro :
forall (p : next_state p1 = next_state p2),
(rew [fun s => R s _] H in rew p in unstep_rel p1) = unstep_rel p2 ->
path_eq' (unstep p1) (unstep p2) p ->
path_eq' p1 p2 H.
CoFixpoint path_eq'_of_path_eq {s} {p1 p2 : path s}
: path_eq p1 p2 -> path_eq' p1 p2 eq_refl.
Proof using Type.
intro H; unshelve econstructor; destruct H.
{ cbn. reflexivity. }
{ cbn. reflexivity. }
{ cbn. apply path_eq'_of_path_eq, H. }
Qed.
Lemma next_state_eq_of_path_eq' {s1 s2} {p1 : path s1} {p2 : path s2} {H : s1 = s2}
: path_eq' p1 p2 H -> next_state p1 = next_state p2.
Proof using Type.
intro H'; destruct H'; assumption.
Defined.
Lemma rel_eq_of_path_eq' {s1 s2} {p1 : path s1} {p2 : path s2} {H : s1 = s2}
: forall p : path_eq' p1 p2 H, (rew [fun s => R s _] H in rew next_state_eq_of_path_eq' p in unstep_rel p1) = unstep_rel p2.
Proof using Type.
intro H'; destruct H'; cbn in *; assumption.
Defined.
CoFixpoint path_eq_of_path_eq' {s} {p1 p2 : path s}
: path_eq' p1 p2 eq_refl -> path_eq p1 p2.
Proof using Type.
intro H'; destruct p1, p2, H'; cbn in *; subst; cbn in *.
constructor; auto.
Qed.
Lemma iff_path_eq_path_eq'_eq_refl {s} (p1 p2 : path s)
: path_eq p1 p2 <-> path_eq' p1 p2 eq_refl.
Proof using Type.
split; first [ apply path_eq'_of_path_eq | apply path_eq_of_path_eq' ].
Qed.
Lemma iff_path_eq_path_eq' {s1 s2} (p1 : path s1) (p2 : path s2) (H : s1 = s2)
: path_eq (rew H in p1) p2 <-> path_eq' p1 p2 H.
Proof using Type.
subst; apply iff_path_eq_path_eq'_eq_refl.
Qed.
End Paths.
Module PathsExt.
Section __.
Context {state : Type}.
Variable R : relation state.
Definition t := { s : state & path R s }.
Definition fun_type := { st : nat -> state | forall n, R (st n) (st (S n)) }.
Definition mk_fun_type (st : nat -> state) (H : forall n, R (st n) (st (S n))) : fun_type
:= exist _ st H.
(** inclusion, injection, section, monomorphism *)
CoFixpoint sect' (x : fun_type) : path R (proj1_sig x 0)
:= step
R _ _
(proj2_sig x 0)
(sect' (mk_fun_type (fun i => proj1_sig x (S i)) (fun i => proj2_sig x (S i)))).
Definition sect (x : fun_type) : t := existT _ _ (sect' x).
(* surjection, retraction, epimorphism *)
Fixpoint retr_index (x : t) (i : nat) : state
:= match i with
| O => projT1 x
| S i => retr_index (existT _ _ (unstep _ (projT2 x))) i
end.
Fixpoint retr' (x : t) (i : nat) : R (retr_index x i) (retr_index x (S i))
:= match i with
| O => unstep_rel _ (projT2 x)
| S i => retr' (existT _ _ (unstep _ (projT2 x))) i
end.
Definition retr (x : t) : fun_type := mk_fun_type (retr_index x) (retr' x).
Import EqNotations.
(** Two paths are coextensionally equal, then the corresponding functions are extensionally equal *)
Definition t_eq (s1 s2 : t) : Prop
:= { p : projT1 s1 = projT1 s2 | path_eq' _ (projT2 s1) (projT2 s2) p }.
Definition fun_type_eq (s1 s2 : fun_type) : Prop
:= exists p : (forall i, proj1_sig s1 i = proj1_sig s2 i),
forall i, (rew [fun s => R s _] (p i) in rew (p (S i)) in proj2_sig s1 i) = proj2_sig s2 i.
Lemma iff_path_eq_pointwise_eq (s1 s2 : t) : t_eq s1 s2 <-> fun_type_eq (retr s1) (retr s2).
Proof using Type.
split; cbv [t_eq fun_type_eq].
{ intro H; unshelve eexists; intro i; revert s1 s2 H; induction i as [|i IHi]; cbn; intros [s1 s1'] [s2 s2'] [H1 H2];
cbn in *.
{ assumption. }
{ apply IHi; cbn.
unshelve eexists; destruct H2; eassumption. }
{ cbn. destruct H2; assumption. }
{ cbn in *. apply IHi. } }
{ intros [H1 H2].
exists (H1 0).
revert s1 s2 H1 H2; cofix CIH; intros.
unshelve econstructor.
{ exact (H1 1). }
{ exact (H2 O). }
{ apply (CIH _ _ (fun i => H1 (S i)) (fun i => H2 (S i))). } }
Defined.
Lemma ext_from_funext'
(funext_fun_type : forall f g, fun_type_eq f g -> f = g)
(axiom : forall x, sect (retr x) = x)
(funext_fun_type_pr : forall f g p q, f_equal (fun a => proj1_sig a 0) (funext_fun_type f g (ex_intro _ p q)) = p 0)
(axiom_pr1 : forall x, f_equal (@projT1 _ _) (axiom x) = eq_refl)
: forall (p1 p2 : t) (H : t_eq p1 p2), { pf : p1 = p2 | f_equal (@projT1 _ _) pf = proj1_sig H }.
Proof using Type.
intros p1 p2.
intro H; unshelve eexists.
{ apply iff_path_eq_pointwise_eq, funext_fun_type, (f_equal sect) in H.
etransitivity; [ | apply axiom ]; etransitivity; [ symmetry; apply axiom | ].
exact H. }
{ cbv zeta beta.
rewrite !eq_trans_map_distr, <- !eq_sym_map_distr, !axiom_pr1; cbn [eq_sym].
rewrite !eq_trans_refl_l, !eq_trans_refl_r, !f_equal_compose.
cbn [projT1 sect].
cbv [iff_path_eq_pointwise_eq]; cbn.
rewrite funext_fun_type_pr.
cbn.
destruct p1, p2, H; cbn; reflexivity. }
Qed.
Lemma f_equal_projT1_eq_sigT {A P u v p q}
: f_equal (@projT1 _ _) (@eq_sigT A P u v p q) = p.
Proof using Type. destruct u, v; cbn in *; subst; cbn; reflexivity. Qed.
Lemma ext_from_funext''
(funext_nat : forall f g : nat -> state, (forall x, f x = g x) -> f = g)
(funext_rel : forall F (f g : forall n : nat, R (F n) (F (S n))), (forall x, f x = g x) -> f = g)
(axiom : forall x, sect (retr x) = x)
(funext_nat_f_equal : forall f g p x, f_equal (fun f => f x) (funext_nat f g p) = p x)
(axiom_pr1 : forall x, f_equal (@projT1 _ _) (axiom x) = eq_refl)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
intros s p1 p2 H.
apply iff_path_eq_path_eq'_eq_refl in H.
unshelve epose proof (ext_from_funext' _ _ _ _ (existT _ _ _) (existT _ _ _) (exist _ eq_refl H)) as H'; try eassumption; revgoals.
{ destruct H' as [H0 H']; cbn in *.
induction H0 using (@eq_sigT_ind _ _ _ _); cbn [projT1 projT2] in *.
rewrite f_equal_projT1_eq_sigT in H'; subst; cbn in *.
reflexivity. }
all: revgoals.
{ cbv [fun_type_eq].
intros [f1 f2] [g1 g2] [H1 H2]; cbn in *.
apply eq_sig_uncurried; cbn.
exists (funext_nat _ _ H1).
apply funext_rel; intro n.
etransitivity; [ | apply H2 ].
transitivity (rew [fun s => R s _] f_equal (fun f => f _) (funext_nat _ _ H1) in rew [R _] f_equal (fun f => f _) (funext_nat _ _ H1) in f2 n).
{ generalize (funext_nat _ _ H1); intro; subst; reflexivity. }
{ rewrite <- (funext_nat_f_equal _ _ H1 n), <- (funext_nat_f_equal _ _ H1 (S n)); reflexivity. } }
{ intros; cbn.
destruct f, g; cbn in *.
move funext_nat at bottom.
generalize (funext_nat_f_equal _ _ p).
generalize (funext_nat _ _ p).
clear funext_nat funext_nat_f_equal.
intro; subst; cbn in *.
intro funext_nat_f_equal.
destruct funext_rel; cbn; apply funext_nat_f_equal. }
Qed.
(* quoting myself at https://github.com/HoTT/HoTT/issues/757#issue-76140493 *)
Definition good_funext_of_funext {A B}
(funext : forall f g : A -> B, (forall x, f x = g x) -> f = g)
(funext_dep : forall (f : A -> B) (F G : forall x : A, {x0 : B & f x = x0}),
(forall x, F x = G x) -> F = G)
: { funext : forall f g : A -> B, (forall x, f x = g x) -> f = g
| (forall f g p, funext f g (fun x => f_equal (fun f => f x) p) = p)
/\ (forall f g p x, f_equal (fun f => f x) (funext f g p) = p x) }.
Proof using Type.
exists (fun f g p => eq_trans (eq_sym (funext _ _ (fun _ => eq_refl))) (funext f g p)).
split.
{ intros; subst; cbn; apply eq_trans_sym_inv_l. }
{ intros f g p.
pose (fun x => existT _ (g x) (p x)) as p'.
change p with (fun x => projT2 (p' x)).
change g with (fun x => projT1 (p' x)).
clearbody p'; clear p g.
assert (H'' : forall x, existT _ (f x) eq_refl = p' x).
{ intro x.
destruct (p' x) as [? []]; reflexivity. }
intro x.
apply funext_dep in H''; subst p'; cbn.
rewrite eq_trans_sym_inv_l; reflexivity. }
Qed.
Lemma ext_from_funext_specific
(funext_nat : forall f g : nat -> state, (forall x, f x = g x) -> f = g)
(funext_nat_sig : forall (f : nat -> state) (F G : forall x : nat, {x0 : state & f x = x0}),
(forall x, F x = G x) -> F = G)
(funext_rel : forall F (f g : forall n : nat, R (F n) (F (S n))), (forall x, f x = g x) -> f = g)
(axiom : forall x, projT2 (sect (retr x)) = projT2 x)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
unshelve eapply ext_from_funext''.
{ unshelve eapply good_funext_of_funext.
{ exact funext_nat. }
{ exact funext_nat_sig. } }
{ intro x.
unshelve eapply eq_sigT.
{ reflexivity. }
{ apply axiom. } }
{ apply funext_rel. }
{ cbn; intros f g p n.
set (fs := good_funext_of_funext _ _).
destruct fs as [fs [H1 H2]].
apply H2. }
{ cbv beta.
intro; apply f_equal_projT1_eq_sigT. }
Qed.
Lemma ext_from_funext_dep
(funext_dep : forall A B (f g : forall a : A, B a), (forall x, f x = g x) -> f = g)
(axiom : forall x, projT2 (sect (retr x)) = projT2 x)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
apply ext_from_funext_specific; try first [ intros *; apply funext_dep | apply axiom ].
Qed.
Lemma f_equal_id {A x y p} : @f_equal A A id x y p = p.
Proof using Type. destruct p; reflexivity. Qed.
(** A more conceptually separated version of this is at
https://github.com/HoTT/HoTT/blob/master/theories/Metatheory/FunextVarieties.v
*)
Lemma ext_from_funext
(funext : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g)
(axiom : forall x, projT2 (sect (retr x)) = projT2 x)
: forall {s} (p1 p2 : path R s), path_eq R p1 p2 -> p1 = p2.
Proof using Type.
apply ext_from_funext_dep; [ | apply axiom ].
intros A B f g H.
pose (existT (fun F : A -> { x : A & { y : B x & f x = y } } => (fun x => projT1 (F x)) = id)
(fun x : A => existT _ x (existT _ (f x) eq_refl))
eq_refl) as F.
pose (existT (fun G : A -> { x : A & { y : B x & f x = y } } => (fun x => projT1 (G x)) = id)
(fun x : A => existT _ x (existT _ (g x) (H x)))
eq_refl) as G.
cut (F = G).
{ intro H'.
change ((rew [fun F => forall x, B (F x)] projT2 F in (fun x => projT1 (projT2 (projT1 F x)))) =
(rew [fun F => forall x, B (F x)] projT2 G in (fun x => projT1 (projT2 (projT1 G x))))).
clearbody F G; subst G; reflexivity. }
{ clearbody F G.
pose (fun F : A -> {x : A & {y : B x & f x = y}} => fun x => projT1 (F x)) as postcomp_projT1.
pose (fun F : A -> A
=> (fun x : A => existT (fun x : A => {y : B x & f x = y}) (F x) (existT _ _ eq_refl))) as inv.
assert (H' : forall F, inv (postcomp_projT1 F) = F).
{ clear -funext.
intro F.
apply funext; intro x.
subst inv postcomp_projT1; cbn.
destruct (F x) as [? [? []]]; cbn; reflexivity. }
simple refine (let H'' : forall F, postcomp_projT1 (inv F) = F := _ in _).
{ reflexivity. }
cut (forall Fid (F : {G : A -> {x : A & {y : B x & f x = y}} & postcomp_projT1 G = Fid}),
F = existT _ (fun x => existT _ _ (existT _ _ eq_refl)) eq_refl).
{ intro contr; etransitivity; [|symmetry]; apply contr. }
{ clear F G.
intros Fid F.
refine (eq_sym (@eq_trans _ _ (existT _ _ (H'' Fid)) _ _ (eq_sym _))).
{ apply eq_sigT_uncurried; subst inv postcomp_projT1; cbn.
exists eq_refl; cbv.
reflexivity. }
{ simple refine (let H''' : forall F, inv (postcomp_projT1 F) = F := fun F => eq_trans (eq_trans (f_equal inv (f_equal postcomp_projT1 (eq_sym (H' F)))) (f_equal inv (H'' _))) (H' F) in
_).
clearbody H''.
apply eq_sigT_uncurried; cbn.
exists (eq_trans (eq_sym (H''' _)) (f_equal inv (projT2 F))).
destruct F as [F ?]; subst.
subst H'''; cbn.
clear -funext H' H''.
clearbody inv postcomp_projT1.
clear -funext H' H''.
match goal with
| [ |- rew ?p in eq_refl = ?H ] => cut (f_equal postcomp_projT1 (eq_sym p) = H); [ generalize p | ]
end.
{ clear.
generalize (H'' (postcomp_projT1 F)).
generalize (inv (postcomp_projT1 F)).
intros; subst; cbn; reflexivity. }
rewrite !eq_sym_involutive, !eq_trans_map_distr.
cut (eq_trans
(f_equal postcomp_projT1 (f_equal inv (H'' (postcomp_projT1 F)))) (f_equal postcomp_projT1 (H' F)) =
eq_trans (f_equal postcomp_projT1 (f_equal inv (f_equal postcomp_projT1 (H' F)))) (H'' (postcomp_projT1 F))).
{ rewrite <- !eq_sym_map_distr.
intro H.
rewrite <- eq_trans_assoc, H, !eq_trans_assoc, eq_trans_sym_inv_l, eq_trans_refl_l.
reflexivity. }
generalize (f_equal postcomp_projT1 (H' F)).
generalize (postcomp_projT1 F).
cut (forall a b (e : postcomp_projT1 (inv a) = b),
eq_trans (f_equal postcomp_projT1 (f_equal inv (H'' a))) e = eq_trans (f_equal postcomp_projT1 (f_equal inv e)) (H'' b)).
{ clear; intros H ??; apply H. }
intros; subst b; cbn.
rewrite eq_trans_refl_l.
rewrite f_equal_compose.
set (F' := fun a => postcomp_projT1 (inv a)).
change (forall F, F' F = F) in H''.
change (f_equal F' (H'' a) = H'' (F' a)).
assert (Hid : F' = id) by (apply funext, H'').
clearbody F'; subst F'.
rewrite f_equal_id; reflexivity. } } }
Qed.
End __.
End PathsExt.