text:
From Coq Require Import Decidable Bool ZArith Reals Lia.
From Flocq Require Import Core Bracket Digits.
Require Import Gappa_definitions.
Require Import Gappa_dyadic.
Require Import Gappa_round_def.
Require Import Gappa_round_aux.

Definition shr_aux (p : rnd_record) : rnd_record :=
 let s := rnd_r p || rnd_s p in
 match (rnd_m p) with
 | N0 => rnd_record_mk N0 false s
 | Npos m1 =>
  match m1 with
  | xH => rnd_record_mk N0 true s
  | xO m2 => rnd_record_mk (Npos m2) false s
  | xI m2 => rnd_record_mk (Npos m2) true s
  end
 end.

Definition shr (m : positive) (d : positive) :=
 iter_pos shr_aux d (rnd_record_mk (Npos m) false false).

Definition round_pos (rdir : rnd_record -> bool)
  (rexp : Z -> Z) (m : positive) (e : Z) :=
 let e' := rexp (e + Zpos (digits m))%Z in
 match (e' - e)%Z with
 | Zpos d =>
   let r := shr m d in
   ((if rdir r then N.succ (rnd_m r) else rnd_m r), e')
 | _ => (Npos m, e)
 end.

Definition round (rdirs : round_dir) (rexp : Z -> Z) (f : float2) :=
 match (Fnum f) with
 | Z0 => Float2 Z0 Z0
 | Zpos p =>
   match (round_pos (rpos rdirs) rexp p (Fexp f)) with
   | (N0, _) => Float2 Z0 Z0
   | (Npos q, e) => Float2 (Zpos q) e
   end
 | Zneg p =>
   match (round_pos (rneg rdirs) rexp p (Fexp f)) with
   | (N0, _) => Float2 Z0 Z0
   | (Npos q, e) => Float2 (Zneg q) e
   end
 end.

Definition tofloat p := match p with
 | (m,e) => Float2 (Z_of_N m) e
 end.

Section ZrndG.

Section rndG.

Lemma bracket_aux :
  forall x,
  (IZR (Zfloor x) <= x < IZR (Zfloor x) + 1)%R.
Proof.
split.
apply Zfloor_lb.
apply Zfloor_ub.
Qed.

Variable rdir : rnd_record -> bool.
Variable good_rdir : good_rdir rdir.

Definition hrndG_aux mx x :=
  match inbetween_loc (IZR mx) (IZR mx + 1) x with
  | loc_Exact => (false, false)
  | loc_Inexact Lt => (false, true)
  | loc_Inexact Eq => (true, false)
  | loc_Inexact Gt => (true, true)
  end.

Definition hrndG x :=
  let mx := Zfloor x in
  let m := ZtoN mx in
  let l := inbetween_loc (IZR mx) (IZR mx + 1) x in
  let r := let (r, s) := hrndG_aux mx x in rnd_record_mk m r s in
  if rdir r then Zceil x else Zfloor x.

Lemma hrndG_DN :
  forall x,
  rdir (rnd_record_mk (ZtoN (Zfloor x)) true true) = false ->
  hrndG x = Zfloor x.
Proof.
intros x Hx1.
destruct (good_rdir (ZtoN (Zfloor x))) as (Hx2, (Hx3, Hx4)).
rewrite Hx1 in Hx4.
destruct Hx4 as [Hx4|Hx4] ; try easy.
rewrite Hx4 in Hx3.
destruct Hx3 as [Hx3|Hx3] ; try easy.
unfold hrndG.
destruct (hrndG_aux (Zfloor x) x) as ([|],[|]) ;
  now rewrite ?Hx1, ?Hx2, ?Hx3, ?Hx4.
Qed.

Lemma hrndG_UP :
  forall x,
  rdir (rnd_record_mk (ZtoN (Zfloor x)) false true) = true ->
  hrndG x = Zceil x.
Proof.
intros x Hx1.
destruct (good_rdir (ZtoN (Zfloor x))) as (Hx2, (Hx3, Hx4)).
rewrite Hx1 in Hx3.
destruct Hx3 as [Hx3|Hx3] ; try easy.
rewrite Hx3 in Hx4.
destruct Hx4 as [Hx4|Hx4] ; try easy.
unfold hrndG, hrndG_aux.
destruct (inbetween_spec _ _ x (bracket_aux _)) as [H|l H1 H2].
rewrite Hx2.
rewrite H at 2.
now rewrite Zceil_IZR.
now case l ; rewrite ?Hx1, ?Hx3, ?Hx4.
Qed.

Lemma hrndG_N :
  forall x,
  ( forall b, rdir (rnd_record_mk (ZtoN (Zfloor x)) b true) = b ) ->
  hrndG x = Znearest (fun x => rdir (rnd_record_mk (ZtoN x) true false)) x.
Proof with auto with typeclass_instances.
intros x Hx1.
destruct (good_rdir (ZtoN (Zfloor x))) as (Hx2, _).
unfold hrndG, hrndG_aux.
destruct (inbetween_spec _ _ x (bracket_aux _)) as [Hx4|l Hx4 Hx5].
rewrite Hx2.
rewrite Hx4 at 2.
rewrite Zrnd_IZR...
unfold Znearest.
rewrite Rcompare_floor_ceil_middle with (1 := Rlt_not_eq _ _ (proj1 Hx4)).
rewrite Rcompare_middle.
rewrite Zceil_floor_neq with (1 := Rlt_not_eq _ _ (proj1 Hx4)).
rewrite plus_IZR.
rewrite Hx5.
now case l ; rewrite ?Hx1, ?Hx2.
Qed.

Instance valid_rnd_hG : Valid_rnd hrndG.
Proof with auto with typeclass_instances.
split.
(* monotone *)
intros x y Hxy.
destruct (Z.eq_dec (Zfloor x) (Zfloor y)) as [H|H].
(* *)
case_eq (rdir (rnd_record_mk (ZtoN (Zfloor x)) true true)) ; intros Hb1.
case_eq (rdir (rnd_record_mk (ZtoN (Zfloor x)) false true)) ; intros Hb2.
(* . *)
rewrite hrndG_UP with (1 := Hb2).
rewrite H in Hb2.
rewrite hrndG_UP with (1 := Hb2).
now apply Zceil_le.
(* . *)
assert (Hb3: forall b, rdir (rnd_record_mk (ZtoN (Zfloor x)) b true) = b).
now intros [|].
rewrite hrndG_N with (1 := Hb3).
rewrite H in Hb3.
rewrite hrndG_N with (1 := Hb3).
apply Zrnd_le...
(* . *)
rewrite hrndG_DN with (1 := Hb1).
rewrite H in Hb1.
rewrite hrndG_DN with (1 := Hb1).
now apply Zfloor_le.
(* *)
apply Z.le_trans with (Zceil x).
unfold hrndG.
case rdir.
apply Z.le_refl.
apply le_IZR.
exact (Rle_trans _ _ _ (Zfloor_lb x) (Zceil_ub x)).
apply Z.le_trans with (Zfloor y).
apply Z.le_trans with (Zfloor x + 1)%Z.
apply Zceil_glb.
rewrite plus_IZR.
apply Rlt_le.
apply Zfloor_ub.
generalize (Zfloor_le x y Hxy).
lia.
unfold hrndG.
case rdir.
apply le_IZR.
exact (Rle_trans _ _ _ (Zfloor_lb y) (Zceil_ub y)).
apply Z.le_refl.
(* Z2R *)
intros n.
unfold hrndG.
case rdir.
apply Zceil_IZR.
apply Zfloor_IZR.
Qed.

Lemma hrndG_pos :
  forall x, (0 <= x)%R -> (0 <= hrndG x)%Z.
Proof with auto with typeclass_instances.
intros x Hx.
rewrite <- (Zrnd_IZR hrndG 0).
apply Zrnd_le...
Qed.

Lemma shr_conversion :
  forall m d,
  shr m d = let (r, s) := hrndG_aux (Zfloor (IZR (Zpos m) * bpow radix2 (- Zpos d))) (IZR (Zpos m) * bpow radix2 (- Zpos d)) in
    rnd_record_mk (ZtoN (Zfloor (IZR (Zpos m) * bpow radix2 (- Zpos d)))) r s.
Proof.
intros m d.
unfold shr.
rewrite iter_pos_nat.
rewrite (Zpos_eq_Z_of_nat_o_nat_of_P d).
induction (nat_of_P d).
(* *)
simpl.
rewrite Rmult_1_r.
rewrite Zfloor_IZR.
unfold hrndG_aux, inbetween_loc.
now rewrite Rcompare_Eq.
(* *)
rewrite iter_nat_S.
rewrite IHn. clear IHn.
unfold hrndG_aux.
set (ms := (IZR (Zpos m) * bpow radix2 (- Z_of_nat (S n)))%R).
replace (IZR (Zpos m) * bpow radix2 (- Z_of_nat n))%R with (ms * 2)%R.
assert (H0: (0 <= Zfloor ms)%Z).
apply Zfloor_lub.
unfold ms.
apply Rmult_le_pos.
now apply IZR_le.
apply bpow_ge_0.
clearbody ms. clear -H0.
destruct (inbetween_spec _ _ ms (bracket_aux _)) as [H|l H1 H2].
(* . *)
replace (Zfloor (ms * 2)) with (Zfloor ms * 2)%Z.
unfold inbetween_loc.
rewrite mult_IZR.
rewrite Rcompare_Eq.
destruct (Zfloor ms) as [|p|p] ; try easy.
now rewrite Zmult_comm.
now rewrite <- H.
rewrite H at 2.
rewrite <- mult_IZR.
now rewrite Zfloor_IZR.
(* . *)
unfold inbetween_loc.
assert (H3: Rcompare (ms * 2) (IZR (Zfloor ms) * 2 + 1) = l).
rewrite <- (Rcompare_mult_r 2) in H2.
now replace (IZR (Zfloor ms) * 2 + 1)%R with ((IZR (Zfloor ms) + (IZR (Zfloor ms) + 1)) / 2 * 2)%R by field.
now apply IZR_lt.
clear H2. rewrite <- H3. clear H3.
case Rcompare_spec ; intros H4.
elim Rlt_not_le with (1 := H4).
apply Zfloor_lb.
(* .. *)
unfold shr_aux. simpl.
rewrite H4.
rewrite <- mult_IZR, <- plus_IZR.
rewrite Rcompare_IZR.
rewrite <- H4.
replace (Zfloor (ms * 2)) with (1 + 2 * Zfloor ms)%Z.
rewrite Zcompare_Eq.
clear -H0.
destruct (Zfloor ms) as [|p|p] ; [easy|easy|].
now elim H0.
now rewrite Zmult_comm, Zplus_comm.
clear -H1 H4.
assert (Zfloor ms * 2 < Zfloor (ms * 2) < (Zfloor ms + 1) * 2)%Z.
split ; apply lt_IZR ; rewrite <- H4 ; rewrite mult_IZR ; apply Rmult_lt_compat_r.
now apply IZR_lt.
apply H1.
now apply IZR_lt.
now rewrite plus_IZR.
lia.
(* .. *)
set (rs := match Rcompare (ms * 2) ((IZR (Zfloor (ms * 2)) + (IZR (Zfloor (ms * 2)) + 1)) / 2) with
  Eq => (true, false) | Lt => (false, true) | Gt => (true, true) end).
rewrite (surjective_pairing rs).
unfold shr_aux. simpl.
replace (fst rs || snd rs) with true.
clear rs.
case Rcompare_spec ; intros H2.
(* ... *)
replace (Zfloor (ms * 2)) with (2 * Zfloor ms)%Z.
now case (Zfloor ms).
apply sym_eq.
rewrite Zmult_comm.
apply Zfloor_imp.
rewrite plus_IZR, mult_IZR.
refine (conj _ H2).
apply Rmult_le_compat_r.
now apply IZR_le.
apply Zfloor_lb.
(* ... *)
elim Rlt_not_le with (1 := H4).
rewrite H2.
rewrite <- mult_IZR, <- plus_IZR.
rewrite Zfloor_IZR.
apply Rle_refl.
(* ... *)
replace (Zfloor (ms * 2)) with (1 + 2 * Zfloor ms)%Z.
revert H0.
case (Zfloor ms) ; [easy|easy|].
intros p H. now elim H.
apply sym_eq.
apply Zfloor_imp.
rewrite plus_IZR, mult_IZR.
split.
rewrite Rplus_comm, Rmult_comm.
now apply Rlt_le.
rewrite 2!plus_IZR, mult_IZR.
simpl.
replace (1 + 2 * IZR (Zfloor ms) + 1)%R with ((IZR (Zfloor ms) + 1) * 2)%R by ring.
apply Rmult_lt_compat_r.
now apply IZR_lt.
apply H1.
(* ... *)
unfold rs.
now case Rcompare.
unfold ms.
rewrite Rmult_assoc.
change 2%R with (bpow radix2 1).
rewrite <- bpow_plus.
apply (f_equal (fun e => _ * bpow radix2 e)%R).
rewrite inj_S.
unfold Z.succ.
ring.
Qed.

Lemma Z_of_N_ZtoN :
  forall n, (0 <= n)%Z -> Z_of_N (ZtoN n) = n.
Proof.
intros [|p|p] H ; [easy|easy|].
now elim H.
Qed.

Theorem hrndG_conversion :
  forall rexp m e,
  float2R (tofloat (round_pos rdir rexp m e)) =
    Generic_fmt.round radix2 rexp hrndG (F2R (Float radix2 (Zpos m) e)).
Proof with auto with typeclass_instances.
intros rexp m e.
assert (He: cexp radix2 rexp (F2R (Float radix2 (Zpos m) e)) = rexp (e + Zpos (digits m))%Z).
rewrite digits2_digits.
rewrite Zdigits_mag. 2: easy.
unfold cexp.
rewrite mag_F2R. 2: easy.
now rewrite Zplus_comm.
unfold round_pos.
case_eq (rexp (e + Zpos (digits m)) - e)%Z.
(* *)
intros H.
apply sym_eq.
apply round_generic...
apply generic_format_F2R.
intros _ ; simpl.
rewrite He.
rewrite Zminus_eq with (1 := H).
apply Z.le_refl.
(* *)
intros p H.
unfold Generic_fmt.round, scaled_mantissa.
rewrite He.
unfold F2R, float2R. simpl.
rewrite Rmult_assoc, <- bpow_plus.
assert (rexp (e + Zpos (digits m)) = e + Zpos p)%Z.
lia.
rewrite H0.
ring_simplify (e + -(e + Zpos p))%Z.
apply (f_equal (fun m => IZR m * _)%R).
unfold hrndG.
rewrite (shr_conversion m p).
simpl.
set (rs := hrndG_aux (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p))) (IZR (Zpos m) * / IZR (Zpower_pos 2 p))).
rewrite (surjective_pairing rs).
simpl.
assert (H1: rdir (rnd_record_mk (ZtoN (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p)))) (fst rs) (snd rs)) = true ->
  (IZR (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p))) <> IZR (Zpos m) * / IZR (Zpower_pos 2 p))%R).
