Library CatSem.RPCF.RPCF_rep_comp
Require Import Coq.Logic.Eqdep.
Require Export CatSem.RPCF.RPCF_rep_hom.
Require Export CatSem.CAT.rmonad_gen_comp.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Transparent Obligations.
Unset Automatic Introduction.
Ltac gendep H := generalize dependent H.
Section rep_comp.
Variables P Q R : PCFPO_rep.
Variable M : PCFPO_rep_Hom P Q.
Variable N : PCFPO_rep_Hom Q R.
Lemma SM_ind_comp T (V : ITYPE T) (W : IPO T) (Z : IPO T)
(f: forall t, V t -> W t) (g: W ---> Z) :
SM_ind f ;; g == SM_ind (fun t z => g t (f t z)).
Proof.
simpl.
auto.
Qed.
Lemma SM_ipo_mor_comp T (V : ITYPE T) (W : ITYPE T)
(f: V ---> W)(Z : IPO T) (g: sm_ipo W ---> Z) :
sm_ipo_mor f ;; g == SM_ind (fun t z => g t (f t z)).
Proof.
simpl.
auto.
Qed.
Lemma eq_eq_rect A (z : A) (P : A -> Type)
(f g : P z) (y : A) (e : z = y):
f = g -> eq_rect z P f y e = eq_rect z P g y e.
Proof.
intros.
subst.
auto.
Qed.
Obligation Tactic := idtac.
Lemma exsimio:
forall u v : Sorts P,
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) (u ~~> v) =
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) u ~~>
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) v.
Proof.
simpl; intros.
destruct (HArrow N (Sorts_map M u) (Sorts_map M v)).
destruct (HArrow M u v).
reflexivity.
Defined.
Lemma exsimio_bool:
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) (Bool P) = Bool R.
Proof.
destruct (HBool N).
destruct (HBool M).
reflexivity.
Qed.
Lemma exsimio_nat:
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) (Nat P) = Nat R.
Proof.
destruct (HNat N).
destruct (HNat M).
reflexivity.
Qed.
Program Instance Rep_comp_struct :
PCFPO_rep_Hom_struct (P:=P) (R:=R)
(Sorts_map := fun t => Sorts_map N (Sorts_map M t))
exsimio
exsimio_bool
exsimio_nat
(RMon_comp M N).
Obligation 12.
Proof. unfold abs_hom';
simpl.
intros u v c y.
assert (HM:=abs_hom (u:=u)(v:=v)
(PCFPO_rep_Hom_struct :=M) ).
assert (HN:=abs_hom (u:=Sorts_map M u)
(v:=Sorts_map M v)
(PCFPO_rep_Hom_struct :=N)
).
simpl in HM ,HN.
simpl in *.
generalize (@eq_sym (Sorts R) (@Sorts_map Q R N (@Sorts_map P Q M (@Arrow P u v)))
(@Arrow R (@Sorts_map Q R N (@Sorts_map P Q M u))
(@Sorts_map Q R N (@Sorts_map P Q M v))) (exsimio u v)).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
intro e.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A ].
simpl in *.
clear Prec Papp tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qrec Qapp tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rrec tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
rewrite HM.
gendep e.
generalize (eq_sym (HMarrow u v)).
rewrite HMarrow.
intros.
rewrite (UIP_refl _ _ e).
simpl.
rewrite HN.
clear e.
gendep e0.
generalize (eq_sym (HNarrow (gM u) (gM v))).
rewrite HNarrow.
intros.
rewrite (UIP_refl _ _ e).
rewrite (UIP_refl _ _ e0).
simpl.
clear HN HM e e0.
assert (H:=rmod_hom_rmkl
(Rabs (gN (gM u)) (gN (gM v)))).
simpl in H.
unfold rlift at 1.
rewrite <- H.
apply f_equal.
fold (rlift HR).
rew (rlift_rkleisli (M:= HR)).
rew (rlift_rlift HR).
assert (H':= gen_rh_rlift TN).
assert (H2 := H'
(retype (fun t : U => gM t) (opt u c))
(opt (gM u) (retype (fun t : U => gM t) c))
(@der_comm _ _ _ _ _ )).
rewrite <- H2.
rew (rlift_rkleisli (M:=HR)).
unfold rlift.
apply (rkl_eq HR).
simpl.
intros t z.
destruct z as [t z];
simpl.
destruct z as [t z];
simpl.
destruct z as [t z | ];
simpl;
auto.
unfold rlift.
simpl.
rew (retakl HR).
Qed.
Obligation 10.
Proof. unfold app_hom';
simpl.
intros u v c y.
assert (HM:=app_hom (u:=u)(v:=v)
(PCFPO_rep_Hom_struct :=M) (c:=c)y).
assert (HN:=app_hom (u:=Sorts_map M u)
(v:=Sorts_map M v)
(PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)).
simpl in HM ,HN.
generalize (exsimio u v) as e.
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
clear HMnat HMbool.
clear HNnat HNbool.
rewrite <- HM.
rewrite <- HN.
simpl.
clear HM.
clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A ].
simpl in *.
clear Prec Pabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qrec Qabs Qrec tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rabs Rrec tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
intro e.
assert (r:=rmod_hom_rmkl (Rapp (gN (gM u)) (gN (gM v)))).
simpl in r.
unfold rlift.
rewrite <- r.
apply f_equal.
simpl.
clear r Rapp Papp Qapp.
destruct y as [y1 y2];
simpl in *.
gendep e.
rewrite <- HNarrow.
rewrite <- HMarrow.
intros.
rewrite (UIP_refl _ _ e).
simpl.
auto.
Qed.
Obligation 9.
Proof. unfold nats_hom';
simpl.
intros m c t.
elim t.
clear t.
assert (HM:=nats_hom m (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=nats_hom m (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (nats_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : Sorts P => Sorts_map N (Sorts_map M t)) exsimio_nat m) as e.
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (nats_hom'_obligation_1 HMbool m) .
intros. clear HM.
generalize HN.
generalize (nats_hom'_obligation_1 HNbool m) .
intros. clear HN.
destruct P as [U Uarrow Unat Ubool PM Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff Pnats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff Qnats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff Rnats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl (Rnats m)).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (Rnats m (retype (fun t : U => gN (gM t)) c)).
intro Rnats1.
destruct Rnats1 as [RNat RNats].
simpl in *.
clear RNats.
gendep RNat.
gendep HN0.
generalize (e1).
gendep HM0.
generalize (e).
generalize (Qnats m (retype (fun t => gM t) c)).
intro Qnats1.
destruct Qnats1 as [QNat QNats].
simpl in *.
clear QNats.
gendep QNat.
generalize (Rnats m (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro Rnats1.
destruct Rnats1 as [RNat RNats].
simpl in *.
clear RNats.
gendep RNat.
destruct e1.
destruct e.
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 8.
Proof. unfold bottom_hom';
simpl.
intros u c t.
elim t.
clear t.
assert (HM:=bottom_hom (PCFPO_rep_Hom_struct :=M)
(c:=c) u tt).
assert (HN:=bottom_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c) (Sorts_map M u) tt).
simpl in HM ,HN.
rewrite HM.
rewrite HN.
unfold rlift;
simpl.
assert (h:=rmod_hom_rmkl
(bottom (PCFPO_rep_struct := R)
(Sorts_map N (Sorts_map M u)))).
simpl in h.
rewrite <- h.
auto.
Qed.
Obligation 7.
Proof. unfold ttt_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=ttt_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=ttt_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (ttt_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => Sorts_map N (Sorts_map M t)) exsimio_bool).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (ttt_hom'_obligation_1 HMnat) .
intros. clear HM.
generalize HN.
generalize (ttt_hom'_obligation_1 HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec Ptttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec Qtttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec Rtttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl Rtttt).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (Rtttt (retype (fun t : U => gN (gM t)) c)).
intro Rtttt1.
destruct Rtttt1 as [Rttt Rttts].
simpl in *.
clear Rttts.
gendep Rttt.
gendep HN0.
generalize (e1).
gendep HM0.
generalize e.
generalize (Qtttt (retype (fun t => gM t) c)).
intro Qtttt1.
destruct Qtttt1 as [Qttt Qttts].
simpl in *.
clear Qttts.
gendep Qttt.
generalize (Rtttt (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro Rtttt1.
destruct Rtttt1 as [Rttt Rttts].
simpl in *.
clear Rttts.
gendep Rttt.
destruct e.
destruct e1.
intros.
rewrite (UIP_refl _ _ e) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 6.
Proof. unfold fff_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=fff_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=fff_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (fff_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio_bool).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (fff_hom'_obligation_1 HMnat) .
intros. clear HM.
generalize HN.
generalize (fff_hom'_obligation_1 HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
Pffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
Qffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
Rffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl Rffff).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (Rffff (retype (fun t : U => gN (gM t)) c)).
intro Rffff1.
destruct Rffff1 as [Rfff Rfffs].
simpl in *.
clear Rfffs.
gendep Rfff.
gendep HN0.
generalize e1.
gendep HM0.
generalize e.
generalize (Qffff (retype (fun t => gM t) c)).
intro Qffff1.
destruct Qffff1 as [Qfff Qfffs].
simpl in *.
clear Qfffs.
gendep Qfff.
generalize (Rffff (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro Rffff1.
destruct Rffff1 as [Rfff Rfffs].
simpl in *.
clear Rfffs.
gendep Rfff.
destruct e.
destruct e1.
intros.
rewrite (UIP_refl _ _ e) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 5.
Proof. unfold Succ_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=Succ_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=Succ_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (Succ_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_nat).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (Succ_hom'_obligation_1 HMarrow HMbool) .
intros. clear HM.
generalize HN.
generalize (Succ_hom'_obligation_1 HNarrow HNbool) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats PSucc Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats QSucc Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats RSucc Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RSucc).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RSucc (retype (fun t : U => gN (gM t)) c)).
intro RSucc1.
destruct RSucc1 as [Rsucc Rsuccs].
simpl in *.
clear Rsuccs.
gendep Rsucc.
gendep HN0.
generalize e1.
gendep HM0.
generalize e.
generalize (QSucc (retype (fun t => gM t) c)).
intro QSucc1.
destruct QSucc1 as [Qsucc Qsuccs].
simpl in *.
clear Qsuccs.
gendep Qsucc.
generalize (RSucc (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RSucc1.
destruct RSucc1 as [Rsucc Rsuccs].
simpl in *.
clear Rsuccs.
gendep Rsucc.
rewrite <- e.
rerew_all.
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rew_all.
rew_all.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 4.
Proof. unfold Zero_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=Zero_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=Zero_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (Zero_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_bool
exsimio_nat).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (Zero_hom'_obligation_1 HMarrow HMbool HMnat) .
intros. clear HM.
generalize HN.
generalize (Zero_hom'_obligation_1 HNarrow HNbool HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred PZero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Pred
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred QZero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Pred
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred RZero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Pred
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RZero).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RZero (retype (fun t : U => gN (gM t)) c)).
intro RZero1.
destruct RZero1 as [Rzero Rzeros].
simpl in *.
clear Rzeros.
gendep Rzero.
gendep HN0.
generalize e1.
gendep HM0.
generalize e.
generalize (QZero (retype (fun t => gM t) c)).
intro QZero1.
destruct QZero1 as [Qzero Qzeros].
simpl in *.
clear Qzeros.
gendep Qzero.
generalize (RZero (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RZero1.
destruct RZero1 as [Rzero Rzeros].
simpl in *.
clear Rzeros.
gendep Rzero.
rerew_all.
rerew_all.
repeat rerew_all.
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 3.
Proof. unfold Pred_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=Pred_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=Pred_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (Pred_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_nat).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (Pred_hom'_obligation_1 HMarrow HMnat) .
intros. clear HM.
generalize HN.
generalize (Pred_hom'_obligation_1 HNarrow HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ PPred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Zero CondN
CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ QPred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ RPred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RPred).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RPred (retype (fun t : U => gN (gM t)) c)).
intro RPred1.
destruct RPred1 as [Rpred Rpreds].
simpl in *.
clear Rpreds.
gendep Rpred.
gendep HN0.
generalize e1 .
gendep HM0.
generalize e.
generalize (QPred (retype (fun t => gM t) c)).
intro QPred1.
destruct QPred1 as [Qpred Qpreds].
simpl in *.
clear Qpreds.
gendep Qpred.
generalize (RPred (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RPred1.
destruct RPred1 as [Rpred Rpreds].
simpl in *.
clear Rpreds.
gendep Rpred.
repeat (rerew_all).
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 2.
Proof. unfold CondN_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=CondN_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=CondN_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (CondN_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_bool
exsimio_nat).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (CondN_hom'_obligation_1 HMarrow HMnat HMbool) .
clear HM.
intros e HM.
generalize HN.
generalize (CondN_hom'_obligation_1 HNarrow HNnat HNbool) .
clear HN.
intros.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero PCondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Pred Zero
CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero QCondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Pred Zero
CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero RCondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Pred
Zero CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RCondN).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RCondN (retype (fun t : U => gN (gM t)) c)).
intro RCondN1.
destruct RCondN1 as [RcondN RcondNs].
simpl in *.
clear RcondNs.
gendep RcondN.
gendep HN.
generalize e1.
gendep HM.
generalize e.
generalize (QCondN (retype (fun t => gM t) c)).
intro QCondN1.
destruct QCondN1 as [QcondN QcondNs].
simpl in *.
clear QcondNs.
gendep QcondN.
generalize (RCondN (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RCondN1.
destruct RCondN1 as [RcondN RcondNs].
simpl in *.
clear RcondNs.
gendep RcondN.
repeat (rerew_all).
intros.
rewrite (UIP_refl _ _ _) in HM.
simpl in HM, HN.
simpl in HN.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM.
rewrite HN.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Next Obligation.
Proof.
unfold CondB_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=CondB_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=CondB_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (CondB_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_bool).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (CondB_hom'_obligation_1 HMarrow HMnat) .
clear HM.
intros e HM.
generalize HN.
generalize (CondB_hom'_obligation_1 HNarrow HNnat) .
clear HN.
intros.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN PCondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Pred Zero CondN bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN QCondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Pred Zero CondN bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN RCondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Pred Zero CondN bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RCondB).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RCondB (retype (fun t : U => gN (gM t)) c)).
intro RCondB1.
destruct RCondB1 as [RcondB RcondBs].
simpl in *.
clear RcondBs.
gendep RcondB.
gendep HN.
generalize e1.
gendep HM.
generalize e.
generalize (QCondB (retype (fun t => gM t) c)).
intro QCondB1.
destruct QCondB1 as [QcondB QcondBs].
simpl in *.
clear QcondBs.
gendep QcondB.
generalize (RCondB (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RCondB1.
destruct RCondB1 as [RcondB RcondBs].
simpl in *.
clear RcondBs.
gendep RcondB.
repeat (rerew_all).
intros.
rewrite (UIP_refl _ _ _) in HM.
simpl in HM.
simpl in HN.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM.
rewrite HN.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 11. Proof. unfold rec_hom';
simpl.
intros t c y.
assert (HM:=rec_hom (t:=t) (PCFPO_rep_Hom_struct :=M) (c:=c)y).
assert (HN:=rec_hom (t:=Sorts_map M t) (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)).
simpl in HM ,HN.
generalize (exsimio t t).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
rewrite HM.
rewrite HN.
clear HM.
clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
intro e.
assert (r:=rmod_hom_rmkl (Rrec (gN (gM t)))).
simpl in r.
unfold rlift at 1.
rewrite <- r.
apply f_equal.
simpl.
generalize (Rrec (gN (gM t))
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c)))
as RRec.
simpl in *.
intro RRec.
destruct RRec as [RRec po_mor_s].
simpl in *.
clear po_mor_s.
generalize RRec.
generalize (Rrec (gN (gM t)) (retype (fun t : U => gN (gM t)) c))
as RRec1.
simpl.
intro RRec1.
destruct RRec1 as [RRec1 po_mor_s].
simpl in *.
clear po_mor_s.
generalize RRec1.
gendep e.
rewrite <- HNarrow.
rewrite <- HMarrow.
simpl.
intros.
rewrite (UIP_refl _ _ e).
simpl.
unfold rlift.
simpl.
assert (H':= rkl_eq HR).
simpl in H'.
apply H'.
simpl.
auto.
Qed.
Definition Rep_comp :
PCFPO_rep_Hom P R := Build_PCFPO_rep_Hom Rep_comp_struct.
End rep_comp.
Require Export CatSem.RPCF.RPCF_rep_hom.
Require Export CatSem.CAT.rmonad_gen_comp.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Transparent Obligations.
Unset Automatic Introduction.
Ltac gendep H := generalize dependent H.
Section rep_comp.
Variables P Q R : PCFPO_rep.
Variable M : PCFPO_rep_Hom P Q.
Variable N : PCFPO_rep_Hom Q R.
Lemma SM_ind_comp T (V : ITYPE T) (W : IPO T) (Z : IPO T)
(f: forall t, V t -> W t) (g: W ---> Z) :
SM_ind f ;; g == SM_ind (fun t z => g t (f t z)).
Proof.
simpl.
auto.
Qed.
Lemma SM_ipo_mor_comp T (V : ITYPE T) (W : ITYPE T)
(f: V ---> W)(Z : IPO T) (g: sm_ipo W ---> Z) :
sm_ipo_mor f ;; g == SM_ind (fun t z => g t (f t z)).
Proof.
simpl.
auto.
Qed.
Lemma eq_eq_rect A (z : A) (P : A -> Type)
(f g : P z) (y : A) (e : z = y):
f = g -> eq_rect z P f y e = eq_rect z P g y e.
Proof.
intros.
subst.
auto.
Qed.
Obligation Tactic := idtac.
Lemma exsimio:
forall u v : Sorts P,
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) (u ~~> v) =
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) u ~~>
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) v.
Proof.
simpl; intros.
destruct (HArrow N (Sorts_map M u) (Sorts_map M v)).
destruct (HArrow M u v).
reflexivity.
Defined.
Lemma exsimio_bool:
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) (Bool P) = Bool R.
Proof.
destruct (HBool N).
destruct (HBool M).
reflexivity.
Qed.
Lemma exsimio_nat:
(fun t : Sorts P => Sorts_map N (Sorts_map M t)) (Nat P) = Nat R.
Proof.
destruct (HNat N).
destruct (HNat M).
reflexivity.
Qed.
Program Instance Rep_comp_struct :
PCFPO_rep_Hom_struct (P:=P) (R:=R)
(Sorts_map := fun t => Sorts_map N (Sorts_map M t))
exsimio
exsimio_bool
exsimio_nat
(RMon_comp M N).
Obligation 12.
Proof. unfold abs_hom';
simpl.
intros u v c y.
assert (HM:=abs_hom (u:=u)(v:=v)
(PCFPO_rep_Hom_struct :=M) ).
assert (HN:=abs_hom (u:=Sorts_map M u)
(v:=Sorts_map M v)
(PCFPO_rep_Hom_struct :=N)
).
simpl in HM ,HN.
simpl in *.
generalize (@eq_sym (Sorts R) (@Sorts_map Q R N (@Sorts_map P Q M (@Arrow P u v)))
(@Arrow R (@Sorts_map Q R N (@Sorts_map P Q M u))
(@Sorts_map Q R N (@Sorts_map P Q M v))) (exsimio u v)).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
intro e.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A ].
simpl in *.
clear Prec Papp tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qrec Qapp tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rrec tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
rewrite HM.
gendep e.
generalize (eq_sym (HMarrow u v)).
rewrite HMarrow.
intros.
rewrite (UIP_refl _ _ e).
simpl.
rewrite HN.
clear e.
gendep e0.
generalize (eq_sym (HNarrow (gM u) (gM v))).
rewrite HNarrow.
intros.
rewrite (UIP_refl _ _ e).
rewrite (UIP_refl _ _ e0).
simpl.
clear HN HM e e0.
assert (H:=rmod_hom_rmkl
(Rabs (gN (gM u)) (gN (gM v)))).
simpl in H.
unfold rlift at 1.
rewrite <- H.
apply f_equal.
fold (rlift HR).
rew (rlift_rkleisli (M:= HR)).
rew (rlift_rlift HR).
assert (H':= gen_rh_rlift TN).
assert (H2 := H'
(retype (fun t : U => gM t) (opt u c))
(opt (gM u) (retype (fun t : U => gM t) c))
(@der_comm _ _ _ _ _ )).
rewrite <- H2.
rew (rlift_rkleisli (M:=HR)).
unfold rlift.
apply (rkl_eq HR).
simpl.
intros t z.
destruct z as [t z];
simpl.
destruct z as [t z];
simpl.
destruct z as [t z | ];
simpl;
auto.
unfold rlift.
simpl.
rew (retakl HR).
Qed.
Obligation 10.
Proof. unfold app_hom';
simpl.
intros u v c y.
assert (HM:=app_hom (u:=u)(v:=v)
(PCFPO_rep_Hom_struct :=M) (c:=c)y).
assert (HN:=app_hom (u:=Sorts_map M u)
(v:=Sorts_map M v)
(PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)).
simpl in HM ,HN.
generalize (exsimio u v) as e.
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
clear HMnat HMbool.
clear HNnat HNbool.
rewrite <- HM.
rewrite <- HN.
simpl.
clear HM.
clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A ].
simpl in *.
clear Prec Pabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qrec Qabs Qrec tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rabs Rrec tttt ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
intro e.
assert (r:=rmod_hom_rmkl (Rapp (gN (gM u)) (gN (gM v)))).
simpl in r.
unfold rlift.
rewrite <- r.
apply f_equal.
simpl.
clear r Rapp Papp Qapp.
destruct y as [y1 y2];
simpl in *.
gendep e.
rewrite <- HNarrow.
rewrite <- HMarrow.
intros.
rewrite (UIP_refl _ _ e).
simpl.
auto.
Qed.
Obligation 9.
Proof. unfold nats_hom';
simpl.
intros m c t.
elim t.
clear t.
assert (HM:=nats_hom m (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=nats_hom m (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (nats_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : Sorts P => Sorts_map N (Sorts_map M t)) exsimio_nat m) as e.
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (nats_hom'_obligation_1 HMbool m) .
intros. clear HM.
generalize HN.
generalize (nats_hom'_obligation_1 HNbool m) .
intros. clear HN.
destruct P as [U Uarrow Unat Ubool PM Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff Pnats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff Qnats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff Rnats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl (Rnats m)).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (Rnats m (retype (fun t : U => gN (gM t)) c)).
intro Rnats1.
destruct Rnats1 as [RNat RNats].
simpl in *.
clear RNats.
gendep RNat.
gendep HN0.
generalize (e1).
gendep HM0.
generalize (e).
generalize (Qnats m (retype (fun t => gM t) c)).
intro Qnats1.
destruct Qnats1 as [QNat QNats].
simpl in *.
clear QNats.
gendep QNat.
generalize (Rnats m (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro Rnats1.
destruct Rnats1 as [RNat RNats].
simpl in *.
clear RNats.
gendep RNat.
destruct e1.
destruct e.
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 8.
Proof. unfold bottom_hom';
simpl.
intros u c t.
elim t.
clear t.
assert (HM:=bottom_hom (PCFPO_rep_Hom_struct :=M)
(c:=c) u tt).
assert (HN:=bottom_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c) (Sorts_map M u) tt).
simpl in HM ,HN.
rewrite HM.
rewrite HN.
unfold rlift;
simpl.
assert (h:=rmod_hom_rmkl
(bottom (PCFPO_rep_struct := R)
(Sorts_map N (Sorts_map M u)))).
simpl in h.
rewrite <- h.
auto.
Qed.
Obligation 7.
Proof. unfold ttt_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=ttt_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=ttt_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (ttt_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => Sorts_map N (Sorts_map M t)) exsimio_bool).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (ttt_hom'_obligation_1 HMnat) .
intros. clear HM.
generalize HN.
generalize (ttt_hom'_obligation_1 HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec Ptttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec Qtttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec Rtttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec ffff nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl Rtttt).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (Rtttt (retype (fun t : U => gN (gM t)) c)).
intro Rtttt1.
destruct Rtttt1 as [Rttt Rttts].
simpl in *.
clear Rttts.
gendep Rttt.
gendep HN0.
generalize (e1).
gendep HM0.
generalize e.
generalize (Qtttt (retype (fun t => gM t) c)).
intro Qtttt1.
destruct Qtttt1 as [Qttt Qttts].
simpl in *.
clear Qttts.
gendep Qttt.
generalize (Rtttt (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro Rtttt1.
destruct Rtttt1 as [Rttt Rttts].
simpl in *.
clear Rttts.
gendep Rttt.
destruct e.
destruct e1.
intros.
rewrite (UIP_refl _ _ e) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 6.
Proof. unfold fff_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=fff_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=fff_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (fff_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio_bool).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (fff_hom'_obligation_1 HMnat) .
intros. clear HM.
generalize HN.
generalize (fff_hom'_obligation_1 HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
Pffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
Qffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
Rffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt nats Succ Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl Rffff).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (Rffff (retype (fun t : U => gN (gM t)) c)).
intro Rffff1.
destruct Rffff1 as [Rfff Rfffs].
simpl in *.
clear Rfffs.
gendep Rfff.
gendep HN0.
generalize e1.
gendep HM0.
generalize e.
generalize (Qffff (retype (fun t => gM t) c)).
intro Qffff1.
destruct Qffff1 as [Qfff Qfffs].
simpl in *.
clear Qfffs.
gendep Qfff.
generalize (Rffff (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro Rffff1.
destruct Rffff1 as [Rfff Rfffs].
simpl in *.
clear Rfffs.
gendep Rfff.
destruct e.
destruct e1.
intros.
rewrite (UIP_refl _ _ e) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 5.
Proof. unfold Succ_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=Succ_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=Succ_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (Succ_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_nat).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (Succ_hom'_obligation_1 HMarrow HMbool) .
intros. clear HM.
generalize HN.
generalize (Succ_hom'_obligation_1 HNarrow HNbool) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats PSucc Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats QSucc Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats RSucc Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Pred Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RSucc).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RSucc (retype (fun t : U => gN (gM t)) c)).
intro RSucc1.
destruct RSucc1 as [Rsucc Rsuccs].
simpl in *.
clear Rsuccs.
gendep Rsucc.
gendep HN0.
generalize e1.
gendep HM0.
generalize e.
generalize (QSucc (retype (fun t => gM t) c)).
intro QSucc1.
destruct QSucc1 as [Qsucc Qsuccs].
simpl in *.
clear Qsuccs.
gendep Qsucc.
generalize (RSucc (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RSucc1.
destruct RSucc1 as [Rsucc Rsuccs].
simpl in *.
clear Rsuccs.
gendep Rsucc.
rewrite <- e.
rerew_all.
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rew_all.
rew_all.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 4.
Proof. unfold Zero_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=Zero_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=Zero_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (Zero_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_bool
exsimio_nat).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (Zero_hom'_obligation_1 HMarrow HMbool HMnat) .
intros. clear HM.
generalize HN.
generalize (Zero_hom'_obligation_1 HNarrow HNbool HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred PZero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Pred
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred QZero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Pred
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred RZero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Pred
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RZero).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RZero (retype (fun t : U => gN (gM t)) c)).
intro RZero1.
destruct RZero1 as [Rzero Rzeros].
simpl in *.
clear Rzeros.
gendep Rzero.
gendep HN0.
generalize e1.
gendep HM0.
generalize e.
generalize (QZero (retype (fun t => gM t) c)).
intro QZero1.
destruct QZero1 as [Qzero Qzeros].
simpl in *.
clear Qzeros.
gendep Qzero.
generalize (RZero (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RZero1.
destruct RZero1 as [Rzero Rzeros].
simpl in *.
clear Rzeros.
gendep Rzero.
rerew_all.
rerew_all.
repeat rerew_all.
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 3.
Proof. unfold Pred_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=Pred_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=Pred_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (Pred_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_nat).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (Pred_hom'_obligation_1 HMarrow HMnat) .
intros. clear HM.
generalize HN.
generalize (Pred_hom'_obligation_1 HNarrow HNnat) .
intros. clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ PPred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Zero CondN
CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ QPred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ RPred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Zero
CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RPred).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RPred (retype (fun t : U => gN (gM t)) c)).
intro RPred1.
destruct RPred1 as [Rpred Rpreds].
simpl in *.
clear Rpreds.
gendep Rpred.
gendep HN0.
generalize e1 .
gendep HM0.
generalize e.
generalize (QPred (retype (fun t => gM t) c)).
intro QPred1.
destruct QPred1 as [Qpred Qpreds].
simpl in *.
clear Qpreds.
gendep Qpred.
generalize (RPred (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RPred1.
destruct RPred1 as [Rpred Rpreds].
simpl in *.
clear Rpreds.
gendep Rpred.
repeat (rerew_all).
intros.
rewrite (UIP_refl _ _ _) in HM0.
simpl in HM0.
rewrite (UIP_refl _ _ _) in HN0.
simpl in HN0.
simpl.
rewrite HM0.
rewrite HN0.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 2.
Proof. unfold CondN_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=CondN_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=CondN_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (CondN_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_bool
exsimio_nat).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (CondN_hom'_obligation_1 HMarrow HMnat HMbool) .
clear HM.
intros e HM.
generalize HN.
generalize (CondN_hom'_obligation_1 HNarrow HNnat HNbool) .
clear HN.
intros.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero PCondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Pred Zero
CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero QCondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Pred Zero
CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero RCondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Pred
Zero CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn
Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RCondN).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RCondN (retype (fun t : U => gN (gM t)) c)).
intro RCondN1.
destruct RCondN1 as [RcondN RcondNs].
simpl in *.
clear RcondNs.
gendep RcondN.
gendep HN.
generalize e1.
gendep HM.
generalize e.
generalize (QCondN (retype (fun t => gM t) c)).
intro QCondN1.
destruct QCondN1 as [QcondN QcondNs].
simpl in *.
clear QcondNs.
gendep QcondN.
generalize (RCondN (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RCondN1.
destruct RCondN1 as [RcondN RcondNs].
simpl in *.
clear RcondNs.
gendep RcondN.
repeat (rerew_all).
intros.
rewrite (UIP_refl _ _ _) in HM.
simpl in HM, HN.
simpl in HN.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM.
rewrite HN.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Next Obligation.
Proof.
unfold CondB_hom';
simpl.
intros c t.
elim t.
clear t.
assert (HM:=CondB_hom (PCFPO_rep_Hom_struct :=M)(c:=c) tt).
assert (HN:=CondB_hom (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)tt).
simpl in HM ,HN.
generalize (CondB_hom'_obligation_1 (P:=P) (R:=R)
(Sorts_map:=fun t : _ P => _ N (_ M t)) exsimio exsimio_bool).
destruct N as [gN HNarrow HNbool HNnat TN TNs].
destruct M as [gM HMarrow HMbool HMnat TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
generalize HM.
generalize (CondB_hom'_obligation_1 HMarrow HMnat) .
clear HM.
intros e HM.
generalize HN.
generalize (CondB_hom'_obligation_1 HNarrow HNnat) .
clear HN.
intros.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN PCondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs Prec tttt ffff nats Succ Pred Zero CondN bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN QCondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs Qrec tttt ffff nats Succ Pred Zero CondN bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN RCondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs Rrec tttt ffff nats Succ Pred Zero CondN bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
assert (HH:=rmod_hom_rmkl RCondB).
simpl in HH.
assert (HH':= HH
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c))
(retype (fun t : U => gN (gM t)) c)).
simpl in HH'.
gendep HH'.
generalize (RCondB (retype (fun t : U => gN (gM t)) c)).
intro RCondB1.
destruct RCondB1 as [RcondB RcondBs].
simpl in *.
clear RcondBs.
gendep RcondB.
gendep HN.
generalize e1.
gendep HM.
generalize e.
generalize (QCondB (retype (fun t => gM t) c)).
intro QCondB1.
destruct QCondB1 as [QcondB QcondBs].
simpl in *.
clear QcondBs.
gendep QcondB.
generalize (RCondB (retype (fun t => gN t)
(retype (fun t => gM t) c))).
intro RCondB1.
destruct RCondB1 as [RcondB RcondBs].
simpl in *.
clear RcondBs.
gendep RcondB.
repeat (rerew_all).
intros.
rewrite (UIP_refl _ _ _) in HM.
simpl in HM.
simpl in HN.
rewrite (UIP_refl _ _ _).
simpl.
rewrite HM.
rewrite HN.
simpl.
unfold rlift.
simpl.
rewrite <- HH'.
auto.
Qed.
Obligation 11. Proof. unfold rec_hom';
simpl.
intros t c y.
assert (HM:=rec_hom (t:=t) (PCFPO_rep_Hom_struct :=M) (c:=c)y).
assert (HN:=rec_hom (t:=Sorts_map M t) (PCFPO_rep_Hom_struct :=N)
(c:=retype(fun t => Sorts_map M t) c)).
simpl in HM ,HN.
generalize (exsimio t t).
destruct N as [gN HNarrow HNnat HNbool TN TNs].
destruct M as [gM HMarrow HMnat HMbool TM TMs].
clear M N.
simpl in *.
clear TNs.
clear TMs.
rewrite HM.
rewrite HN.
clear HM.
clear HN.
destruct P as [U Uarrow PM fP HP Prep].
destruct Q as [U' U'arrow QM fQ HQ Qrep];
destruct R as [U'' U''arrow RM fR HR Rrep];
clear P Q R;
simpl in *.
destruct Prep as [Papp Pabs Prec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Papp Pabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A.
destruct Qrep as [Qapp Qabs Qrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Qapp Qabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
destruct Rrep as [Rapp Rabs Rrec tttt
ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z
Rec_A ].
simpl in *.
clear Rapp Rabs tttt ffff nats Succ Pred Zero CondN CondB bottom
beta_red
CondN_t CondN_f
CondB_t CondB_f Succ_red Zero_t Zero_f Pred_Sn Pred_Z Rec_A.
intro e.
assert (r:=rmod_hom_rmkl (Rrec (gN (gM t)))).
simpl in r.
unfold rlift at 1.
rewrite <- r.
apply f_equal.
simpl.
generalize (Rrec (gN (gM t))
(retype (fun t : U' => gN t) (retype (fun t : U => gM t) c)))
as RRec.
simpl in *.
intro RRec.
destruct RRec as [RRec po_mor_s].
simpl in *.
clear po_mor_s.
generalize RRec.
generalize (Rrec (gN (gM t)) (retype (fun t : U => gN (gM t)) c))
as RRec1.
simpl.
intro RRec1.
destruct RRec1 as [RRec1 po_mor_s].
simpl in *.
clear po_mor_s.
generalize RRec1.
gendep e.
rewrite <- HNarrow.
rewrite <- HMarrow.
simpl.
intros.
rewrite (UIP_refl _ _ e).
simpl.
unfold rlift.
simpl.
assert (H':= rkl_eq HR).
simpl in H'.
apply H'.
simpl.
auto.
Qed.
Definition Rep_comp :
PCFPO_rep_Hom P R := Build_PCFPO_rep_Hom Rep_comp_struct.
End rep_comp.