unfold rs, hrndG_aux.
destruct (inbetween_spec _ _ (IZR (Zpos m) * / IZR (Zpower_pos 2 p)) (bracket_aux _)) as [H1|l H1 H2].
simpl.
intros H2 _.
destruct (good_rdir (ZtoN (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p))))) as (H3, _).
now rewrite H2 in H3.
intros _.
now apply Rlt_not_eq.
revert H1.
case rdir.
intros H1.
rewrite Znat.Z_of_N_succ.
rewrite Z_of_N_ZtoN.
apply sym_eq.
apply Zceil_floor_neq.
now apply H1.
apply Zfloor_lub.
now apply (F2R_ge_0 radix2 (Float radix2 (Zpos m) (- (Zpos p)))).
intros _.
rewrite Z_of_N_ZtoN.
apply refl_equal.
apply Zfloor_lub.
now apply (F2R_ge_0 radix2 (Float radix2 (Zpos m) (- (Zpos p)))).
(* *)
intros p H.
apply sym_eq.
apply round_generic...
apply generic_format_F2R.
intros _ ; simpl.
rewrite He.
generalize (Zlt_neg_0 p).
lia.
Qed.

End rndG.

Variable rdir : round_dir.

Definition rndG x :=
  match Rcompare x 0 with
  | Gt => hrndG (rpos rdir) x
  | Lt => Z.opp (hrndG (rneg rdir) (-x))
  | _ => Z0
  end.

Instance valid_rnd_G : Valid_rnd rndG.
Proof.
split.
(* monotone *)
intros x y Hxy.
unfold rndG.
destruct (Rcompare_spec x 0) as [Hx|Hx|Hx].
(* *)
destruct (Rcompare_spec y 0) as [Hy|Hy|Hy].
(* . *)
apply Zopp_le_cancel.
rewrite 2!Z.opp_involutive.
apply Zrnd_le.
apply valid_rnd_hG.
apply rneg_good.
now apply Ropp_le_contravar.
(* . *)
apply Zopp_le_cancel.
rewrite Z.opp_involutive.
apply hrndG_pos.
apply rneg_good.
rewrite <- Ropp_0.
apply Ropp_le_contravar.
now apply Rlt_le.
(* . *)
apply Z.le_trans with Z0.
apply Zopp_le_cancel.
rewrite Z.opp_involutive.
apply hrndG_pos.
apply rneg_good.
rewrite <- Ropp_0.
apply Ropp_le_contravar.
now apply Rlt_le.
apply hrndG_pos.
apply rpos_good.
now apply Rlt_le.
(* *)
destruct (Rcompare_spec y 0) as [Hy|Hy|Hy].
elim Rle_not_lt with (1 := Hxy).
now rewrite Hx.
apply Z.le_refl.
apply hrndG_pos.
apply rpos_good.
now apply Rlt_le.
(* *)
rewrite Rcompare_Gt.
apply Zrnd_le.
apply valid_rnd_hG.
apply rpos_good.
exact Hxy.
now apply Rlt_le_trans with x.
(* Z2R *)
intros n.
unfold rndG.
rewrite Rcompare_IZR.
rewrite <- opp_IZR.
rewrite 2!Zrnd_IZR.
rewrite Z.opp_involutive.
now case n.
apply valid_rnd_hG.
apply rpos_good.
apply valid_rnd_hG.
apply rneg_good.
Qed.

Lemma rndG_conversion_aux :
  forall rexp f,
  float2R (round rdir rexp f) = Generic_fmt.round radix2 rexp rndG (float2R f).
Proof with auto with typeclass_instances.
intros rexp (m, e).
unfold float2R. simpl.
destruct m as [|m|m].
rewrite 2!F2R_0, round_0...
(* *)
unfold round. simpl.
generalize (hrndG_conversion (rpos rdir) (rpos_good _) rexp m e).
unfold Generic_fmt.round, rndG. simpl.
rewrite Rcompare_Gt.
intros H.
rewrite <- H.
case round_pos.
intros [|n] z ; simpl.
unfold float2R.
now rewrite 2!F2R_0.
apply refl_equal.
unfold scaled_mantissa.
apply Rmult_lt_0_compat.
now apply F2R_gt_0.
apply bpow_gt_0.
(* *)
unfold round. simpl.
change (Zneg m) with (- Zpos m)%Z.
rewrite F2R_Zopp.
generalize (hrndG_conversion (rneg rdir) (rneg_good _) rexp m e).
unfold Generic_fmt.round, rndG. simpl.
rewrite Rcompare_Lt.
rewrite cexp_opp.
rewrite scaled_mantissa_opp.
rewrite Ropp_involutive.
rewrite F2R_Zopp.
intros H.
rewrite <- H.
case round_pos.
intros [|n] z ; simpl.
unfold float2R.
rewrite 2!F2R_0.
now rewrite Ropp_0.
now rewrite <- Fopp2_correct.
rewrite scaled_mantissa_opp.
apply Ropp_lt_gt_0_contravar.
unfold scaled_mantissa.
apply Rmult_lt_0_compat.
now apply F2R_gt_0.
apply bpow_gt_0.
Qed.

End ZrndG.

Existing Instance valid_rnd_G.

Record rndG_prop := {
  rndG_g : round_dir;
  rndG_f : R -> Z;
  rndG_eq : forall x, rndG rndG_g x = rndG_f x
}.

Theorem rndG_conversion :
  forall rdir rexp f,
  float2R (round (rndG_g rdir) rexp f) = Generic_fmt.round radix2 rexp (rndG_f rdir) (float2R f).
Proof.
intros (rf, rg, req) rexp f.
simpl.
rewrite rndG_conversion_aux.
now apply round_ext.
Qed.

Instance valid_rnd_Gf : forall rdir, Valid_rnd (rndG_f rdir).
Proof with auto with typeclass_instances.
split.
intros x y H.
rewrite <- 2!rndG_eq.
apply Zrnd_le...
intros n.
rewrite <- rndG_eq.
apply Zrnd_IZR...
Qed.

Lemma roundDN_eq :
  forall x,
  rndG roundDN x = Zfloor x.
Proof.
intros x.
simpl.
unfold rndG.
case Rcompare_spec ; intros H.
rewrite hrndG_UP.
unfold Zceil.
rewrite Ropp_involutive.
apply Z.opp_involutive.
apply roundDN.
apply refl_equal.
rewrite H.
apply sym_eq.
apply Zfloor_IZR.
rewrite hrndG_DN ; try easy.
apply roundDN.
Qed.

Canonical Structure roundDN_cs := Build_rndG_prop _ _ roundDN_eq.

Lemma roundUP_eq :
  forall x,
  rndG roundUP x = Zceil x.
Proof.
intros x.
simpl.
unfold rndG.
case Rcompare_spec ; intros H.
rewrite hrndG_DN ; try easy.
apply roundUP.
rewrite H.
apply sym_eq.
apply Zceil_IZR.
rewrite hrndG_UP ; try easy.
apply roundUP.
Qed.

Canonical Structure roundUP_cs := Build_rndG_prop _ _ roundUP_eq.

Lemma roundZR_eq :
  forall x,
  rndG roundZR x = Ztrunc x.
Proof.
intros x.
simpl.
unfold rndG, Ztrunc.
destruct (Rlt_bool_spec x 0) as [Hx|[Hx|Hx]].
rewrite Rcompare_Lt with (1 := Hx).
rewrite hrndG_DN ; try easy.
apply roundZR.
rewrite Rcompare_Gt with (1 := Hx).
rewrite hrndG_DN ; try easy.
apply roundZR.
rewrite <- Hx.
rewrite Rcompare_Eq with (1 := refl_equal _).
apply sym_eq.
apply Zfloor_IZR.
Qed.

Canonical Structure roundZR_cs := Build_rndG_prop _ _ roundZR_eq.

Lemma roundN_eq :
  forall r f,
  ( forall m, (0 <= m)%Z -> forall b c, rneg r (rnd_record_mk (ZtoN m) b c) = andb b (orb c (negb (f (- (m + 1))%Z))) ) ->
  ( forall m, (0 <= m)%Z -> forall b c, rpos r (rnd_record_mk (ZtoN m) b c) = andb b (orb c (f m)) ) ->
  forall x,
  rndG r x = Znearest f x.
Proof with auto with typeclass_instances.
intros r f Hn Hp x.
simpl.
destruct (Req_dec (IZR (Zfloor x)) x) as [H1|H1].
rewrite <- H1.
rewrite 2!Zrnd_IZR...
unfold rndG.
case Rcompare_spec ; intros H2.
(* *)
rewrite hrndG_N. 2: apply rneg_good.
rewrite Znearest_opp, Z.opp_involutive.
unfold Znearest.
case Rcompare ; trivial.
rewrite Hn.
simpl.
replace (- (- (Zfloor x + 1) + 1))%Z with (Zfloor x) by ring.
now rewrite negb_involutive.
cut (Zfloor x < 0)%Z. lia.
apply lt_IZR.
apply Rle_lt_trans with (2 := H2).
apply Zfloor_lb.
intros b.
rewrite Hn.
apply andb_true_r.
apply Zfloor_lub.
apply Rlt_le.
now apply Ropp_0_gt_lt_contravar.
(* *)
rewrite H2.
apply sym_eq.
apply Zrnd_IZR...
(* *)
rewrite hrndG_N. 2: apply rpos_good.
unfold Znearest.
case Rcompare ; trivial.
rewrite Hp.
apply refl_equal.
apply Zfloor_lub.
now apply Rlt_le.
intros b.
rewrite Hp.
apply andb_true_r.
apply Zfloor_lub.
now apply Rlt_le.
Qed.

Lemma roundNE_eq :
  forall x,
  rndG roundNE x = rndNE x.
Proof.
apply roundN_eq ;
  intros m Hm r s ;
  unfold roundNE, GrndNE ; simpl ;
  apply (f_equal (fun v => r && (s || negb v))).
rewrite Z.even_opp, Z.even_add.
now destruct m as [|[m|m|]|].
now destruct m as [|[m|m|]|].
Qed.

Canonical Structure roundNE_cs := Build_rndG_prop _ _ roundNE_eq.

Lemma roundNA_eq :
  forall x,
  rndG roundNA x = rndNA x.
Proof.
apply roundN_eq ;
  intros m Hm r s ; simpl.
rewrite Zle_bool_false.
now rewrite orb_comm, andb_comm.
lia.
rewrite Zle_bool_true with (1 := Hm).
now rewrite orb_comm, andb_comm.
Qed.

Canonical Structure roundNA_cs := Build_rndG_prop _ _ roundNA_eq.

author: ejgallego

repo: gappa-coq

save_path: github-repos/coq/ejgallego-gappa-coq


text:
From iris_time Require Import Base.
From iris.base_logic Require Import invariants.
From iris.algebra Require Import lib.gmap_view.
From iris.proofmode Require Import coq_tactics.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Reduction Tactics.
From iris_time Require Export Simulation.
Import uPred.

Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
Implicit Type m n : nat.
Implicit Type φ ψ : val → Prop.
Implicit Type Σ : gFunctors.

(*
 * Abstract interface of time credits
 *)

(* Ideally, this would be represented as a record (or a typeclass), but it has
 * to be an Iris proposition (iProp Σ) and not a Coq proposition (Prop). *)
Definition TC_interface `{!irisGS heap_lang Σ, Tick}
  (TC : nat → iProp Σ)
: iProp Σ := (
    ⌜∀ n, Timeless (TC n)⌝
  ∗ (|==> TC 0%nat)
  ∗ ⌜∀ m n, TC (m + n)%nat ≡ (TC m ∗ TC n)⌝
  ∗ (∀ v, {{{ TC 1%nat }}} tick v {{{ RET v ; True }}})
)%I.

(*
 * Prerequisites on the global monoid Σ
 *)

Class timeCreditHeapPreG Σ := {
  timeCreditHeapPreG_heapPreG :> heapGpreS Σ ;
  timeCreditHeapPreG_inG :> inG Σ (authR natUR) ;
}.

Class timeCreditHeapG Σ := {
  timeCreditHeapG_heapG :> heapGS Σ ;
  timeCreditHeapG_inG :> inG Σ (authR natUR) ;
  timeCreditHeapG_loc :> TickCounter ;
  timeCreditHeapG_name : gname ;
}.

Local Notation γ := timeCreditHeapG_name.
Local Notation ℓ := tick_counter.

(*
 * Implementation and specification of `TC` and `tick`
 *)

(* This code is irrelevant for tick_spec but has to be unsafe for proving
 * the safety theorem: *)
Definition fail : val :=
  λ: <>, #() #().

Global Instance credits_tick {_:TickCounter} : Tick :=
  generic_tick fail.

Section TickSpec.

  Context `{timeCreditHeapG Σ}.

  Definition TC (n : nat) : iProp Σ :=
    own γ (◯nat n).

  (* Note: we can avoid the update modality by redefining TC like so:
         Definition TC' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TC n. *)
  Lemma zero_TC :
    ⊢ |==> TC 0.
  Proof. apply own_unit. Qed.
  Lemma TC_plus m n :
    TC (m + n) ≡ (TC m ∗ TC n)%I.
  Proof. by rewrite /TC auth_frag_op own_op. Qed.
  Lemma TC_succ n :
    TC (S n) ≡ (TC 1%nat ∗ TC n)%I.
  Proof. by rewrite (eq_refl : S n = 1 + n)%nat TC_plus. Qed.
  Lemma TC_weaken (n₁ n₂ : nat) :
    (n₂ ≤ n₁)%nat →
    TC n₁ -∗ TC n₂.
  Proof. apply own_auth_nat_weaken. Qed.

  Lemma TC_timeless n :
    Timeless (TC n).
  Proof. exact _. Qed.

  (* We give higher priorities to the (+) instances so that the (S n)
     instances are not chosen when m is a constant. *)
  Global Instance into_sep_TC_plus m n : IntoSep (TC (m + n)) (TC m) (TC n) | 0.
  Proof. by rewrite /IntoSep TC_plus. Qed.
  Global Instance from_sep_TC_plus m n : FromSep (TC (m + n)) (TC m) (TC n) | 0.
  Proof. by rewrite /FromSep TC_plus. Qed.
  Global Instance into_sep_TC_succ n : IntoSep (TC (S n)) (TC 1) (TC n) | 100.
  Proof. by rewrite /IntoSep TC_succ. Qed.
  Global Instance from_sep_TC_succ n : FromSep (TC (S n)) (TC 1) (TC n) | 100.
  Proof. by rewrite /FromSep [TC (S n)] TC_succ. Qed.

  Definition timeCreditN := nroot .@ "timeCredit".

  Definition TC_invariant : iProp Σ :=
    inv timeCreditN (∃ (m:nat), ℓ ↦ #m ∗ own γ (●nat m))%I.

  Theorem tick_spec s E (v : val) :
    ↑timeCreditN ⊆ E →
    TC_invariant -∗
    {{{ ▷ TC 1 }}} tick v @ s ; E {{{ RET v ; True }}}.
  Proof.
    intros ?. iIntros "#Inv" (Ψ) "!# Hγ◯ HΨ".
    iLöb as "IH".
    wp_lam.
    (* open the invariant, in order to read the value n of location ℓ: *)
    wp_bind (! _)%E ;
    iInv timeCreditN as (n) ">(Hℓ & Hγ●)" "InvClose".
    wp_load.
    (* deduce that n ≥ 1, because we hold a time credit: *)
    iDestruct (own_auth_nat_le with "Hγ● Hγ◯") as %I.
    (* close the invariant: *)
    iMod ("InvClose" with "[ Hℓ Hγ● ]") as "_" ; [ by auto with iFrame | iModIntro ].
    wp_let.
    (* test whether n ≤ 0: *)
    wp_op ; destruct (bool_decide (n ≤ 0)) eqn:Im ; wp_if.
    (* — if n ≤ 0 then this is absurd, because we hold a time credit: *)
    - apply Is_true_eq_left, bool_decide_spec in Im.
      exfalso ; lia.
    (* — otherwise: *)
    - clear Im.
      wp_op.
      (* open the invariant again, in order to perform CAS on location ℓ: *)
      wp_bind (CAS _ _ _)%E ;
      iInv timeCreditN as (n') ">(Hℓ & Hγ●)" "InvClose".
      (* test whether the value ℓ is still k, by comparing n with n': *)
      destruct (nat_eq_dec n n') as [ <- | Hneq ].
      (* — if it holds, then CAS succeeds and ℓ is decremented: *)
      + wp_cas_suc.
        (* reform the invariant with n−1 instead of n: *)
        replace (Z.of_nat n - 1) with (Z.of_nat (n - 1)%nat) by lia.
        iMod (auth_nat_update_decr _ _ _ 1 with "Hγ● Hγ◯") as "[Hγ● Hγ◯]" ; first done.
        (* close the invariant: *)
        iMod ("InvClose" with "[ Hℓ Hγ● ]") as "_" ; [ by auto with iFrame | iModIntro ].
        (* finish: *)
        wp_if. by iApply "HΨ".
      (* — otherwise, CAS fails and ℓ is unchanged: *)
      + wp_cas_fail ; first (injection ; lia).
        (* close the invariant as is: *)
        iMod ("InvClose" with "[ Hℓ Hγ● ]") as "_" ; [ by auto with iFrame | iModIntro ] ; clear dependent n.
        wp_if.
        (* conclude using the induction hypothesis: *)
        iApply ("IH" with "Hγ◯ HΨ").
  Qed.

  Theorem tick_spec_simple v :
    TC_invariant -∗
    {{{ TC 1 }}} tick v {{{ RET v ; True }}}.
  Proof.
    iIntros "#Hinv" (Ψ) "!# HTC HΨ".
    by iApply (tick_spec with "Hinv [HTC//] HΨ").
  Qed.

  Lemma TC_implementation : TC_invariant -∗ TC_interface TC.
  Proof.
    iIntros "#Hinv". iSplit ; last iSplit ; last iSplit.
    - iPureIntro. by apply TC_timeless.
    - by iApply zero_TC.
    - iPureIntro. by apply TC_plus.
    - iIntros (v). by iApply (tick_spec_simple with "Hinv").
  Qed.

End TickSpec.

(*
 * Operational semantics of `tick`
 *)

Section Tick_lemmas.

  Context {Hloc : TickCounter}.

  (* Semantics in the “successful” case. *)

  Lemma exec_tick_success n v σ :
    prim_exec  (tick v) (<[ℓ := #(S n)]> σ)  v (<[ℓ := #n]> σ)  [].
  Proof. by apply exec_tick_success. Qed.

  (* Semantics in the “failing” case. *)

  Lemma not_safe_tick v σ :
    ¬ safe (tick v) (<[ℓ := #0]> σ).
  Proof.
    assert (prim_exec  (tick v) (<[ℓ := #0]> σ)  (#() #()) (<[ℓ := #0]> σ)  []) as Hexec.
    {
      unlock tick credits_tick generic_tick fail.
      eapply prim_exec_cons_nofork.
      { by prim_step. }
      simpl. eapply prim_exec_cons_nofork.
      { prim_step. apply lookup_insert. }
      simpl. eapply prim_exec_cons_nofork.
      { prim_step. }
      simpl. eapply prim_exec_cons_nofork.
      { by prim_step. }
      simpl. eapply prim_exec_cons_nofork.
      { by prim_step. }
      simpl. eapply prim_exec_cons_nofork.
      { by prim_step. }
      simpl. eapply prim_exec_cons_nofork.
      { by prim_step. }
      simpl. apply prim_exec_nil.
    }
    assert (¬ safe (#() #()) (<[ℓ := #0]> σ)) as Hnotsafe.
    {
      apply stuck_not_safe, head_stuck_stuck, ectxi_language_sub_redexes_are_values.
      - split ; first done. inversion 1.
      - intros [] ; try discriminate 1 ; inversion 1 ; by eauto.
    }
    intros Hsafe. eapply Hnotsafe, safe_exec_nofork, prim_exec_exec ; eassumption.
  Qed.

End Tick_lemmas.

(*
 * Simulation
 *)

Section Simulation.

  Context {Hloc : TickCounter}.

  (* Simulation in the “successful” case. *)

  Definition simulation_exec_success := simulation_exec_success fail.
  Definition simulation_exec_success' := simulation_exec_success' fail.

  (* Simulation in the “failing” case. *)

  Local Ltac not_safe_tick :=
    lazymatch goal with
    | |- ¬ safe ?e _ =>
        reshape_expr false e ltac:(fun K e' =>
          apply not_safe_fill' with K e' ; first reflexivity ;
          eapply not_safe_tick
        )
    end ;
    done.

  Lemma simulation_head_step_failure e1 σ1 κ e2 σ2 efs :
    head_step e1 σ1 κ e2 σ2 efs →
    ¬ safe «e1» S«σ1, 0».
  Proof.
    destruct 1 as
      [(* RecS *) f x e σ
      | | | | | | | | | | | |
      | (* ForkS *) e1 σ
      | | | | | | ] ;
    simpl_trans ;
    try not_safe_tick.
    (* RecS f x e σ : *)
    - eapply not_safe_prim_step; last prim_step.
      eapply not_safe_tick.
    (* ForkS e σ : *)
    - eapply not_safe_prim_step ; last prim_step.
      eapply not_safe_tick.
  Qed.

  Lemma simulation_prim_step_failure e1 σ1 κ e2 σ2 efs :
    prim_step e1 σ1 κ e2 σ2 efs →
    ¬ safe «e1» S«σ1, 0».
  Proof.
    intros [ K e1' e2' -> -> H ].
    rewrite translation_fill.
    by eapply not_safe_fill, simulation_head_step_failure.
  Qed.

  Lemma simulation_step_failure t1 σ1 κ t2 σ2 :
    step (t1, σ1) κ (t2, σ2) →
    ∃ e1, e1 ∈ t1 ∧
    ¬ safe «e1» S«σ1, 0».
  Proof.
    intros [e1 σ1_ e2 σ2_ efs t t' E1 E2 Hstep] ;
    injection E1 as -> <- ; injection E2 as -> <-.
    exists e1 ; split ; first set_solver.
    by eapply simulation_prim_step_failure.
  Qed.

  Local Lemma simulation_exec_failure_now n t1 σ1 t2 σ2 :
    relations.nsteps erased_step (S n) (t1, σ1) (t2, σ2) →
    ∃ e1, e1 ∈ t1 ∧
    ¬ safe «e1» S«σ1, 0».
  Proof.
    make_eq (S n) as Sn En.
    make_eq (t1, σ1) as config1 E1.
    destruct 1 as [ ? | ? ? [] ? [? ?] _ ], E1.
    - discriminate En.
    - by eapply simulation_step_failure.
  Qed.

  Lemma simulation_exec_failure m n e1 σ1 t2 σ2 :
    σ2 !! ℓ = None →
    relations.nsteps erased_step (m + S n) ([e1], σ1) (t2, σ2) →
    ¬ safe «e1» S«σ1, m».
  Proof.
    intros Hℓ Hnsteps.
    assert (
      ∃ t3 σ3,
        rtc erased_step (T«[e1]», S«σ1, m») (T«t3», S«σ3, 0») ∧
        ∃ e3, e3 ∈ t3 ∧
        ¬ safe «e3» S«σ3, 0»
    ) as (t3 & σ3 & Hsteps & e3 & E3 & Hsafe).
    {
      apply nsteps_split in Hnsteps as ((t3, σ3) & Hnsteps1to3 & Hnsteps3to2).
      exists t3, σ3 ; repeat split.
      - assert (σ3 !! ℓ = None) by (eapply loc_fresh_in_dom_nsteps ; cycle 1 ; eassumption).
        replace m with (m+0)%nat by lia.
        apply simulation_exec_success ; assumption.
      - by eapply simulation_exec_failure_now.
    }
    apply (elem_of_list_fmap_1 translation) in E3.
    eapply not_safe_exec ; eassumption.
  Qed.

End Simulation.

Section Soundness.

  (* See also `TimeCreditsAltProofs.v` *)

  (* assuming the safety of the translated expression,
   * a proof that the computation time of the original expression is bounded. *)

  Local Lemma gt_sum m n :
    (m > n)%nat → ∃ (k : nat), m = (n + S k)%nat.
  Proof.
    intro. exists (m - S n)%nat. lia.
  Qed.
  Lemma safe_tctranslation__bounded {Hloc : TickCounter} m e σ t2 σ2 n :
    σ2 !! ℓ = None →
    safe «e» S«σ, m» →
    relations.nsteps erased_step n ([e], σ) (t2, σ2) →
    (n ≤ m)%nat.
  Proof.
    intros Hfresh Hsafe Hnsteps.
    (* reasoning by contradiction: assume (n > m), ie. (n = m + S k) for some k: *)
    apply not_gt ; intros [k ->] % gt_sum.
    (* apply the simulation lemma: *)
    by eapply simulation_exec_failure.
  Qed.

  Lemma adequate_tctranslation__bounded m φ e σ :
    (∀ `{TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))) →
    bounded_time e σ m.
  Proof.
    intros Hadq.
    intros t2 σ2 k.
    (* build a location ℓ which is not in the domain of σ2: *)
    pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
    assert (σ2 !! ℓ = None)
      by (unfold ℓ ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
    specialize (Hadq Hloc) as Hsafe % safe_adequate.
    by eapply safe_tctranslation__bounded.
  Qed.

  Definition adequate_tctranslation__nadequate := adequate_translation__nadequate fail.

  (* now let’s combine the three results. *)

  Lemma adequate_tctranslation__adequate_and_bounded m φ e σ :
    (∀ (k : nat), (k ≥ m)%nat →
      ∀ `{TickCounter}, adequate NotStuck «e» S«σ, k» (λ v σ, φ (invtranslationV v))
    ) →
    adequate NotStuck e σ (λ v σ, φ v)  ∧  bounded_time e σ m.
  Proof.
    intros Hadq.
    assert (bounded_time e σ m) as Hbounded
      by (eapply adequate_tctranslation__bounded, Hadq ; lia).
    assert (nadequate NotStuck (m + 1) e σ φ) as Hadqm
      by (apply adequate_tctranslation__nadequate, Hadq ; lia).
    clear Hadq.
    split ; last done.
    split.
    - intros t2 σ2 v2 [n Hnsteps] % rtc_nsteps.
      assert (n ≤ m)%nat as Inm by by eapply Hbounded.
      eapply nadequate_result ; try done ; lia.
    - intros t2 σ2 e2 _ [n Hnsteps] % rtc_nsteps He2.
      assert (n ≤ m)%nat as Inm by by eapply Hbounded.
      eapply nadequate_not_stuck ; try done ; lia.
  Qed.

  (* finally, derive the adequacy assumption from a Hoare triple in Iris. *)

  Lemma spec_tctranslation__adequate_translation {Σ} m ψ e :
    (∀ `{timeCreditHeapG Σ},
      TC_invariant -∗
      {{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v⌝ }}}
    ) →
    ∀ `{timeCreditHeapPreG Σ} `{TickCounter} σ,
      ∀ (k : nat), (k ≥ m)%nat → adequate NotStuck «e» S«σ,k» (λ v σ, ψ v).
  Proof.
    intros Hspec HpreG Hloc σ k Ik.
    (* apply the adequacy results. *)
    apply (wp_adequacy _ _) ; simpl ; intros HinvG.
    (* … now we have to prove a WP. *)
    set σ' := S«σ».
    (* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
    iMod (gen_heap_init (<[ℓ := #k]> σ')) as (Hheap) "(Hh● & Hℓ◯ & _)".
    iDestruct (big_sepM_lookup _ _ ℓ with "Hℓ◯") as "Hℓ◯".
    { by rewrite lookup_insert. }
    (* allocate the ghost state associated with ℓ: *)
    iMod (auth_nat_alloc k) as (γ) "[Hγ● Hγ◯]".
    (* packing all those bits, build the heap instance necessary to use time credits: *)
    pose (Build_timeCreditHeapG Σ (HeapGS Σ _ Hheap) _ _ γ)
      as HtcHeapG.
    (* create the invariant: *)
    iAssert (|={⊤}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> Hinv".
    {
      iApply inv_alloc.
      iExists k. iFrame.
    }
    iIntros (?) "!>".
    (* finally, use the user-given specification: *)
    iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iFrame.
    iDestruct (own_auth_nat_weaken _ _ _ Ik with "Hγ◯") as "Hγ◯".
    iApply (Hspec with "Hinv Hγ◯") ; auto.
  Qed.

  Theorem spec_tctranslation__adequate_and_bounded {Σ} m φ e :
    (∀ `{timeCreditHeapG Σ},
      TC_invariant -∗
      {{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v)⌝ }}}
    ) →
    ∀ {_ : timeCreditHeapPreG Σ} σ,
      adequate NotStuck e σ (λ v σ, φ v)  ∧  bounded_time e σ m.
  Proof.
    intros Hspec HpreG σ.
    apply adequate_tctranslation__adequate_and_bounded.
    intros k Ik Hloc. by eapply spec_tctranslation__adequate_translation.
  Qed.

  (* The abstract version of the theorem: *)
  Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m φ e :
    (∀ `{heapGS Σ, Tick} (TC : nat → iProp Σ),
      TC_interface TC -∗
      {{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v)⌝ }}}
    ) →
    ∀ {_ : timeCreditHeapPreG Σ} σ,
      adequate NotStuck e σ (λ v σ, φ v)  ∧  bounded_time e σ m.
  Proof.
    intros Hspec HpreG σ.
    eapply spec_tctranslation__adequate_and_bounded ; try done.
    clear HpreG. iIntros (HtcHeapG) "#Hinv".
    iApply Hspec. by iApply TC_implementation.
  Qed.

  (* A simplification for common use-cases: when the return value does not
   * contain a closure, there is no need to compose the postcondition φ with
   * the translation: *)
  Theorem spec_tctranslation__adequate_and_bounded' {Σ} m (φ : val → Prop) e :
    (∀ v, φ v → closure_free v) →
    (∀ `{timeCreditHeapG Σ},
      TC_invariant -∗
      {{{ TC m }}} «e» {{{ v, RET v ; ⌜φ v⌝ }}}
    ) →
    ∀ {_ : timeCreditHeapPreG Σ} σ,
      adequate NotStuck e σ (λ v σ, φ v)  ∧  bounded_time e σ m.
  Proof.
    intros Hφ Hspec HpreG σ.
    apply (spec_tctranslation__adequate_and_bounded (Σ:=Σ)) ; try assumption.
    intros HtcHeapG.
    iIntros "#Htickinv !#" (Φ) "Htc Post".
    wp_apply (Hspec with "Htickinv Htc"). iIntros (v Hv).
    iApply ("Post" with "[%]").
    by apply closure_free_predicate.
  Qed.

End Soundness.

(*
 * Proof-mode tactics for proving WP of translated expressions
 *)

Section Tactics.

  Context {Σ : gFunctors}.

  Implicit Types Φ : val → iProp Σ.
  Implicit Types Δ : envs (uPredI (iResUR Σ)).

  (* concrete version: *)
  Lemma tac_wp_tick `{timeCreditHeapG Σ} Δ Δ' Δ'' s E i j n K (v : val) Φ :
    ↑timeCreditN ⊆ E →
    MaybeIntoLaterNEnvs 1 Δ Δ' →
    envs_lookup i Δ  = Some (true, TC_invariant) →
    envs_lookup j Δ' = Some (false, TC (S n)) →
    envs_simple_replace j false (Esnoc Enil j (TC n)) Δ' = Some Δ'' →
    envs_entails Δ'' (WP fill K v @ s; E {{ Φ }}) →
    envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
  Proof.
    rewrite envs_entails_eq => HsubsetE ???? Hentails''.
    rewrite envs_lookup_intuitionistic_sound // intuitionistically_elim. apply wand_elim_r'.
    rewrite -wp_bind.
    eapply wand_apply ; first by (iIntros "HTC1 HΦ #Htick" ; iApply (tick_spec with "Htick HTC1 HΦ")).
    rewrite into_laterN_env_sound -later_sep /=. apply later_mono.
    rewrite envs_simple_replace_sound // ; simpl.
    rewrite TC_succ -sep_assoc. apply sep_mono_r.
    iIntros "[HTC Hwand] _". iApply Hentails''. iApply "Hwand" ; by iFrame.
  Qed.

(*
  (* TODO: abstract version: *)
  Lemma tac_wp_tick_abstr `{heapGS Σ} (TC : nat → iProp Σ) (tick : val) Δ Δ' Δ'' s E i j n K e (v : val) Φ :
    MaybeIntoLaterNEnvs 1 Δ Δ' →
    envs_lookup i Δ' = Some (true,  ∀ (v : val), {{{ TC 1%nat }}} tick v @ s ; E {{{ RET v ; True }}})%I →
    envs_lookup j Δ' = Some (false, TC (S n)) →
    envs_simple_replace i false (Esnoc Enil j (TC n)) Δ' = Some Δ'' →
    envs_entails Δ'' (WP fill K v @ s; E {{ Φ }}) →
    envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
  Admitted.
*)

End Tactics.

Ltac wp_tick ::=
  let solve_TICKCTXT _ :=
    iAssumptionCore || fail "wp_tick: cannot find TC_invariant" in
  let solve_TC _ :=
    iAssumptionCore || fail "wp_tick: cannot find TC (S _)" in
  iStartProof ;
  simpl_trans ;
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
      first
        [ reshape_expr false e ltac:(fun K e' =>
            eapply (tac_wp_tick _ _ _ _ _ _ _ _ K)
          )
        | fail 1 "wp_tick: cannot find 'tick ?v' in" e ] ;
      [ try solve_ndisj
      | exact _
      | solve_TICKCTXT ()
      | solve_TC ()
      | proofmode.reduction.pm_reflexivity
      | wp_expr_simpl ]
  | _ => fail "wp_tick: not a 'wp'"
  end.

author: Ricagraca

repo: i-splay-tree

save_path: github-repos/coq/Ricagraca-i-splay-tree


text:
From Hammer Require Import Hammer.

From WeakUpTo Require Export Relations.
Set Implicit Arguments.

Section Def1.
Variables X X' Y Y': Type.
Variable RX: relation2 X X'.
Variable R:  relation2 X Y.
Variable RY: relation2 Y Y'.
Variable R': relation2 X' Y'.
Definition diagram := forall x x' y, RX x x' -> R x y -> exists2 y', RY y y' & R' x' y'.
End Def1.
Section Def2.
Variable X: Type.
Variables R S: relation X.
Definition strong_commute := diagram R S R S.
Definition local_commute  := diagram R S (star R) (star S).
Definition semi_commute   := diagram R S (star R) S.
Definition commute        := diagram (star R) (star S) (star R) (star S).
Definition confluent      := diagram (star R) (star R) (star R) (star R).
End Def2.

Section Incl.
Variables X X' Y Y': Type.
Variable RX: relation2 X X'.
Variable R R':  relation2 X Y.
Variable RY: relation2 Y Y'.
Variables S S': relation2 X' Y'.
Hypothesis H: diagram RX R RY S.
Hypothesis HR: forall x y, R' x y -> R x y.
Hypothesis HS: forall x y, S x y -> S' x y.
Theorem diagram_incl: diagram RX R' RY S'.
Proof. hammer_hook "Diagrams" "Diagrams.diagram_incl".
intros x x' y Hxx' xRy.
elim (H Hxx' (y:=y)); auto.
intros y' Hyy' x'Ry'.
exists y'; auto.
Qed.
End Incl.

Section Reverse.
Variables X X' Y Y': Type.
Variable RX: relation2 X X'.
Variable R:  relation2 X Y.
Variable RY: relation2 Y Y'.
Variable R': relation2 X' Y'.
Hypothesis H: diagram RX R RY R'.
Theorem diagram_reverse: diagram R RX R' RY.
Proof. hammer_hook "Diagrams" "Diagrams.diagram_reverse".
intros x x' y Hxx' xRy.
elim (H xRy Hxx'); intros y' A B.
exists y'; assumption.
Qed.
End Reverse.

Section Compose.
Variables X Y Z X' Y' Z': Type.
Variable RY: relation2 Y Y'.
Variable RX: relation2 X X'.
Variable R1: relation2 X Y.
Variable R2: relation2 Y Z.
Variable RZ: relation2 Z Z'.
Variable S1: relation2 X' Y'.
Variable S2: relation2 Y' Z'.
Hypothesis H1: diagram RX R1 RY S1.
Hypothesis H2: diagram RY R2 RZ S2.
Theorem diagram_comp: diagram RX (comp R1 R2) RZ (comp S1 S2).
Proof. hammer_hook "Diagrams" "Diagrams.diagram_comp".
intros x x' z Hxx' xRz; destruct xRz as [ y xRy yRz ].
elim (H1 Hxx' xRy); intros y' Hyy' x'Sy'.
elim (H2 Hyy' yRz); intros z' Hzz' y'Sz'.
exists z'; auto.
exists y'; assumption.
Qed.
End Compose.

Section Union.
Variables X Y X' Y' I: Type.
Variable  RX: relation2 X X'.
Variables R: I -> relation2 X Y.
Variable  RY: relation2 Y Y'.
Variable  S: relation2 X' Y'.
Hypothesis H: forall i, diagram RX (R i) RY S.
Theorem diagram_union: diagram RX (union R) RY S.
Proof. hammer_hook "Diagrams" "Diagrams.diagram_union".
intros x x' z Hxx' xRy; destruct xRy as [ i xRy ].
elim (H Hxx' xRy); intros y' Hyy' x'Sy'.
exists y'; assumption.
Qed.
End Union.

Section Star.
Variables X X': Type.
Variable RX: relation2 X X'.
Variable R: relation X.
Variable S: relation X'.
Hypothesis H: diagram RX R RX (star S).
Theorem diagram_star: diagram RX (star R) RX (star S).
Proof. hammer_hook "Diagrams" "Diagrams.diagram_star".
intros x x' y Hxx' xRy; cgen Hxx'; cgen x'.
induction xRy as [ x | y x z xRy yRz IH ]; intros x' Hxx'.
exists x'; auto.
elim (H Hxx' xRy); intros y' Hyy' x'Sy'.
elim (IH _ Hyy'); intros z' Hzz' y'Sz'.
exists z'; auto.
apply star_trans with y'; assumption.
Qed.
End Star.

Section Plus.
Variables X X': Type.
Variable RX: relation2 X X'.
Variable R: relation X.
Variable S: relation X'.
Hypothesis HR: diagram RX R RX (plus S).
Theorem diagram_plus: diagram RX (plus R) RX (plus S).
Proof. hammer_hook "Diagrams" "Diagrams.diagram_plus".
intros x x' z Hxx' xRz; destruct xRz as [ y xRy yRz ].
elim (HR Hxx' xRy); intros y' Hyy' x'Sy'.
elim diagram_star with X X' RX R S y y' z; auto.
intros z' Hzz' y'Sz'.
exists z'; auto; apply plus_star_plus with y'; assumption.
apply diagram_incl with R (plus S); auto.
Qed.
End Plus.

Section PlusWf.

Variable X: Set.
Variable S: relation X.
Variable TX: relation X.

Hypothesis HS: diagram TX S (star TX) (plus S).
Hypothesis Hwf: well_founded (trans S).
Let Hpwf: well_founded (trans (plus S)) := plus_wf Hwf.

Lemma diagram_plus_wf: diagram (star TX) (plus S) (star TX) (plus S).
Proof. hammer_hook "Diagrams" "Diagrams.diagram_plus_wf".

intros x x'; cgen x.
induction x' as [x' IH ] using (well_founded_ind Hpwf).
intros x y xTx'; cgen y.

induction xTx' as [ x | x1 x x' xTx1 x1Ts' IHv ]; intros y xSy.
exists y; auto.
destruct xSy as [ w xSw wSy ].
destruct (HS xTx1 xSw) as [ w1 wTw1 x1Sw1 ].
elim IHv with w1; auto; intros w' w1Tw' x'Sw'.
destar wSy z.
exists w'; auto; apply star_trans with w1; assumption.
elim IH with w' w y; auto.
intros y' yTy' w'Ty'.
exists y'; auto; apply plus_trans with w'; assumption.
apply star_trans with w1; assumption.
Qed.

Variable TX': relation X.

Hypothesis HS': diagram TX' S (comp (star TX) TX') (plus S).

Lemma diagram_plus_wf_1: strong_commute (comp (star TX) TX') (plus S).
Proof. hammer_hook "Diagrams" "Diagrams.diagram_plus_wf_1".

intros x x'; cgen x.
induction x' as [x' IH ] using (well_founded_ind Hpwf).
intros x y xTx' xSy; destruct xTx' as [ x1 xTx1 x1Tx' ].
destruct (diagram_plus_wf xTx1 xSy) as [ y1 yTy1 x1Sy1 ].
destruct x1Sy1 as [ w1 x1Sw1 w1Sy1 ].
destruct (HS' x1Tx' x1Sw1) as [ w' w1Tw' x'Sw' ].
destar w1Sy1 z1.
destruct w1Tw' as [ w2 w1Tw2 w2Tw' ];
exists w'; auto; exists w2; auto; apply star_trans with w1; auto.
elim IH with w' w1 y1; auto.
intros y' y1Ty' w'Sy'; exists y'.
destruct y1Ty' as [ y2 y1Ty2 y2Ty' ];
exists y2; auto; apply star_trans with y1; auto.
apply plus_trans with w'; auto.
Qed.

Variable Y: Type.
Variables R R': relation2 X Y.
Variable TY TY': relation Y.

Hypothesis HR: diagram TX R (star TY) (comp (star S) R).
Hypothesis HR': diagram TX' R (comp (star TY) TY') (comp (star S) R').

Theorem diagram_plus_wf_2: diagram (comp (star TX) TX') (comp (star S) R) (comp (star TY) TY') (comp (star S) R').
Proof. hammer_hook "Diagrams" "Diagrams.diagram_plus_wf_2".

intros x x'; cgen x.
induction x' as [x' IH ] using (well_founded_ind Hpwf).
intros x y xTx' xSRy; destruct xSRy as [ w xSw wRy ].
destar xSw z.
destruct xTx' as [ x1 xTx2 x2Tx' ].

cgen wRy; cgen y; induction xTx2 as [ x | x1 x x2 xTx1 x1Tx2 IHv ]; intros y xRy.
exact (HR' x2Tx' xRy).
destruct (HR xTx1 xRy) as [ y1 yTy1 x1SRy1 ].
destruct x1SRy1 as [ w1 x1Sw1 w1Ry1 ]; destar x1Sw1 z1.
elim IHv with y1; auto; intros y' y1Ty' x'SRy'.
destruct y1Ty' as [ y2 ].
exists y'; auto; exists y2; auto; apply star_trans with y1; auto.

elim diagram_plus_wf_1 with x1 x' w1; auto.
intros w' w1Tw' x'Sw'.
elim IH with w' w1 y1; auto.
intros y' y1Ty' w'SRy'; exists y'; auto.
destruct y1Ty' as [ y2 ]; exists y2; auto; apply star_trans with y1; auto.
destruct w'SRy' as [ z' ]; exists z'; auto; apply star_trans with w'; auto.
exists w1; auto.
exists x2; auto.

destruct (diagram_plus_wf_1 xTx' xSw) as [ w' wTw' x'Sw' ].
elim IH with w' w y; auto.
intros y' yTy' w'SRy'; exists y'; auto.
destruct w'SRy' as [ z' ]; exists z'; auto; apply star_trans with w'; auto.
exists w; auto.
Qed.

End PlusWf.

Section StarWf.

Variable X: Set.
Variable S: relation X.
Variable TX: relation X.

Hypothesis HS: local_commute TX S.
Hypothesis Hwf: well_founded (trans (comp (plus S) (plus TX))).

Section Gen.
Variable Y: Type.
Variable R: relation2 X Y.
Variable TY: relation Y.

Let SR := comp (star S) R.
Hypothesis HR: diagram TX R (star TY) SR.

Lemma diagram_star_wf_1: diagram (star TX) SR (star TY) SR.
Proof. hammer_hook "Diagrams" "Diagrams.diagram_star_wf_1".
apply diagram_reverse.
apply diagram_star.
apply diagram_reverse.

intro x; induction x as [ x IH ] using (well_founded_ind Hwf).
intros x' y xTx' xSRy; cgen xTx'; cgen x'.
destruct xSRy as [ z xSz zRy ].

induction xSz as [ x | w x z xSw wSz IHh ]; intros x' xTx'.
destruct (HR xTx' zRy) as [ y' yTy' x'SRy' ]; exists y'; auto.
destruct (HS xTx' xSw) as [ w' wTw' x'Sw' ].
destruct wTw' as [ w | w1 w w' wTw1 w1Tw' ].
exists y; auto; exists z; auto; apply star_trans with w; assumption.
elim IHh with w1; auto.
intros z1 zTz1 w1Sz1.
cut (forall w2,
star TX w1 w2 ->
forall w3 y2,
TX w2 w3 -> SR w2 y2 -> exists2 y3, star TY y2 y3 & SR w3 y3).
clear IH IHh xTx' xSw x wSz wTw1 w; intro IH; cgen w1Sz1; cgen zTz1; cgen z1.

induction w1Tw' as [ w1 | w2 w1 w' w1Tw2 w2Tw' IHv ]; intros y1 yTy1 w1SRy1.
destruct w1SRy1 as [ z1 w1Sz1 z1Ry1 ].
exists y1; auto; exists z1; auto; apply star_trans with w1; auto.
elim IH with w1 w2 y1; auto; intros y2 y1Ty2 w2Sy2.
elim IHv with y2; auto.
intros y' y2Ty' w'SRy'.
destruct w'SRy' as [ z' w'Sz' z'Ry' ].
exists y'; auto; exists z'; auto; apply star_trans with z1; assumption.
intros w3 w2Tw3 w4 y3 w3Tw4 w3SRy3.
elim IH with w3 w4 y3; auto.
intros y4 y3Ty4 w4SRy4.
destruct w4SRy4 as [ z4 w4Sz4 s4Ry4 ].
exists y4; auto; exists z4; auto; apply star_trans with w3; assumption.
apply S_star with w2; assumption.
apply star_trans with y1; assumption.

intros w2 w1Tw2 w3 y2 w2Tw3 w2SRy2; destruct w2SRy2 as [ z2 w2Sz2 z2Ry2 ].
elim IH with w2 w3 y2; auto.
intros y3 y2Ty3 w3SRy3.
exists y3; auto.
exists w; auto.
exists w1; assumption.
exists z2; assumption.

intros w2 wSTw2 w3 y2 w2Tw3 w2SRy2; destruct w2SRy2 as [ z2 w2Sz2 z2Ry2 ].
destruct wSTw2 as [ u wSu uTw2 ].
elim IH with w2 w3 y2; auto.
intros y3 y2Ty3 w3SRy3; destruct w3SRy3 as [ z3 w3Sz3 z3Ry3 ].
exists y3; auto.
exists z3; auto.
exists u; auto; exists w; auto.
exists z2; assumption.
Qed.

Variables X' Y': Type.
Variable TaX: relation2 X X'.
Variable TaY: relation2 Y Y'.
Variable S' : relation2 X' X'.
Variable R' : relation2 X' Y'.

Let SR' := comp (star S') R'.
Let TAX := comp (star TX) TaX.
Let TAY := comp (star TY) TaY.

Hypothesis HT:  diagram TaX S TAX (star S').
Hypothesis HRT: diagram TaX R TAY SR'.

Theorem diagram_star_wf_2: diagram TAX SR TAY SR'.
Proof. hammer_hook "Diagrams" "Diagrams.diagram_star_wf_2".
apply diagram_reverse.
apply diagram_incl with TAX (comp (star TY) TAY); auto.
unfold TAX; eapply diagram_comp;
apply diagram_reverse.
apply diagram_star_wf_1.

intro x; induction x as [ x IH ] using (well_founded_ind Hwf).
intros x' y xTx' xSRy; cgen xTx'; cgen x'.
destruct xSRy as [ z xSz zRy ].

induction xSz as [ x | w x z xSw wSz IHh ]; intros x' xTx'.
destruct (HRT xTx' zRy) as [ y' yTy' x'SRy' ]; exists y'; auto.
destruct (HT xTx' xSw) as [ w' wTw' x'Sw' ].
destruct wTw' as [ wa wTwa waTw' ].
destruct wTwa as [ w | w1 w wa wTw1 w1Twa ].
elim IHh with w'; auto.
intros y' yTy' w'SRy'; exists y'; auto.
destruct w'SRy' as [ z' ]; exists z'; auto; apply star_trans with w'; assumption.
intros u Hu; apply IH; auto; destruct Hu as [ t ]; exists t; auto; apply S_plus with w; auto.

elim diagram_star_wf_1 with w wa y.
intros ya yTya waSRya.
elim IH with wa w' ya; auto.
intros y' yaTy' w'SRy'; exists y'.
destruct yaTy' as [ yb yaTyb ybTy' ]; exists yb; auto; apply star_trans with ya; assumption.
destruct w'SRy' as [ z' w'Tz' z'Ty' ]; exists z'; auto; apply star_trans with w'; assumption.
exists w; auto; exists w1; assumption.
apply S_star with w1; assumption.
exists z; auto.

intros x y H; destruct H as [ z H H']; destruct H' as [ t ];
exists t; auto; apply star_trans with z; assumption.
Qed.

End Gen.

Lemma diagram_star_wf: commute TX S.
Proof. hammer_hook "Diagrams" "Diagrams.diagram_star_wf".
unfold commute.
generalize (diagram_star_wf_1 (Y:=X) (R := eq (A:=X)) (TY:=TX)); intro H.
intros x x' y xTx' xSy.
elim H with x x' y; auto.
intros y' yTy' x'Sy'; exists y'; auto.
destruct x'Sy' as [ t' XT TY ].
destruct TY; assumption.
intros u u' v UU' UV; destruct UV; exists u'; auto; exists u'; auto.
exists y; auto.
Qed.

End StarWf.

author: lukaszcz

repo: coqhammer-eval


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Definition synth (lf2 : natural) (y : natural) (lf1 : natural) : natural :=
  plus lf1 lf2.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import Essentials.Notations.
Require Import Essentials.Types.
Require Import Essentials.Facts_Tactics.
Require Import Category.Main.
Require Import Functor.Main.
Require Import NatTrans.Main.
Require Import Adjunction.Adjunction Adjunction.Duality.
Require Import Ext_Cons.Comma.
Require Import Basic_Cons.Terminal Basic_Cons.Facts.Term_IsoCat.
Require Import Cat.Cat_Iso.
Require Import Archetypal.Discr.Discr Archetypal.Discr.NatFacts.

(** A functor G : D –≻ C has a left adjoint if and only if
the comma category (Comma (Func_From_SingletonCat x) G) has
an initial object for any (x : C).

Dually, a functor F : C –≻ D has a right adjoint if and only
if the comma category (Comma F (Func_From_SingletonCat x))
has a terminal object for any (x : D).
 *)

(**
If the comma category (Comma (Func_From_SingletonCat x) G) has
an initial object for any (x : C). Then G : D –≻ C has
a left adjoint.
*)

Section Universal_Morphism_Right_Adjonit.
  Context
    {C D : Category}
    (G : (D –≻ C)%functor)
    (HU_init : ∀ (x : C), Initial (Comma (Func_From_SingletonCat x) G) )
  .

  Local Definition Universal_Morphism_Lem :
    ∀ c a h,
      CMH_right (t_morph (HU_init c) a) = CMH_right h
  .
  Proof.
    intros c a h.
    apply f_equal.
    apply (t_morph_unique (HU_init c)).
  Qed.

  Local Ltac smart_apply_Universal_Morphism_Lem :=
    match goal with
      [|- CMH_right ?A = ?B] =>
      match type of A with
        ?W =>
        let M :=
            (eval cbn in W)
        in
        match M with
          Comma_Hom _ _ ?X ?Y =>
          evar (U : Comma_Hom _ _ X Y);
            replace B with (CMH_right ?U);
            [
              eapply
                (
                  Universal_Morphism_Lem
                    _
                    Y
                    (
                      Build_Comma_Hom
                        _
                        _
                        X
                        Y
                        tt
                        B
                        _
                    )
                )
            |
            reflexivity
            ]
        end
      end
    end.

  Program Definition Universal_Morphism_Right_Adjonit_Func : (C –≻ D)%functor
    :=
      {|
        FO :=
          fun c =>
            CMO_trg (terminal (HU_init c));
        FA :=
          fun c c' h =>
            CMH_right
              (t_morph
                 (HU_init c)
                 (@Build_Comma_Obj
                    _
                    _
                    _
                    (Const_Func 1 c)
                    G
                    tt
                    (CMO_trg (terminal (HU_init c')))
                    ((CMO_hom (terminal (HU_init c'))) ∘ h)%morphism
                 )
              )
      |}
  .

  Next Obligation.
  Proof.
    smart_apply_Universal_Morphism_Lem.
    Unshelve.
    cbn; auto.
  Qed.

  Next Obligation.
  Proof.
    smart_apply_Universal_Morphism_Lem.
    Unshelve.
    {
      cbn.
      rewrite F_compose.
      rewrite assoc.
      simpl_ids;
      match goal with
        [|- ((G _a) ((CMH_right ?A)) ∘ ((G _a) (CMH_right ?B)) ∘ _)%morphism = _] =>
        cbn_rewrite (CMH_com B);
          do 2 rewrite assoc_sym;
          cbn_rewrite (CMH_com A); auto
      end.
    }
  Qed.

  Local Obligation Tactic := idtac.

  Program Definition Universal_Morphism_Right_Adjonit_unit :
    (Functor_id C –≻ G ∘ Universal_Morphism_Right_Adjonit_Func)%nattrans
    :=
      {|
        Trans := fun c => CMO_hom (terminal (HU_init c))
      |}
  .

  Next Obligation.
  Proof.
    intros c c' h.
    cbn.
    match goal with
      [|- _ = (G _a (CMH_right ?A) ∘ _)%morphism] =>
      cbn_rewrite (CMH_com A)
    end.
    auto.
  Qed.

  Next Obligation.
  Proof.
    symmetry.
    apply Universal_Morphism_Right_Adjonit_unit_obligation_1.
  Qed.

  Program Definition Universal_Morphism_Right_Adjonit :
    (Universal_Morphism_Right_Adjonit_Func ⊣ G)%functor
    :=
      {|
        adj_unit := Universal_Morphism_Right_Adjonit_unit;
        adj_morph_ex :=
          fun c d f =>
            CMH_right
              (t_morph
                 (HU_init c)
                 (@Build_Comma_Obj
                    _
                    _
                    _
                    (Const_Func 1 c)
                    G
                    tt
                    d
                    f
                 )
              )
      |}
  .

  Next Obligation.
  Proof.
    intros c d f.
    cbn in *.
    match goal with
      [|- _ = (G _a (CMH_right ?A) ∘ _)%morphism] =>
      cbn_rewrite (CMH_com A)
    end.
    auto.
  Qed.

  Next Obligation.
  Proof.
    intros c d f g h H1 H2.
    cbn in *.
    rewrite <- (id_unit_right _ _ f) in H1, H2.
    symmetry in H1, H2.
    set (W :=
           @Build_Comma_Obj
             _
             _
             _
             (Const_Func 1 c)
             G
             tt
             d
             f
        )
    .
    let tac u H
        :=
        (
          change u with
          (
            CMH_right
              (
                Build_Comma_Hom
                  _
                  _
                  (terminal (HU_init c))
                  W
                  tt
                  u
                  H
              )
          )
        )
    in
    tac g H1;
      tac h H2
    .
    transitivity (CMH_right (t_morph (HU_init c) W));
      [symmetry|];
      apply (Universal_Morphism_Lem c W)
    .
  Qed.

End Universal_Morphism_Right_Adjonit.

(**
if a functor G : D –≻ C has a left adjoint then the comma
category (Comma (Func_From_SingletonCat x) G) has
an initial object for any (x : C).
*)
Section Right_Adjoint_Universal_Morphism.
  Context
    {C D : Category}
    {F : (C –≻ D)%functor}
    {G : (D –≻ C)%functor}
    (Adj : (F ⊣ G)%functor)
    (x : C)
  .

  Program Definition Right_Adjoint_Universal_Morphism_terminal : (Comma (Func_From_SingletonCat x) G)
    :=
      {|
        CMO_src := tt;
        CMO_trg := (F _o x)%object;
        CMO_hom := Trans (adj_unit Adj) x
      |}
  .

  Program Definition Right_Adjoint_Universal_Morphism_t_morph
          (u : (Comma (Func_From_SingletonCat x) G))
    :
      Comma_Hom _ _ Right_Adjoint_Universal_Morphism_terminal u
    :=
      {|
        CMH_left := tt;
        CMH_right :=
          @adj_morph_ex
            _
            _
            _
            _
            Adj
            x
            (CMO_trg u)
            (CMO_hom u)
      |}
  .

  Next Obligation.
  Proof.
    simpl_ids.
    symmetry.
    apply (@adj_morph_com _ _ _ _ Adj).
  Qed.

  Program Definition Right_Adjoint_Universal_Morphism : Initial (Comma (Func_From_SingletonCat x) G)
    :=
      {|
        terminal := Right_Adjoint_Universal_Morphism_terminal;
        t_morph := Right_Adjoint_Universal_Morphism_t_morph
      |}
  .

  Next Obligation.
  Proof.
    assert (Hf := CMH_com f).
    assert (Hg := CMH_com g).
    cbn in *.
    simpl_ids in Hf; simpl_ids in Hg.
    symmetry in Hf, Hg.
    apply Comma_Hom_eq_simplify.
    match goal with
      [|- ?A = ?B] =>
      destruct A; destruct B; trivial
    end.
    eapply (@adj_morph_unique _ _ _ _ Adj); eauto.
  Qed.

End Right_Adjoint_Universal_Morphism.

(**
If the comma category (Comma F (Func_From_SingletonCat x)) has
an initial object for any (x : D). Then F : D –≻ C has
a right adjoint.
*)
Section Universal_Morphism_Left_Adjonit.
  Context
    {C D : Category}
    (F : (C –≻ D)%functor)
    (HU_term : ∀ (x : D), Terminal (Comma F (@Func_From_SingletonCat D x)))
  .

  Definition Universal_Morphism_Left_Adjonit_HU_init
             (x : (D^op)%category)
    :
      Initial (Comma ((@Func_From_SingletonCat (D ^op) x)) (F^op))
    :=
      Term_IsoCat
        (
          Opposite_Cat_Iso
            (
              Isomorphism_Compose
                (Comma_Opposite_Iso F (@Func_From_SingletonCat D x))
                (Comma_Left_Func_Iso (@Func_From_SingletonCat_Opposite D x) (F ^op))
            )
        )
        (HU_term x)
  .

  Definition Universal_Morphism_Left_Adjonit
    :
      (F ⊣ (
               Universal_Morphism_Right_Adjonit_Func
                 (F ^op)
                 Universal_Morphism_Left_Adjonit_HU_init
             )^op
      )%functor
    :=
      Adjunct_Duality
        (
          @Universal_Morphism_Right_Adjonit
            (D^op)
            (C^op)
            (F^op)
            Universal_Morphism_Left_Adjonit_HU_init
        )
  .

End Universal_Morphism_Left_Adjonit.

(**
if a functor F : C –≻ D has a right adjoint then the comma
category (Comma F (Func_From_SingletonCat x)) has
an terminal object for any (x : D).
*)
Section Left_Adjoint_Universal_Morphism.
  Context
    {C D : Category}
    {F : (C –≻ D)%functor}
    {G : (D –≻ C)%functor}
    (Adj : (F ⊣ G)%functor)
    (x : D)
  .

  Definition Left_Adjoint_Universal_Morphism : Terminal (Comma F (Const_Func 1 x))
    :=
      Term_IsoCat
        (
          Opposite_Cat_Iso
            (
              Isomorphism_Compose
                (
                  Comma_Left_Func_Iso
                    (Inverse_Isomorphism (@Func_From_SingletonCat_Opposite D x))
                    (F ^op)
                )
                (Inverse_Isomorphism (Comma_Opposite_Iso F (@Func_From_SingletonCat D x)))
            )
        )
        (Right_Adjoint_Universal_Morphism (Adjunct_Duality Adj) x)
  .

End Left_Adjoint_Universal_Morphism.

author: amintimany

repo: Categories-HoTT