text:
(*
 - Definition of adjoint equivalences
 - Projections
 - Proofs of inverse triangles
*)

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.

Require Import Integers.WildCategories.WildCat.
Require Import Integers.WildCategories.DispWildCat.
Require Import Integers.WildCategories.Invertible_2cells.
Require Import Integers.WildCategories.WildFunctor.
Import WildFunctor.Notations.
Require Import Integers.WildCategories.WildNaturalTransformation.
Import WildNaturalTransformation.Notations.
Require Import Integers.WildCategories.WildNaturalIsomorphism.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

(** Definition **)
Definition is_adjoint_equivalence
           {C D : wild_cat}
           (L : wild_functor C D)
           (R : wild_functor D C)
  : UU.
Proof.
  use total2.
  - exact (wild_nat_iso (R ✦ L) (id_wild_functor D) × wild_nat_iso (id_wild_functor C) (L ✦ R)).
  - intro units.
    destruct units as [ε η].
    exact ((∏ (a : D), invertible_2cell (η (R a) · #R (ε a)) (id₁ (R a)))
             ×
             ∏ (a : C), invertible_2cell (#L (η a) · ε (L a)) (id₁ (L a))).
Defined.

Definition adjoint_equivalence (C D : wild_cat) : UU
  := ∑ (L : wild_functor C D) (R : wild_functor D C), is_adjoint_equivalence L R.

Definition make_adjoint_equivalence
           {C D : wild_cat}
           (L : wild_functor C D)
           (R : wild_functor D C)
           (ε : wild_nat_iso (R ✦ L) (id_wild_functor D))
           (η : wild_nat_iso (id_wild_functor C) (L ✦ R))
           (tR : ∏ (a : D), invertible_2cell (η (R a) · #R (ε a)) (id₁ (R a)))
           (tL : ∏ (a : C), invertible_2cell (#L (η a) · ε (L a)) (id₁ (L a)))
  : adjoint_equivalence C D
  := L ,, R ,, (ε ,, η) ,, tR ,, tL.

(** Projections **)
Definition adj_left {C D : wild_cat} (A : adjoint_equivalence C D)
  : wild_functor C D
  := pr1 A.

(*Coercion adj_left : adjunction >-> wild_functor.*)

Definition adj_right {C D : wild_cat} (A : adjoint_equivalence C D)
  : wild_functor D C
  := pr12 A.

Definition adj_counit {C D : wild_cat} (A : adjoint_equivalence C D)
  : wild_nat_iso ((adj_right A) ✦ (adj_left A)) (id_wild_functor D)
  := pr1 (pr122 A).

Definition adj_unit {C D : wild_cat} (A : adjoint_equivalence C D)
  : wild_nat_iso (id_wild_functor C) ((adj_left A) ✦ (adj_right A))
  := pr2 (pr122 A).

Definition adj_tR {C D : wild_cat} (A : adjoint_equivalence C D)
  : ∏ (a : D), invertible_2cell
                 ((adj_unit A) (adj_right A a) · #(adj_right A) (adj_counit A a))
                 (id₁ (adj_right A a))
  := pr1 (pr222 A).

Definition adj_tL {C D : wild_cat} (A : adjoint_equivalence C D)
  : ∏ (a : C), invertible_2cell
                 (#(adj_left A) (adj_unit A a) · adj_counit A (adj_left A a))
                 (id₁ (adj_left A a))
  := pr2 (pr222 A).

(** Inverse triangles **)
Lemma adj_tL_inv {C D : wild_cat} (A : adjoint_equivalence C D)
  : ∏ (a : C), invertible_2cell
                 (wild_nat_iso_trans_inv (adj_counit A) (adj_left A a)
                   · #(adj_left A) (wild_nat_iso_trans_inv (adj_unit A) a))
                 (id₁ (adj_left A a)).
Proof.
  intro a.
  use tpair.
  - refine (_ • _ • _ • _ • _ • _ • _ • _ • _).
    + apply linvunitor.
    + apply ((adj_tL A a)^-1 ▹ _).
    + apply rassociator.
    + apply (_ ◃ lassociator _ _ _).
    + apply (_ ◃ (wild_nat_iso_r (adj_counit A) (adj_left A a) ▹ _)).
    + apply (_ ◃ lunitor _).
    + apply (wild_functor_comp (adj_left A)).
    + apply (##(adj_left A) (wild_nat_iso_r (adj_unit A) a)).
    + apply ((wild_functor_id (adj_left A) a)^-1).
  - refine (_ • _ • _ • _ • _ • _ • _ • _ • _).
    + apply ((wild_functor_id (adj_left A) a)).
    + apply (##(adj_left A) ((wild_nat_iso_r (adj_unit A) a)^-1)).
    + apply ((wild_functor_comp (adj_left A) _ _)^-1).
    + apply (_ ◃ linvunitor _).
    + apply (_ ◃ ((wild_nat_iso_r (adj_counit A) (adj_left A a)^-1) ▹ _)).
    + apply (_ ◃ rassociator _ _ _).
    + apply lassociator.
    + apply (adj_tL A a ▹ _).
    + apply lunitor.
Qed.

Lemma adj_tR_inv {C D : wild_cat} (A : adjoint_equivalence C D)
  : ∏ (b : D), invertible_2cell
                 (#(adj_right A) (wild_nat_iso_trans_inv (adj_counit A) b)
                   · wild_nat_iso_trans_inv (adj_unit A) (adj_right A b))
                 (id₁ (adj_right A b)).
Proof.
  intro b.
  use tpair.
  - refine (_ • _ • _ • _ • _ • _ • _ • _ • _).
    + apply linvunitor.
    + apply ((adj_tR A b)^-1 ▹ _).
    + apply rassociator.
    + apply (_ ◃ lassociator _ _ _).
    + apply (_ ◃ (wild_functor_comp (adj_right A) _ _ ▹ _)).
    + apply (_ ◃ ((##(adj_right A) (wild_nat_iso_r (adj_counit A) b) ) ▹ _)).
    + apply (_ ◃ (((wild_functor_id _ _)^-1) ▹ _)).
    + apply (_ ◃ lunitor _).
    + apply (wild_nat_iso_r (adj_unit A) (adj_right A b)).
  - refine (_ • _ • _ • _ • _ • _ • _ • _ • _).
    + apply ((wild_nat_iso_r (adj_unit A) (adj_right A b))^-1).
    + apply (_ ◃ linvunitor _).
    + apply (_ ◃ ((wild_functor_id (adj_right A) _ ) ▹ _)).
    + apply (_ ◃ ((##(adj_right A) ((wild_nat_iso_r (adj_counit A) b)^-1)) ▹ _)).
    + apply (_ ◃ ((wild_functor_comp (adj_right A) _ _)^-1 ▹ _)).
    + apply (_ ◃ rassociator _ _ _).
    + apply lassociator.
    + apply (adj_tR A b ▹ _).
    + apply lunitor.
Qed.

author: nmvdw

repo: Integers

save_path: github-repos/coq/nmvdw-Integers


text:
(** Strong normalization of the model of CC+W in the type-based
  termination presentation.
*)
Require Import basic Models.
Require SN_ECC_Real.
Import ZFgrothendieck.
Import ZF ZFsum ZFnats ZFrelations ZFord ZFfix.
Require Import ZFfunext ZFfixrec ZFcoc ZFecc ZFuniv_real SATtypes SATw.

Import SN_ECC_Real.
Opaque Real.
Import Sat Sat.SatSet.

(** Typing rules related to ordinals *)

Require Import SN_ord.

(** Judgments with variance *)

Require Import SN_variance.

(** W *)

(** The abstract model construction is a functor based on any
    abstract set-theoretical model of W-types. *)
Module Make(W:W_PartialModel).

Module Wsat := SATw.Make(W).
Import W Wsat.

(** Facts derived from the signature *)

(** Back to the subject: W-types model construction *)
Section Wtypes_typing.

Variable o : set.
Hypothesis oo : isOrd o.
Hypothesis oz : zero ∈ o.

Variable e:env.

Variable A B:term.
Hypothesis Atyp : typ e A kind.
Hypothesis Btyp : typ (A::e) B kind.

Let Aw i := El (int A i).
Let Bw i x := El (int B (V.cons x i)).
Let RAw i a := Real (int A i) a.
Let RBw i a b := Real (int B (V.cons a i)) b.

Definition WF i X := W_F (Aw i) (Bw i) X.
Definition RW i o w := rWi (Aw i) (Bw i) (RAw i) (RBw i) o w.

Instance Aw_morph : Proper (eq_val==>eq_set) Aw.
do 2 red; intros.
apply El_morph.
apply int_morph; auto with *.
Qed.

Instance Bw_morph : Proper (eq_val==>eq_set==>eq_set) Bw.
do 3 red; intros.
apply El_morph.
rewrite H; rewrite H0; reflexivity.
Qed.
Instance Bwi_morph i : morph1 (Bw i).
apply Bw_morph; reflexivity.
Qed.

Instance RAw_morph : Proper (eq_val ==> eq_set ==> eqSAT) RAw.
do 3 red; intros.
unfold RAw.
rewrite H; rewrite H0; reflexivity.
Qed.
Instance RAwi_morph i : Proper (eq_set ==> eqSAT) (RAw i).
apply RAw_morph; reflexivity.
Qed.

Instance RBw_morph : Proper (eq_val ==> eq_set ==> eq_set ==> eqSAT) RBw.
do 4 red; intros.
unfold RBw.
rewrite H; rewrite H0; rewrite H1; reflexivity.
Qed.
Instance RBwi_morph i : Proper (eq_set ==> eq_set ==> eqSAT) (RBw i).
apply RBw_morph; reflexivity.
Qed.

Instance WF_morph : Proper (eq_val ==> eq_set ==> eq_set) WF.
do 3 red; intros.
apply W_F_ext; trivial.
 apply Aw_morph; trivial.

 red; intros.
 apply Bw_morph; trivial.
Qed.

  Lemma WF_mono i : Proper (incl_set==>incl_set) (WF i).
do 2 red; intros.
unfold WF.
apply W_F_mono; auto with *.
Qed.
  Hint Resolve WF_mono.

Instance RW_morph : Proper (eq_val ==> eq_set ==> eq_set ==> eqSAT) RW.
do 4 red; intros.
unfold RW.
apply rWi_morph_gen; auto with *.
 apply Aw_morph; trivial.
 apply Bw_morph; trivial.
 apply RAw_morph; trivial.
 apply RBw_morph; trivial.
Qed.

Definition WI (O:term) : term.
(*begin show*)
left; exists (fun i => mkTY (TI (WF i) (int O i)) (RW i (int O i)))
             (fun j => Lc.App2 Lc.K (tm A j) (Lc.App2 Lc.K (Lc.Abs(tm B (Lc.ilift j))) (tm O j))).
(*end show*)
 do 2 red; intros.
 apply mkTY_ext; intros.
  apply TI_morph_gen.
   apply WF_morph; trivial.
   rewrite H; reflexivity.

  apply RW_morph; trivial.
  rewrite H; reflexivity.
 (**)
 do 2 red; intros.
 rewrite H; reflexivity.
 (**)
 red; intros.
 simpl.
 rewrite <- tm_liftable.
 rewrite <- tm_liftable.
 rewrite <- tm_liftable.
 unfold Lc.App2.
 f_equal.
 f_equal.
 f_equal.
 f_equal.
 apply tm_morph; auto with *.
 apply Lc.ilift_binder_lift.
 (**)
 red; intros.
 simpl.
 rewrite <- tm_substitutive.
 rewrite <- tm_substitutive.
 rewrite <- tm_substitutive.
 unfold Lc.App2.
 f_equal.
 f_equal.
 f_equal.
 f_equal.
 apply tm_morph; auto with *.
 apply Lc.ilift_binder.
Defined.

Lemma El_int_W O i :
  El (int (WI O) i) == cc_bot (TI (WF i) (int O i)).
simpl.
rewrite El_def; reflexivity.
Qed.
Lemma Real_int_W O i x :
  x ∈ cc_bot (TI (WF i) (int O i)) ->
  eqSAT (Real (int (WI O) i) x) (RW i (int O i) x).
simpl; intros.
rewrite Real_def; auto with *.
intros.
rewrite H1; reflexivity.
Qed.

Lemma typ_WI : forall eps O,
  isOrd eps ->
  typ e O (Ordt eps) ->
  typ e (WI O) kind.
red; intros; simpl.
red in H0; specialize H0 with (1:=H1).
assert (tyA := Atyp _ _ H1).
apply in_int_not_kind in H0.
2:discriminate.
destruct tyA as (Ank,(_,snA)).
destruct (Btyp _ _ (val_ok_cons_default H1 Ank)) as (Bnk,(_,snB)).
split;[|split].
 discriminate.

 exists nil; exists (WI O);[reflexivity|].
 exists empty; simpl; auto.
 red; auto.

 simpl.
 apply real_sn in H0.
 apply Lc.sn_K2; trivial.
 apply Lc.sn_K2; trivial.
 apply Lc.sn_abs.
 rewrite tm_subst_cons in snB.
 apply Lc.sn_subst in snB; trivial.
Qed.
(** Constructor *)

Definition Wc (x:term) (f:term) : term.
(* begin show *)
left; exists (fun i => mkw (int x i) (int f i))
             (fun j => WC (tm x j) (tm f j)).
(* end show *)
 do 2 red; intros; apply mkw_morph; apply int_morph; auto with *.
 (**)
 do 2 red; intros.
 rewrite H; reflexivity.
 (**)
 red; intros.
 unfold WC, COUPLE; simpl.
 do 2 rewrite tm_liftable.
 do 2 rewrite Lc.permute_lift; reflexivity.
 (**)
 red; intros.
 unfold WC, COUPLE; simpl.
 do 2 rewrite tm_substitutive.
 do 2 rewrite Lc.commut_lift_subst; reflexivity.
Defined.

Lemma typ_Wc : forall O X F,
  typ e O (Ordt o) ->
  typ e X A ->
  typ e F (Prod (subst X B) (lift 1 (WI O))) ->
  typ e (Wc X F) (WI (OSucc O)).
red; intros.
red in H0; specialize H0 with (1:=H2).
apply in_int_not_kind in H0.
2:destruct (Atyp _ _ H2); trivial.
red in H1; specialize H1 with (1:=H2).
apply in_int_not_kind in H1.
2:discriminate.
destruct tyord_inv with (3:=H)(4:=H2) as (?,(?,_)); trivial.
apply in_int_intro; try discriminate.
assert (mkw (int X0 i) (int F i) ∈ TI (WF i) (osucc (int O i))).
 apply TI_intro with (int O i); auto.
 apply W_F_intro.
  apply Bw_morph; auto with *.

  apply H0.

  destruct H1.
  red in H1; rewrite El_int_arr in H1.
  rewrite El_int_W in H1.
  rewrite <- int_subst_eq in H1.
  trivial.
split.
 red; rewrite El_int_W; auto.

 rewrite Real_int_W; auto.
 simpl.
 unfold RW; apply Real_WC; auto with *.
  rewrite w1_eq.
  apply H0.

  destruct H1.
  red in H1; rewrite El_int_prod in H1.
  rewrite Real_int_prod in H6; trivial.
  revert H6; apply piSAT0_morph; intros.
   red; intros.
   rewrite w1_eq.
   rewrite <- int_subst_eq; reflexivity.

   rewrite w1_eq.
   rewrite <- int_subst_eq; reflexivity.

   rewrite int_cons_lift_eq.
   rewrite Real_int_W.
    unfold RW; apply rWi_morph; auto with *.
     rewrite w2_eq; reflexivity.

     apply cc_prod_elim with (2:=H7) in H1.
     rewrite int_cons_lift_eq in H1.
     rewrite El_int_W in H1; trivial.
Qed.

(* Case analysis *)

Definition mkw_case (b : set -> set -> set) c :=
  cond_set (c == mkw (w1 c) (w2 c)) (b (w1 c) (w2 c)).

Definition W_CASE b w :=
  mkw_case (fun x f => app (app b x) f) w.

Definition Wcase (b n : term) : term.
(*begin show*)
left; exists (fun i => W_CASE (int b i) (int n i))
             (fun j => WCASE (tm b j) (tm n j)).
(*end show*)
do 2 red; intros.
unfold W_CASE.
apply cond_set_morph.
 rewrite H; reflexivity.
 rewrite H; reflexivity.
(**)
do 2 red; intros.
unfold WCASE; rewrite H; reflexivity.
(**)
red; intros; simpl.
unfold WCASE; simpl.
do 2 rewrite tm_liftable; reflexivity.
(**)
red; intros; simpl.
unfold WCASE; simpl.
do 2 rewrite tm_substitutive; reflexivity.
Defined.

Instance Wcase_morph :
  Proper (eq_term ==> eq_term ==> eq_term) Wcase.
do 3 red; intros.
split; red; simpl; intros.
 unfold sigma_case.
 apply cond_set_morph.
  rewrite H0; rewrite H1; reflexivity.
  rewrite H; rewrite H0; rewrite H1; reflexivity.

 rewrite H; rewrite H0; rewrite H1; reflexivity.
Qed.

Lemma Wcase_iota : forall X F G,
  eq_typ e (Wcase G (Wc X F)) (App (App G X) F).
red; red; intros.
simpl.
unfold W_CASE.
unfold mkw_case; rewrite cond_set_ok.
 rewrite w1_eq, w2_eq; reflexivity.
 rewrite w1_eq, w2_eq; reflexivity.
Qed.

Lemma typ_Wcase P O G n :
  typ e O (Ordt o) ->
  typ e G (Prod A (Prod (Prod B (lift 2 (WI O))) (App (lift 2 P) (Wc (Ref 1) (Ref 0))))) ->
  typ e n (WI (OSucc O)) ->
  typ e (Wcase G n) (App P n).
red; intros.
destruct tyord_inv with (3:=H)(4:=H2) as (?,(?,_ )); trivial.
red in H0; specialize H0 with (1:=H2).
apply in_int_not_kind in H0;[|discriminate].
red in H1; specialize H1 with (1:=H2).
apply in_int_not_kind in H1;[|discriminate].
apply in_int_intro; try discriminate.
destruct H0; red in H0.
rewrite El_int_prod in H0.
rewrite Real_int_prod in H5; trivial.
destruct H1; red in H1.
rewrite El_int_W in H1.
rewrite Real_int_W in H6; trivial.
apply and_split; intros.
 red; simpl.
 rewrite cc_bot_ax in H1; destruct H1.
  unfold W_CASE, mkw_case.
  rewrite H1.
  rewrite cond_set_mt; auto.
  apply discr_mt_mkw.

  simpl in H1; rewrite TI_mono_succ in H1; auto with *.
  apply W_F_elim in H1.
  2:apply Bw_morph; auto with *.
  destruct H1 as (ty1,(ty2,eqn)).
  unfold W_CASE, mkw_case.
  rewrite cond_set_ok; trivial.
  specialize cc_prod_elim with (1:=H0) (2:=ty1); clear H0; intro H0.
  rewrite El_int_prod in H0.
  apply eq_elim with (El
     (app (int (lift 2 P) (V.cons (w2 (int n i)) (V.cons (w1 (int n i)) i)))
        (mkw (w1 (int n i)) (w2 (int n i))))).
   apply El_morph.
   apply app_ext; auto with *.
   rewrite split_lift; do 2 rewrite int_cons_lift_eq; reflexivity.

   apply cc_prod_elim with (1:=H0).
   rewrite split_lift.
   rewrite El_int_arr.
   revert ty2; apply eq_elim.
   apply cc_arr_morph.
    reflexivity.

    rewrite int_cons_lift_eq.
    rewrite El_int_W; reflexivity.

 simpl in H6|-*.
 rewrite cc_bot_ax in H1; destruct H1.
  (* neutral case *)
  rewrite H1 in H6.
  unfold WCASE.
  eapply prodSAT_elim;[|apply H5].
  unfold RW in H6; rewrite rWi_neutral in H6; auto with *.
  apply neuSAT_def; trivial.

  (* regular case *)
  eapply Real_WCASE with (6:=H1) (7:=H6)
    (C:=fun x => Real (app (int P i) x) (mkw_case (fun x f => app (app (int G i) x) f) x));
     auto with *.
  do 2 red; intros.
   unfold mkw_case.
   rewrite H8.
   reflexivity.

   revert H5; apply piSAT0_morph; intros.
    red; intros; reflexivity.

    reflexivity.

    specialize cc_prod_elim with (1:=H0) (2:=H8); clear H0; intro H0.
    rewrite El_int_prod in H0.
    rewrite Real_int_prod; trivial.
    apply piSAT0_morph; intros.
     red; intros.
     rewrite split_lift.
     rewrite El_int_arr.
     apply in_set_morph; auto with *.
     apply cc_arr_morph.
      reflexivity.

      rewrite int_cons_lift_eq.
      rewrite El_int_W; reflexivity.

     rewrite split_lift.
     rewrite Real_int_arr; trivial.
      apply piSAT0_morph; intros.
       red; intros.
       reflexivity.

       reflexivity.

       specialize cc_arr_elim with (1:=H9) (2:=H11); clear H9; intro H9.
       rewrite int_cons_lift_eq.
       rewrite Real_int_W; trivial.
       reflexivity.

      revert H10; apply eq_elim.
      rewrite split_lift.
      rewrite El_int_arr; reflexivity.

     apply Real_morph.
      simpl.
      rewrite split_lift; do 2 rewrite int_cons_lift_eq.
      reflexivity.

      unfold mkw_case; rewrite cond_set_ok.
       rewrite w1_eq, w2_eq; reflexivity.
       rewrite w1_eq, w2_eq; reflexivity.
Qed.
(*Print Assumptions typ_Wcase.*)

Lemma typ_Wcase' : forall P O G n T,
  T <> kind ->
  typ e O (Ordt o) ->
  sub_typ e (App P n) T ->
  typ e G (Prod A (Prod (Prod B (lift 2 (WI O))) (App (lift 2 P) (Wc (Ref 1) (Ref 0))))) ->
  typ e n (WI (OSucc O)) ->
  typ e (Wcase G n) T.
intros.
apply typ_subsumption with (App P n); auto.
2:discriminate.
apply typ_Wcase with O; trivial.
Qed.

End Wtypes_typing.
Hint Resolve WF_mono.

Lemma typ_WI_type n eps e A B O :
  isOrd eps ->
  zero ∈ eps ->
  A <> kind ->
  typ e O (Ordt eps) ->
  typ e A (type n) ->
  typ (A::e) B (type n) ->
  typ e (WI A B O) (type n).
red; intros epso eps_nz Ank tyO tyA tyB i j is_val; simpl.
destruct tyord_inv with (3:=tyO)(4:=is_val) as (oo,(_,osn)); trivial.
clear tyO.
red in tyA; specialize tyA with (1:=is_val).
apply in_int_not_kind in tyA.
2:discriminate.
destruct tyA as (Aty,Asn).
red in Aty.
change (int (type n) i) with (sn_sort (ecc (S n))) in Aty.
apply El_in_grot in Aty; auto.
split;[discriminate|].
assert (G_B : forall a, a ∈ El (int A i) -> El (int B (V.cons a i)) ∈ ecc (S n)).
 intros.
 assert (val_ok (A::e) (V.cons a i) (I.cons daimon j)).
  apply vcons_add_var_daimon; trivial.
 apply tyB in H0.
 destruct H0; trivial.
 destruct H1; trivial.
 red in H1; change (int (type n) (V.cons a i)) with (sn_sort (ecc (S n))) in H1.
 apply El_in_grot in H1; trivial.
apply and_split; intros.
 red; change (int (type n) i) with (sn_sort (ecc (S n))).
 simpl int.
 apply sn_sort_intro.
  intros.
  apply RW_morph; auto with *.

  apply G_incl with (TI (WF A B i) (W_ord (El(int A i)) (fun x => El(int B (V.cons x i))))); trivial.
   apply G_TI; trivial.
    apply WF_morph; auto with *.

    apply W_ord_ord.
    do 2 red; intros.
    rewrite H; reflexivity.

    apply G_W_ord; auto.
    do 2 red; intros.
    rewrite H; reflexivity.

    intros.
    apply G_W_F; auto.
    do 2 red; intros.
    rewrite H0; reflexivity.

   apply W_stages; auto.
   do 2 red; intros.
   rewrite H; reflexivity.

 red in H.
 destruct (tyB _ _ (val_ok_cons_default is_val Ank)) as (Bnk,(_,snB)).
 change (int (type n) i) with (sn_sort (ecc (S n))).
 rewrite Real_sort_sn; trivial.
 apply sat_sn in Asn.
 apply sat_sn in snB.
 rewrite tm_subst_cons in snB.
 apply Lc.sn_subst in snB.
 simpl.
 apply snSAT_intro.
 apply Lc.sn_K2; trivial.
 apply Lc.sn_K2; trivial.
 apply Lc.sn_abs; trivial.
Qed.

(*****************************************************************************)
(** Recursor (without case analysis) *)

(* WFix O M is a fixpoint of domain WI O with body M *)
Definition WFix (O M:term) : term.
(*begin show*)
left.
exists (fun i => WREC (fun o' f => int M (V.cons f (V.cons o' i))) (int O i))
       (fun j => WFIX (Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j))))).
(*end show*)
 do 2 red; intros.
 apply WREC_morph.
  do 2 red; intros.
  apply int_morph; auto with *.
  apply V.cons_morph; trivial.
  apply V.cons_morph; trivial.

  apply int_morph; auto with *.
 (* *)
 do 2 red; intros.
 rewrite H; reflexivity.

 (* *)
 red; intros.
 replace (Lc.lift_rec 1
     (WFIX (Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j))))) k) with
   (WFIX (Lc.lift_rec 1 (Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j)))) k)).
  simpl.
  f_equal.
  f_equal.
  rewrite <- tm_liftable.
  apply tm_morph; auto with *.
  rewrite <- Lc.ilift_binder_lift.
  apply Lc.ilift_morph.
  intros [|k']; simpl; trivial.
  apply tm_liftable.

  generalize  (Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j)))); intro.
  unfold WFIX, FIXP; simpl.
  rewrite <- Lc.permute_lift.
  reflexivity.

 (* *)
 red; intros.
 replace (Lc.subst_rec u
     (WFIX (Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j))))) k) with
   (WFIX (Lc.subst_rec u (Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j)))) k)).
  simpl.
  f_equal.
  f_equal.
  rewrite <- tm_substitutive.
  apply tm_morph; auto with *.
  rewrite <- Lc.ilift_binder.
  apply Lc.ilift_morph.
  intros [|k']; simpl; trivial.
  apply tm_substitutive.

  generalize  (Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j)))); intro.
  unfold WFIX, FIXP; simpl.
  rewrite <- Lc.commut_lift_subst.
  reflexivity.
Defined.

(** Typing rules of WFix *)

Section WFixRules.

  Variable infty : set.
  Hypothesis infty_ord : isOrd infty.
  Hypothesis infty_nz : zero ∈ infty.
  Variable E : fenv.
  Let e := tenv E.
  Variable A B O U M : term.
  Hypothesis A_nk : A <> kind.
  Hypothesis Aeq : fx_equals E A.
  Hypothesis Beq : fx_equals (push_var E A) B.

  Definition WIL n := WI (lift n A) (lift_rec n 1 B).

  Hypothesis ty_O : typ e O (Ordt infty).
  Hypothesis ty_M : typ (Prod (WIL 1 (Ref 0)) U::OSucct O::e)
    M (Prod (WIL 2 (OSucc (Ref 1)))
         (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U)))).

  Hypothesis stab : fx_extends
    (push_fun (push_ord E (OSucct O)) (WIL 1 (Ref 0)) U)
    (WIL 2 (OSucc (Ref 1)))
    M.

  Let Wi i o := cc_bot (TI (WF A B i) o).
  Let F i := fun o' f => squash (int M (V.cons f (V.cons o' i))).
  Let U' i := fun o' x => El (int U (V.cons x (V.cons o' i))).
  Notation F' i := (fun o' f => int M (V.cons f (V.cons o' i))).

  Local Instance U'morph : forall i, morph2 (U' i).
do 3 red; intros; unfold U'.
rewrite H; rewrite H0; reflexivity.
Qed.
  Instance morph_fix_body : forall i, morph2 (F i).
unfold F; do 3 red; intros.
apply squash_morph.
rewrite H; rewrite H0; reflexivity.
Qed.
  Lemma ext_fun_ty : forall o i,
    ext_fun (Wi i o) (U' i o).
do 2 red; intros.
rewrite H0;reflexivity.
Qed.
  Hint Resolve U'morph morph_fix_body ext_fun_ty.

  Hypothesis fx_sub_U :
    fx_sub (push_var (push_ord E (OSucct O)) (WIL 1 (OSucc (Ref 0)))) U.

Lemma El_int_W_lift O' n i :
  El (int (WIL n O') i) == cc_bot (TI (WF A B (V.shift n i)) (int O' i)).
unfold WIL; rewrite El_int_W.
apply cc_bot_morph.
apply TI_morph_gen; auto with *.
red; intros.
unfold WF; apply W_F_ext; auto with *.
 rewrite int_lift_eq; reflexivity.

 red; intros.
 rewrite int_lift_rec_eq.
 rewrite <- V.cons_lams.
 2:apply V.shift_morph; trivial.
 rewrite V.lams0.
 rewrite H1; reflexivity.
(*
 rewrite H; reflexivity.*)
Qed.

Lemma Real_int_W_lift O' n i x :
  x ∈ cc_bot (TI (WF A B (V.shift n i)) (int O' i)) ->
  eqSAT (Real (int (WIL n O') i) x) (RW A B (V.shift n i) (int O' i) x).
intros.
unfold WIL; rewrite Real_int_W.
 unfold RW.
 apply rWi_morph_gen; auto with *.
  rewrite int_lift_eq; reflexivity.

  red; intros.
  rewrite int_lift_rec_eq.
  rewrite <- V.cons_lams.
  2:apply V.shift_morph; trivial.
  rewrite V.lams0.
  rewrite H0; reflexivity.

  red; intros.
  rewrite H0; rewrite int_lift_eq; reflexivity.

  do 2 red; intros.
  rewrite H1; rewrite int_lift_rec_eq.
  rewrite <- V.cons_lams.
  2:apply V.shift_morph; trivial.
  rewrite V.lams0.
  rewrite H0; reflexivity.

 revert H; apply eq_elim.
 apply cc_bot_morph.
 apply TI_morph_gen; auto with *.
 red; intros.
 unfold WF; apply W_F_ext.
  rewrite int_lift_eq; reflexivity.

  red; intros.
  rewrite H1; rewrite int_lift_rec_eq.
  rewrite <- V.cons_lams.
  2:apply V.shift_morph; trivial.
  rewrite V.lams0.
  reflexivity.

  (*apply cc_bot_morph;*) trivial.
Qed.

Lemma Elt_int_W_lift O' n i :
  Elt (int (WIL n O') i) == TI (WF A B (V.shift n i)) (int O' i).
simpl; rewrite Elt_def.
apply TI_morph_gen; auto with *.
red; intros.
unfold WF; apply W_F_ext; auto with *.
 rewrite int_lift_eq; reflexivity.

 red; intros.
 rewrite int_lift_rec_eq.
 rewrite <- V.cons_lams.
 2:apply V.shift_morph; trivial.
 rewrite V.lams0.
 rewrite H1; reflexivity.

(* rewrite H; reflexivity.*)
Qed.

  Lemma val_mono_1 i i' j j' y y' f g:
    val_mono E i j i' j' ->
    isOrd (int O i) ->
    isOrd (int O i') ->
    int O i ⊆ int O i' ->
    isOrd y ->
    isOrd y' ->
    y ⊆ int O i ->
    y' ⊆ int O i' ->
    y ⊆ y' ->
    f ∈ cc_prod (Wi i y) (U' i y) ->
    g ∈ cc_prod (Wi i' y') (U' i' y') ->
    fcompat (Wi i y) f g ->
    val_mono (push_fun (push_ord E (OSucct O)) (WIL 1 (Ref 0)) U)
      (V.cons f (V.cons y i)) (I.cons daimon (I.cons daimon j))
      (V.cons g (V.cons y' i')) (I.cons daimon (I.cons daimon j')).
intros is_val Oo Oo' oo' yo y'o yO y'O yy' fty gty eqfg.
apply val_push_fun.
 apply val_push_ord; auto.
 3:discriminate.
  split;[|apply varSAT].
  red; rewrite El_int_osucc.
  apply ole_lts; trivial.

  split;[|apply varSAT].
  red; rewrite El_int_osucc.
  apply ole_lts; trivial.

 split;[|apply varSAT].
 red; rewrite El_int_prod.
 revert fty; apply eq_elim; apply cc_prod_ext; intros.
  rewrite El_int_W_lift; reflexivity.

  apply ext_fun_ty.

 split;[|apply varSAT].
 red; rewrite El_int_prod.
 revert gty; apply eq_elim; apply cc_prod_ext; intros.
  rewrite El_int_W_lift; reflexivity.

  apply ext_fun_ty.

 rewrite El_int_W_lift.
 trivial.
Qed.

  Lemma val_mono_2 i j y y' n n':
    val_ok e i j ->
    isOrd (int O i) ->
    isOrd y ->
    isOrd y' ->
    y ⊆ y' ->
    y' ⊆ int O i ->
    n ∈ Wi i y ->
    n == n' ->
    val_mono (push_var (push_ord E (OSucct O)) (WIL 1 (OSucc (Ref 0))))
      (V.cons n (V.cons y i)) (I.cons daimon (I.cons daimon j))
      (V.cons n' (V.cons y' i)) (I.cons daimon (I.cons daimon j)).
Proof.
intros.
apply val_push_var; auto with *.
 4:discriminate.
 apply val_push_ord; auto with *.
  4:discriminate.
  apply val_mono_refl; trivial.

  split;[|apply varSAT].
  red; rewrite El_int_osucc.
  apply ole_lts; auto.
  transitivity y'; trivial.

  split;[|apply varSAT].
  red; rewrite El_int_osucc.
  apply ole_lts; auto.

 split;[|apply varSAT].
 red; rewrite El_int_W_lift.
 revert H5; apply cc_bot_mono.
 apply TI_incl; simpl; auto.

 split;[|apply varSAT].
 red; rewrite El_int_W_lift.
 rewrite <- H6.
 revert H5; apply cc_bot_mono.
 apply TI_incl; simpl; auto.
 apply ole_lts; trivial.
Qed.

Let F2m : forall i T, morph2 (fun o' f => int T (V.cons f (V.cons o' i))).
do 3 red; intros.
apply int_morph; [reflexivity|].
repeat apply V.cons_morph; trivial.
reflexivity.
Qed.
Let U2m : forall i T, morph2 (fun o' f => El (int T (V.cons f (V.cons o' i)))).
do 3 red; intros.
apply El_morph; apply F2m; trivial.
Qed.
Set Implicit Arguments.

Let Mty : forall i j,
 val_ok e i j ->
 forall o',
 o' ∈ osucc (int O i) ->
 forall f,
 f ∈ cc_prod (Wi i o') (U' i o') ->
 int M (V.cons f (V.cons o' i)) ∈ cc_prod (Wi i (osucc o')) (U' i (osucc o')).
intros.
assert (val_ok (Prod (WIL 1 (Ref 0)) U :: OSucct O :: e)
          (V.cons f (V.cons o' i)) (I.cons daimon (I.cons daimon j))).
 apply vcons_add_var_daimon; [| |discriminate].
  apply vcons_add_var_daimon; [trivial| |discriminate].
  red; simpl; rewrite El_def; auto.

  red; rewrite El_int_prod.
  revert H1; apply eq_elim; apply cc_prod_ext.
   rewrite El_int_W_lift; reflexivity.

   apply ext_fun_ty.
apply ty_M in H2.
apply in_int_not_kind in H2.
2:discriminate.
destruct H2 as (H2,_).
red in H2; rewrite El_int_prod in H2.
revert H2; apply eq_elim; apply cc_prod_ext.
 rewrite El_int_W_lift; reflexivity.

 red; intros.
 rewrite int_lift_rec_eq.
 rewrite int_subst_rec_eq.
 rewrite int_lift_rec_eq.
 apply El_morph; apply int_morph; auto with *.
 intros [|[|k]].
  compute; trivial.
  simpl; reflexivity.
  compute; fold minus.
  replace (k-0) with k; auto with *.
Qed.

Let Mirr : forall i j,
 val_ok e i j ->
 forall o' o'' f g,
 isOrd o' ->
 o' ⊆ o'' ->
 o'' ∈ osucc (int O i) ->
 f ∈ cc_prod (Wi i o') (U' i o') ->
 g ∈ cc_prod (Wi i o'') (U' i o'') ->
 fcompat (Wi i o') f g ->
 fcompat (Wi i (osucc o')) (int M (V.cons f (V.cons o' i))) (int M (V.cons g (V.cons o'' i))).
intros.
assert (Oo: isOrd (int O i)).
 destruct tyord_inv with (3:=ty_O)(4:=H); trivial.
assert (o'' ⊆ int O i).
 apply olts_le in H2; trivial.
assert (val_mono (push_fun (push_ord E (OSucct O)) (WIL 1 (Ref 0)) U)
         (V.cons f (V.cons o' i)) (I.cons daimon (I.cons daimon j))
         (V.cons g (V.cons o'' i)) (I.cons daimon (I.cons daimon j))).
 apply val_mono_1; auto with *.
  apply val_mono_refl; trivial.

  eauto using isOrd_inv.

  transitivity o''; auto.
apply stab in H7.
rewrite El_int_W_lift in H7; trivial.
Qed.

Let Usub : forall i j,
 val_ok e i j ->
 forall o' o'' x,
 isOrd o' ->
 o' ⊆ o'' ->
 o'' ∈ osucc (int O i) ->
 x ∈ Wi i o' ->
 U' i o' x ⊆ U' i o'' x.
intros.
assert (Oo: isOrd (int O i)).
 destruct tyord_inv with (3:=ty_O)(4:=H); trivial.
assert (o'' ⊆ int O i).
 apply olts_le in H2; trivial.
eapply El_sub with (1:=fx_sub_U).
apply val_mono_2; auto with *.
 apply val_mono_refl; eexact H.

 eauto using isOrd_inv.
Qed.

Lemma WREC_ok i j :
  val_ok e i j ->
  WREC_assumptions
    (El (int A i)) (fun x => El (int B (V.cons x i))) (int O i) (F' i) (U' i).
intros valok.
destruct tyord_inv with (3:=ty_O)(4:=valok); trivial.
split; auto with *.
 apply Bw_morph; reflexivity.

 unfold U'; auto.

 apply (Mty valok).

 apply (Mirr valok).

 apply (Usub valok).
Qed.

Lemma int_Prod_intro0 dom F0 f t :
  morph1 F0 ->
  f ∈ (Π x ∈ El dom, El(F0 x)) ->
  (forall x u, [x,u] \real dom ->
   app f x ∈ El (F0 x) ->
   inSAT (Lc.App t u) (Real (F0 x) (app f x))) ->
  [f,t] \real prod dom F0.
split.
 red; rewrite El_prod; trivial.
 do 2 red; intros; apply H; trivial.

 rewrite Real_prod; auto.
  apply piSAT0_intro'; intros.
   apply H1; auto.
   apply cc_prod_elim with (1:=H0); trivial.

   exists empty; auto.

  rewrite El_prod; trivial.
  do 2 red; intros; apply H; trivial.
Qed.

Lemma int_Prod_intro A0 B0 f t i :
  f ∈ (Π x ∈ El(int A0 i), El(int B0 (V.cons x i))) ->
  (forall x u, [x,u] \real (int A0 i) ->
   app f x ∈ El(int B0 (V.cons x i)) ->
   inSAT (Lc.App t u) (Real (int B0 (V.cons x i)) (app f x))) ->
  [f,t] \real int (Prod A0 B0) i.
intros.
apply int_Prod_intro0; trivial.
do 2 red; intros.
rewrite H1; reflexivity.
Qed.

Lemma typ_wfix :
  typ e (WFix O M) (Prod (WI A B O) (subst_rec O 1 U)).
red; intros.
destruct tyord_inv with (3:=ty_O)(4:=H); trivial.
apply in_int_intro.
discriminate.
discriminate.
apply and_split; intros.
 red; rewrite El_int_prod.
 eapply eq_elim.
 2:simpl.
 2:apply WREC_typ with (1:=WREC_ok H); auto with *.
 apply cc_prod_ext.
  rewrite El_int_W.
  reflexivity.

  red; intros.
  rewrite int_subst_rec_eq.
  rewrite <- V.cons_lams.
  2:apply V.cons_morph; reflexivity.
  rewrite V.lams0.
  rewrite H3; reflexivity.

(**)
simpl.
rewrite Real_prod; auto with *.
2:intros ? ? ? h; rewrite h; reflexivity.
unfold piSAT.
eapply inSAT_morph;[reflexivity| |].
2:apply WREC_sat with (6:=WREC_ok H)
 (RA:=Real(int A i))(RB:=fun x =>Real(int B(V.cons x i)))
 (RF:= Lc.Abs (tm M (Lc.ilift (I.cons (tm O j) j))))
 (RU:= fun o w => Real (int U (V.cons w (V.cons o i)))); auto with *.
 apply piSAT0_morph.
  red; intros.
  rewrite El_def.
  reflexivity.

  intros.
  rewrite Real_def; trivial.
   reflexivity.

   intros.
   apply RW_morph; auto with *.

  intros.
  rewrite int_subst_rec_eq.
  apply Real_morph; auto with *.
  rewrite <- V.cons_lams; auto with *.
   rewrite V.lams0; reflexivity.

   apply V.cons_morph.
   reflexivity.

 reflexivity.

 apply Bwi_morph.

 apply RAwi_morph.

 apply RBwi_morph.

 do 4 red; intros; apply Real_morph; auto with *.
 apply int_morph; auto with *.
 repeat apply V.cons_morph; auto with *.

 (**)
 red; intros.
 apply fx_sub_U with (V.cons x (V.cons o' i))
     (I.cons daimon (I.cons daimon j)) (I.cons daimon (I.cons daimon j)).
  apply val_mono_2; auto with *.
  unfold Wi; auto.

  split.
   rewrite <- H9; trivial.
   rewrite <- H9; trivial.

 (**)
 intros.
 apply inSAT_exp;[right;apply sat_sn in H6;trivial|].
  replace (Lc.subst u (tm M (Lc.ilift (I.cons (tm O j) j)))) with
     (tm M (I.cons u (I.cons (tm O j) j))).
  2:unfold Lc.subst; rewrite <- tm_substitutive.
  2:apply tm_morph; auto with *.
  2:intros [|[|k]]; unfold Lc.ilift,I.cons; simpl.
  2:rewrite Lc.lift0; reflexivity.
  2:rewrite Lc.simpl_subst; trivial.
  2:rewrite Lc.lift0; trivial.
  2:rewrite Lc.simpl_subst; trivial.
  2:rewrite Lc.lift0; trivial.
  assert (val_ok (Prod (WIL 1 (Ref 0)) U::OSucct O::e)
            (V.cons f (V.cons o' i)) (I.cons u (I.cons (tm O j) j))).
   apply vcons_add_var.
    apply vcons_add_var; trivial.
     split; simpl.
      red; rewrite El_def.
      apply ole_lts in H4; auto.

      rewrite Real_def; auto.
       apply snSAT_intro; apply H1.
       reflexivity.
       apply ole_lts in H4; auto.

     discriminate.

    apply int_Prod_intro.
     revert H5; apply eq_set_ax.
     apply cc_prod_ext.
      rewrite El_int_W_lift; auto with *.
      reflexivity.

      red; intros.
      unfold U'.
      rewrite H7; reflexivity.

     intros.
     destruct H7.
     red in H7; rewrite El_int_W_lift in H7.
     rewrite Real_int_W_lift in H9; trivial.
     apply piSAT0_elim' in H6.
     apply H6; trivial.

    discriminate.

 assert (ty_M' := ty_M _ _ H7).
 apply in_int_not_kind in ty_M'.
 2:discriminate.
 destruct ty_M'.
 red in H8; rewrite El_int_prod in H8.
 rewrite Real_int_prod in H9; trivial.
 revert H9; apply piSAT0_morph.
  red; intros.
  rewrite El_int_W_lift; auto.

  intros.
  rewrite Real_int_W_lift; auto.
  reflexivity.

  intros.
  apply Real_morph; auto with *.
  rewrite int_lift_rec_eq.
  rewrite int_subst_rec_eq.
  rewrite int_lift_rec_eq.
  apply int_morph; auto with *.
  intros [|[|k]]; try reflexivity.
  unfold V.cons, V.lams,V.shift; simpl.
  replace (k-0) with k; auto with *.
Qed.

(** Fixpoint equation holds only when applied to a constructor,
    because of the realizability part of the interpretation.
 *)
Lemma wfix_eq : forall X G,
  let N := Wc X G in
  typ e N (WI A B O) ->
  eq_typ e (App (WFix O M) N)
           (App (subst O (subst (lift 1 (WFix O M)) M)) N).
intros X G N tyN.
red; intros.
unfold eqX.
change
 (app (WREC (F' i) (int O i)) (int N i) ==
  app (int (subst O (subst (lift 1 (WFix O M)) M)) i) (int N i)).
do 2 rewrite <- int_subst_eq.
rewrite int_cons_lift_eq.
red in tyN; specialize tyN with (1:=H).
apply in_int_not_kind in tyN.
2:discriminate.
destruct tyN.
red in H0; rewrite El_int_W in H0.
rewrite cc_bot_ax in H0; destruct H0.
 simpl in H0.
 symmetry in H0; apply discr_mt_mkw in H0; contradiction.
destruct tyord_inv with (3:=ty_O)(4:=H); trivial.
apply WREC_eqn with (1:=WREC_ok H); auto with *.
Qed.

Lemma TIeq: forall i i' j j' o',
  val_mono E i j i' j' ->
  isOrd o' ->
  TI (WF A B i) o' == TI (WF A B i') o'.
intros; apply TI_morph_gen; auto with *.
red; intros.
apply W_F_ext; trivial.
 apply El_morph.
 apply (Aeq _ _ _ _ H).

 red; intros.
 apply El_morph.
 eapply Beq.
 apply val_push_var with (1:=H); trivial.
  split;[trivial|apply varSAT].
  rewrite (Aeq _ _ _ _ H) in H2.
  rewrite H3 in H2.
  split;[trivial|apply varSAT].
Qed.

(*
Lemma WREC_weak A0 B0 o o' F0 U0 :
  isOrd o ->
  isOrd o' ->
  o ⊆ o' ->
  WREC_assumptions A0 B0 o' F0 U0 ->
  WREC_assumptions A0 B0 o F0 U0.
intros.
assert (forall z, z ∈ osucc o -> z ∈ osucc o').
 intros.
 apply ole_lts.
  apply isOrd_inv with (osucc o); auto.
 apply olts_le in H3.
 transitivity o; trivial.
destruct H2; split; intros; auto.
Qed.
*)

Lemma wfix_extend :
  fx_subval E O ->
  fx_extends E (WI A B O) (WFix O M).
intro subO.
do 2 red; intros.
rewrite El_int_W in H0.
simpl.
assert (isval := proj1 H).
assert (isval' := proj1 (proj2 H)).
assert (oo: isOrd (int O i)).
 destruct tyord_inv with (3:=ty_O) (4:=isval); trivial.
assert (oo': isOrd (int O i')).
 destruct tyord_inv with (3:=ty_O) (4:=isval'); trivial.
assert (inclo: int O i ⊆ int O i').
 apply subO in H; trivial.
clear subO.
assert (aeq : El (int A i) == El (int A i')).
 apply El_morph.
 apply Aeq with (1:=H); trivial.
eapply WREC_ext with (6:=WREC_ok isval) (7:=WREC_ok isval'); trivial.
 red; intros.
 apply El_morph.
 eapply Beq.
 apply val_push_var with (1:=H); trivial.
  split;[trivial|apply varSAT].

  split;[trivial|apply varSAT].
  red; rewrite <- H2, <-aeq; trivial.

 red; intros.
 do 2 red in stab; eapply stab.
  apply val_mono_1 with (1:=H); auto with *.
   transitivity (int O i); trivial.

 rewrite El_int_W_lift.
 simpl; auto.
Qed.

Lemma wfix_equals :
  fx_equals E O ->
  fx_equals E (WFix O M).
red; intros.
assert (isval := proj1 H0).
assert (isval' := proj1 (proj2 H0)).
destruct tyord_inv with (3:=ty_O) (4:=proj1 H0) as (Oo,_); trivial.
assert (fxs: fx_subval E O).
 apply fx_equals_subval; trivial.
red in H; specialize H with (1:=H0).
apply wfix_extend in fxs.
red in fxs.
specialize fxs with (1:=H0).
apply fcompat_typ_eq with (3:=fxs).
 rewrite El_int_W.
 eapply cc_prod_is_cc_fun.
 apply WREC_typ with (1:=WREC_ok isval); auto with *.

 rewrite El_int_W.
 rewrite TIeq with (1:=H0); trivial.
 rewrite H in Oo|-*.
 eapply cc_prod_is_cc_fun.
 apply WREC_typ with (1:=WREC_ok isval'); auto with *.
Qed.

End WFixRules.

Lemma typ_wfix' : forall infty e A B O U M T,
       T <> kind ->
       isOrd infty ->
       zero ∈ infty ->
       A <> kind ->
       typ e O (Ordt infty) ->
       typ (Prod (WIL A B 1 (Ref 0)) U :: OSucct O :: e) M
         (Prod (WIL A B 2 (OSucc (Ref 1)))
         (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U)))) ->
       fx_extends (push_fun (push_ord (tinj e) (OSucct O)) (WIL A B 1 (Ref 0)) U)
         (WIL A B 2 (OSucc (Ref 1))) M ->
       fx_sub (push_var (push_ord (tinj e) (OSucct O)) (WIL A B 1 (OSucc (Ref 0)))) U ->
       sub_typ e (Prod (WI A B O) (subst_rec O 1 U)) T ->
       typ e (WFix O M) T.
intros.
apply typ_subsumption with (Prod (WI A B O) (subst_rec O 1 U)); auto.
2:discriminate.
change e with (tenv (tinj e)).
apply typ_wfix with (infty:=infty); trivial.
Qed.

(** Variance results *)

  Lemma Wi_sub : forall e o A B O,
    isOrd o ->
    zero ∈ o ->
    A <> kind ->
    typ (tenv e) O (Ordt o) ->
    fx_equals e A ->
    fx_equals (push_var e A) B ->
    fx_subval e O ->
    fx_sub e (WI A B O).
unfold fx_sub, fx_subval.
intros e o A B O oo oz Ank tyO eqA eqB subO i i' j j' val_m x t (xreal,xsat).
assert (RBm : Proper (eq_set ==> eq_set ==> eqSAT)
          (fun a b => Real (int B (V.cons a i)) b)).
 do 3 red; intros.
 rewrite H,H0; reflexivity.
destruct tyord_inv with (3:=tyO) (4:=proj1 val_m); trivial.
destruct tyord_inv with (3:=tyO) (4:=proj1 (proj2 val_m)); trivial.
assert (eqiA := eqA); red in eqiA; specialize eqiA with (1:=val_m).
specialize subO with (1:=val_m).
red in xreal; rewrite El_int_W in xreal.
rewrite Real_int_W in xsat; trivial.
assert (cc_bot (TI (WF A B i) (int O i)) ⊆ cc_bot (TI (WF A B i') (int O i'))).
 apply cc_bot_mono.
 transitivity (TI (WF A B i') (int O i)).
  apply eq_incl.
  apply TIeq with (4:=val_m); trivial.

(*  intro; apply eq_elim.
  apply TI_morph_gen; auto with *.
  red; intros.
  apply W_F_ext; auto with *.
  red; intros.
  apply El_morph.
  apply eqB with (I.cons daimon j) (I.cons daimon j').
   apply val_push_var; auto with *.
    split; [trivial|apply varSAT].
   rewrite H5 in H4.
   rewrite eqA in H4.
   split; [trivial|apply varSAT].

(*   apply cc_bot_morph; trivial.*)
*)
  destruct H0; destruct H2.
  apply TI_mono; trivial.
   apply WF_morph; auto with *.

 rewrite Real_int_W; auto.
 split.
  apply H3 in xreal.
  rewrite <- El_int_W in xreal; auto.
 rewrite cc_bot_ax in xreal; destruct xreal as [H4|xreal].
  assert (eqSAT (RW A B i (int O i) x) (RW A B i (int O i) empty)).
   unfold RW; apply rWi_morph; auto with *.
    do 2 red; intros.
    rewrite H5; reflexivity.
    do 2 red; intros.
    rewrite H5; reflexivity.
  rewrite H5 in xsat.
  apply neuSAT_def.
  unfold RW in xsat; rewrite rWi_neutral in xsat; auto with *.
   apply Bw_morph; reflexivity.
   apply RAw_morph; reflexivity.

 setoid_replace (RW A B i' (int O i') x) with (RW A B i (int O i) x); trivial.
 symmetry; transitivity (RW A B i (int O i') x).
  unfold RW; apply rWi_mono; trivial.
   apply Bw_morph; reflexivity.
   apply RAw_morph; reflexivity.

  unfold RW; apply rWi_ext; trivial; intros.
   do 2 red; intros.
   rewrite H4; reflexivity.

   apply El_morph; trivial.

   red; intros.
   eapply El_eq with (1:=eqB).
   apply val_push_var; eauto.
    split;[trivial|apply varSAT].
    split;[rewrite eqiA in H4;rewrite H5 in H4;exact H4|apply varSAT].

   do 2 red; intros.
   rewrite <- eqiA; rewrite H4; reflexivity.

   do 2 red; intros.
   apply Real_morph; trivial.
   eapply eqB.
   apply val_push_var; eauto.
    split;[trivial|apply varSAT].
    split;[rewrite eqiA in H4;rewrite H5 in H4;trivial|apply varSAT].

  reflexivity.
  reflexivity.
Qed.

  Lemma Wi_fx_sub : forall e o A B O,
    isOrd o ->
    zero ∈ o ->
    typ_impl e A kind ->
    typ_impl (push_var e A) B kind ->
    typ_monoval e O (Ordt o) ->
    fx_sub e (WI A B O).
intros.
red; intros.
destruct H1.
red in H6; specialize H6 with (1:=proj1 H4).
destruct H6 as (?,_).
destruct H2.
destruct H3.
revert i i' j j' H4 x t H5.
change (fx_sub e (WI A B O)).
apply Wi_sub with (o:=o); trivial.
Qed.

Lemma typ_wfix'' : forall infty e A B O U M T,
       isOrd infty ->
       zero ∈ infty ->
       T <> kind ->
       sub_typ (tenv e) (Prod (WI A B O) (subst_rec O 1 U)) T ->
       typ (tenv e) O (Ordt infty) ->
       typ_mono (push_var (push_ord e (OSucct O)) (WI (lift 1 A) (lift_rec 1 1 B) (OSucc (Ref 0)))) U ->
       typ_ext (push_fun (push_ord e (OSucct O)) (WI (lift 1 A) (lift_rec 1 1 B) (Ref 0)) U)
         M (WI (lift 2 A) (lift_rec 2 1 B) (OSucc (Ref 1)))
           (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
       typ (tenv e) (WFix O M) T.
intros.
destruct H4; destruct H5.
apply typ_subsumption with (2:=H2); trivial.
2:discriminate.
apply typ_wfix with infty; trivial.
Qed.

  Lemma typ_ext_fix : forall eps e A B O U M,
    isOrd eps ->
    zero ∈ eps ->
    typ_impl e A kind ->
    typ_impl (push_var e A) B kind ->
    typ_monoval e O (Ordt eps) ->
    typ_ext (push_fun (push_ord e (OSucct O)) (WI (lift 1 A) (lift_rec 1 1 B) (Ref 0)) U) M
      (WI (lift 2 A) (lift_rec 2 1 B) (OSucc (Ref 1)))
      (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
    fx_sub (push_var (push_ord e (OSucct O)) (WI (lift 1 A) (lift_rec 1 1 B) (OSucc (Ref 0)))) U ->
    typ_ext e (WFix O M) (WI A B O) (subst_rec O 1 U).
intros eps e A B O U M eps_ord eps_nz tyA tyB tyO tyM tyU.
destruct tyO as (inclO,tyO).
destruct tyM as (extM,tyM).
assert (tyF: typ (tenv e) (WFix O M) (Prod (WI A B O) (subst_rec O 1 U))).
 apply typ_wfix with eps; trivial.
split; trivial.
red; intros.
generalize i i' j j' H; change (fx_extends e (WI A B O) (WFix O M)).
destruct tyA as (eqA,tyA).
destruct (tyA _ _ (proj1 H)) as (Ank,_).
destruct tyB as (eqB,_).
apply wfix_extend with eps U; trivial.
Qed.

  Lemma typ_impl_fix : forall eps e A B O U M,
    isOrd eps ->
    zero ∈ eps ->
    typ_impl e A kind ->
    typ_impl (push_var e A) B kind ->
    typ_impl e O (Ordt eps) ->
    typ_ext (push_fun (push_ord e (OSucct O)) (WI (lift 1 A) (lift_rec 1 1 B) (Ref 0)) U) M
      (WI (lift 2 A) (lift_rec 2 1 B) (OSucc (Ref 1)))
      (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
    fx_sub (push_var (push_ord e (OSucct O)) (WI (lift 1 A) (lift_rec 1 1 B) (OSucc (Ref 0)))) U ->
    typ_impl e (WFix O M) (Prod (WI A B O) (subst_rec O 1 U)).
intros eps e A B O U M eps_ord eps_nz (eqA,tyA) (eqB,_) (inclO,tyO) (extM,tyM) tyU.
assert (tyF: typ (tenv e) (WFix O M) (Prod (WI A B O) (subst_rec O 1 U))).
 apply typ_wfix with eps; trivial.
split; trivial.
red; intros.
generalize i i' j j' H; change (fx_equals e (WFix O M)).
destruct (tyA _ _ (proj1 H)) as (Ank,_).
apply wfix_equals with eps A B U; trivial.
Qed.

End Make.

(** * Instantiation of the abstract model construction with ZFind_wbot. *)

(** ZFind_wbot is an instance of the above signature *)
Require ZFind_wbot.
Module W_Model : W_PartialModel.
  Import ZFind_wbot.

  Definition mkw := couple.
  Definition mkw_morph := couple_morph.
  Definition w1 := fst.
  Definition w1_morph := fst_morph.
  Definition w2 := snd.
  Definition w2_morph := snd_morph.
  Definition w1_eq := fst_def.
  Definition w2_eq := snd_def.
  Definition discr_mt_mkw := fun x f => discr_mt_pair (singl x) (pair x f).

  Definition W_F := W_F'.
  Definition W_F_mono := W_F'_mono.
  Definition W_F_ext :=
    fun A A' B B' X X' eqA eqB eqX =>
    W_F_ext A A' B B' (cc_bot X) (cc_bot X') eqA eqB (cc_bot_morph _ _ eqX).
(*  Definition W_F_elim A B Bm X := W_F_elim A B Bm (cc_bot X).*)
  Lemma W_F_elim A B :
    morph1 B ->
    forall X x,
    x ∈ W_F A B X ->
    w1 x ∈ A /\ w2 x ∈ (Π _ ∈ B (w1 x), cc_bot X) /\ x == mkw (w1 x) (w2 x).
intros Bm X x tyx.
destruct sigma_elim with (2:=tyx) as (eqx,(ty1,ty2)); auto.
Qed.
  Lemma W_F_intro A B :
    morph1 B ->
    forall X x f,
    x ∈ A ->
    f ∈ (Π i ∈ B x, cc_bot X) ->
    couple x f ∈ W_F A B X.
intros Bm X x f tyx tyf.
apply couple_intro_sigma; trivial.
do 2 red; intros.
rewrite H0; reflexivity.
Qed.

  Lemma W_F_def : forall A B X,
    W_F A B X == Σ x ∈ A, Π i ∈ B x, cc_bot X.
  reflexivity.
  Qed.
  Definition W_ord := W_ord'.
  Definition W_fix := W_fix'.
(*  Definition mt_not_in_W_F := mt_not_in_W_F'.
  Definition W_stages := W_stages'.*)
  Lemma W_ord_ord : forall A B, morph1 B ->
    isOrd (W_ord A B).
intros A B Bm.
unfold W_ord.
unfold ZFind_wbot.W_ord'.
apply Ffix_o_o.
 apply Wf_mono'; trivial.

 apply Wf_typ'; trivial.
Qed.
  Definition G_W_ord := G_W_ord'.
  Definition G_W_F := G_W_F'.

  Definition WREC := WREC'.
  Lemma WREC_morph : Proper ((eq_set==>eq_set==>eq_set)==>eq_set==>eq_set) WREC.
do 3 red; intros.
apply TR_morph; trivial.
do 2 red; intros.
apply sup_morph; trivial.
red; intros.
apply squash_morph.
apply H; auto with *.
Qed.

  Set Implicit Arguments.
  Record WREC_assumptions A B O M U : Prop := WREC_intro {
    WBm : morph1 B;
    Wo : isOrd O;
    WMm : morph2 M;
    WUm : morph2 U;
    WU_mt : forall o x, empty ∈ U o x;
    WMtyp : forall o,
        o ∈ osucc O ->
        forall f,
        f ∈ (Π x ∈ cc_bot (TI (W_F A B) o), U o x) ->
        M o f
        ∈ (Π x ∈ cc_bot (TI (W_F A B) (osucc o)), U (osucc o) x);
    WMirr : forall o o' f g,
        isOrd o ->
        o ⊆ o' ->
        o' ∈ osucc O ->
        f ∈ (Π x ∈ cc_bot (TI (W_F A B) o), U o x) ->
        g ∈ (Π x ∈ cc_bot (TI (W_F A B) o'), U o' x) ->
        fcompat (cc_bot (TI (W_F A B) o)) f g ->
        fcompat (cc_bot (TI (W_F A B) (osucc o))) (M o f) (M o' g);
    WUmono : forall o o' x,
        isOrd o ->
        o ⊆ o' ->
        o' ∈ osucc O ->
        x ∈ cc_bot (TI (W_F A B) o) ->
        U o x ⊆ U o' x
  }.

  Definition WREC_typ A B O M U (h:WREC_assumptions A B O M U) :=
    WREC'_typ A B (WBm h) O (Wo h) M (WMm h) U
      (WUm h) (WU_mt h) (WMtyp h) (WMirr h) (WUmono h).
(*  Definition WREC_eqn A B O M U (h:WREC_assumptions A B O M U) :=
    WREC'_eqn A B (WBm h) O (Wo h) M (WMm h) U
      (WUm h) (WU_mt h) (WMtyp h) (WMirr h) (WUmono h).*)
  Definition WREC_irr A B O M U (h:WREC_assumptions A B O M U) :=
    WREC'_irr A B (WBm h) O (Wo h) M (WMm h) U
      (WUm h) (WU_mt h) (WMtyp h) (WMirr h) (WUmono h).
  Definition WREC_unfold A B O M U (h:WREC_assumptions A B O M U) :=
    WREC'_unfold A B (WBm h) O (Wo h) M (WMm h) U
      (WUm h) (WU_mt h) (WMtyp h) (WMirr h) (WUmono h).
  Definition WREC_strict A B O M U (h:WREC_assumptions A B O M U) :=
    WREC'_strict A B (WBm h) O (Wo h) M (WMm h) U
      (WUm h) (WU_mt h) (WMtyp h) (WMirr h) (WUmono h).

End W_Model.

(** All that remains to do is apply the functor... *)
Module SN_W := Make(W_Model).
Export SN_W.
Print Assumptions typ_wfix.

author: barras

repo: cic-model

save_path: github-repos/coq/barras-cic-model


text:
From Coq Require Import ssreflect.
From stdpp Require Import base gmap.
From iris.proofmode Require Import tactics.
From aneris.aneris_lang.lib Require Import list_proof.
From aneris.aneris_lang.lib.serialization Require Import serialization_proof.
From aneris.aneris_lang Require Import aneris_lifting proofmode.
From aneris.examples.crdt.spec Require Import crdt_base crdt_time crdt_events crdt_denot crdt_resources.
From aneris.examples.crdt.oplib Require Import oplib_code.
From aneris.examples.crdt.oplib.spec Require Import model spec.
From aneris.examples.crdt.oplib.examples.gcounter Require Import gcounter_code.

(** A positive-negative counter *)
Section GCounterCrdt.

  Inductive CtrOp :=
  | Incr (n : nat) : CtrOp. (* note we can add a negative number *)

  Definition ctr_payload (op : CtrOp) : nat :=
    match op with
    | Incr n => n
    end.

  Global Instance ctr_op_eqdecision : EqDecision CtrOp.
  Proof. solve_decision. Qed.

  Global Instance ctr_op_countable : Countable CtrOp.
  Proof.
    refine {|
      encode op := match op with Incr n => encode n end;
      decode n := Incr <$> @decode nat _ _ n;
    |}.
    intros []. rewrite decode_encode /=. done.
  Qed.

  Definition CtrSt := nat.
  Context `{!Log_Time}.

  (* The value of a counter is just the sum of the operations' payloads. *)
  Fixpoint ctr_value (s : list (Event CtrOp)) : nat :=
    match s with
    | [] => 0%nat
    | ev :: xs => (ctr_payload ev.(EV_Op) + ctr_value xs)%nat
    end.

  Definition ctr_denot (s : gset (Event CtrOp)) (st : CtrSt) : Prop :=
    st = ctr_value (elements s).

  Global Instance ctr_denot_fun : Rel2__Fun ctr_denot.
  Proof.
    constructor; unfold ctr_denot; intros; subst; done.
  Qed.

  Global Instance ctr_denot_instance : CrdtDenot CtrOp CtrSt := {
    crdt_denot := ctr_denot;
  }.
End GCounterCrdt.

Section OpGCounter.

  Context `{!Log_Time}.

  Definition op_ctr_effect st (ev : Event CtrOp) st' :=
    st' = (st + ctr_payload ev.(EV_Op))%nat.

  Lemma op_ctr_effect_fun st : Rel2__Fun (op_ctr_effect st).
  Proof.
    constructor. unfold op_ctr_effect.
    intros a b b' Hb Hb'.
    destruct (EV_Op a) as [z]; simpl in *; subst; auto.
  Qed.

  Lemma ctr_value_singleton ev :
    ctr_value [ev] = ctr_payload (ev.(EV_Op)).
  Proof.
    unfold ctr_value. lia.
  Qed.

  Lemma ctr_value_cons ev l :
    ctr_value (ev :: l) = (ctr_payload ev.(EV_Op) + ctr_value l)%nat.
  Proof.
    simpl. auto.
  Qed.

  Lemma ctr_value_app (l l' : list (Event CtrOp)) :
    ctr_value (l ++ l') = (ctr_value l + ctr_value l')%nat.
  Proof.
    generalize dependent l'.
    induction l as [ | h t Ht]; intros l'; [done |].
    rewrite -app_comm_cons.
    do 2 rewrite ctr_value_cons.
    rewrite (Ht l'). lia.
  Qed.

  Lemma ctr_value_perm (l l' : list (Event CtrOp)) :
    Permutation l l' -> ctr_value l = ctr_value l'.
  Proof.
    generalize dependent l'.
    induction l as [ | h t Ht]; intros l' Hperm.
    - apply Permutation_nil in Hperm; subst; reflexivity.
    - rewrite ctr_value_cons.
      apply Permutation_sym in Hperm.
      pose proof Hperm as Hperm'.
      apply Permutation_vs_cons_inv in Hperm as [l1 [l2 ->]].
      apply Permutation_sym, Permutation_cons_app_inv, Ht in Hperm'.
      rewrite Hperm'.
      do 2 rewrite ctr_value_app.
      rewrite ctr_value_cons.
      lia.
  Qed.

  Lemma ctr_denot_union (s : gset (Event CtrOp)) (ev : Event CtrOp) (res : CtrSt) :
    ⟦ s ⟧ ⇝ res ->
    ev ∉ s ->
    ⟦ s ∪ {[ ev ]} ⟧ ⇝ (res + ctr_payload ev.(EV_Op))%nat.
  Proof.
    simpl. unfold ctr_denot.
    intros -> Hnotin.
    assert (s ## {[ ev ]}) as Hdisj by set_solver.
    pose proof (elements_disj_union s
                                    ({[ev]} : gset (Event CtrOp))
                                    Hdisj) as Hperm.
    apply ctr_value_perm in Hperm. rewrite Hperm.
    by rewrite elements_singleton ctr_value_app ctr_value_singleton.
  Qed.

  Instance op_ctr_effect_coh : OpCrdtEffectCoh op_ctr_effect.
  Proof.
    intros s e st st'.
    intros Hdenot Hnotin. split.
    - intros Heff.
      unfold op_ctr_effect in Heff; subst.
      by apply ctr_denot_union.
    - intros Hdenot'.
      unfold op_ctr_effect.
      pose proof (ctr_denot_union s e st Hdenot Hnotin) as Hunion.
      pose proof (rel2_fun Hdenot' Hunion) as Hequiv.
      apply leibniz_equiv in Hequiv; subst; done.
  Qed.

  Definition op_ctr_init_st := 0%nat.

  Lemma op_ctr_init_st_coh : ⟦ (∅ : gset (Event CtrOp)) ⟧ ⇝ op_ctr_init_st.
  Proof. done. Qed.

  Global Instance op_ctr_model_instance : OpCrdtModel CtrOp CtrSt := {
    op_crdtM_effect := op_ctr_effect;
    op_crdtM_effect_fun := op_ctr_effect_fun;
    op_crdtM_effect_coh := op_ctr_effect_coh;
    op_crdtM_init_st := op_ctr_init_st;
    op_crdtM_init_st_coh := op_ctr_init_st_coh
  }.

End OpGCounter.

From aneris.examples.crdt.oplib.proof Require Import time.

Section GCounter_proof.
  Context `{!anerisG M Σ}.

  Context `{!CRDT_Params, !OpLib_Res CtrOp}.

  Definition Ctr_OpLib_Op_Coh := λ (op : CtrOp) v, match op with Incr z => v = #z end.

  Lemma Ctr_OpLib_Op_Coh_Inj (o1 o2 : CtrOp) (v : val) :
    Ctr_OpLib_Op_Coh o1 v → Ctr_OpLib_Op_Coh o2 v → o1 = o2.
  Proof. destruct o1; destruct o2; simpl; intros ? ?; simplify_eq; done. Qed.

  Lemma Ctr_OpLib_Coh_Ser (op : CtrOp) (v : val) :
    Ctr_OpLib_Op_Coh op v → Serializable int_serialization v.
  Proof.
    destruct op; rewrite /Ctr_OpLib_Op_Coh; intros ?; simplify_eq; apply _.
  Qed.

  Definition Ctr_OpLib_State_Coh := λ (st : CtrSt) v, v = #st.

  Global Instance Ctr_OpLib_Params : OpLib_Params CtrOp CtrSt :=
  {|
    OpLib_Serialization := int_serialization;
    OpLib_State_Coh := Ctr_OpLib_State_Coh;
    OpLib_Op_Coh := Ctr_OpLib_Op_Coh;
    OpLib_Op_Coh_Inj := Ctr_OpLib_Op_Coh_Inj;
    OpLib_Coh_Ser := Ctr_OpLib_Coh_Ser
  |}.

  Lemma Ctr_init_st_fn_spec : ⊢ init_st_fn_spec init_st.
  Proof.
    iIntros (addr).
    iIntros "!#" (Φ) "_ HΦ".
    rewrite /init_st.
    wp_pures.
    iApply "HΦ"; done.
  Qed.

  Lemma Ctr_effect_spec : ⊢ effect_spec effect.
  Proof.
    iIntros (addr ev st s log_ev log_st).
    iIntros "!#" (Φ) "(%Hev & %Hst & %Hs & %Hevs) HΦ".
    rewrite /effect.
    destruct log_ev as [[op] orig vc].
    destruct Hev as (evpl&evvc&evorig&?&Hevpl&?&?).
    rewrite /OpLib_State_Coh /= /Ctr_OpLib_State_Coh in Hst.
    simplify_eq/=.
    rewrite /OpLib_State_Coh /= /Ctr_OpLib_State_Coh.
    do 14 wp_pure _.
    wp_apply assert_proof.wp_assert.
    wp_op.
    rewrite bool_decide_eq_true_2; last lia.
    iSplit; first done.
    iNext.
    wp_pures.
    replace (log_st + op)%Z with ((log_st + op)%nat : Z) by lia.
    iApply "HΦ"; eauto.
  Qed.

  Lemma Ctr_crdt_fun_spec : ⊢ crdt_fun_spec counter_crdt.
  Proof.
    iIntros (addr).
    iIntros "!#" (Φ) "_ HΦ".
    rewrite /counter_crdt.
    wp_pures.
    iApply "HΦ".
    iExists _, _; iSplit; first done.
    iSplit; [iApply Ctr_init_st_fn_spec|iApply Ctr_effect_spec].
  Qed.

  Lemma Ctr_init_spec :
    init_spec (oplib_init
               (s_ser (s_serializer OpLib_Serialization))
               (s_deser (s_serializer OpLib_Serialization))) -∗
    init_spec_for_specific_crdt counter_init.
  Proof.
    iIntros "#Hinit" (repId addr addrs_val).
    iIntros (Φ) "!# (%Haddrs & %Hrepid & Hprotos & Hskt & Hfr & Htoken) HΦ".
    rewrite /counter_init.
    wp_pures.
    wp_apply ("Hinit" with "[$Hprotos $Htoken $Hskt $Hfr]").
    { do 2 (iSplit; first done). iApply Ctr_crdt_fun_spec; done. }
    iIntros (get update) "(HLS & #Hget & #Hupdate)".
    wp_pures.
    iApply "HΦ"; eauto.
  Qed.

End GCounter_proof.

author: logsem

repo: aneris

save_path: github-repos/coq/logsem-aneris


text:
From cap_machine Require Import rules_base.
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac.

Section cap_lang_rules.
  Context `{memG Σ, regG Σ, MonRef: MonRefG (leibnizO _) CapR_rtc Σ}.
  Context `{MachineParameters}.
  Implicit Types P Q : iProp Σ.
  Implicit Types σ : ExecConf.
  Implicit Types c : cap_lang.expr.
  Implicit Types a b : Addr.
  Implicit Types r : RegName.
  Implicit Types v : cap_lang.val.
  Implicit Types w : Word.
  Implicit Types reg : gmap RegName Word.
  Implicit Types ms : gmap Addr Word.

  (* TODO: move to stdpp *)
  Tactic Notation "destruct_or" ident(H) :=
  match type of H with
  | _ ∨ _ => destruct H as [H|H]
  | Is_true (_ || _) => apply orb_True in H; destruct H as [H|H]
  end.
  Tactic Notation "destruct_or" "?" ident(H) := repeat (destruct_or H).
  Tactic Notation "destruct_or" "!" ident(H) := hnf in H; destruct_or H; destruct_or? H.

  Definition denote (i: instr) (c: Cap): Z :=
    match c with
    | (p, g, b, e, a) =>
      match i with
      | GetP _ _ => encodePerm p
      | GetL _ _ => encodeLoc g
      | GetB _ _ => b
      | GetE _ _ => e
      | GetA _ _ => a
      | _ => 0%Z
      end
    end.

  Global Arguments denote : simpl nomatch.

  Definition is_Get (i: instr) (dst src: RegName) :=
    i = GetP dst src ∨
    i = GetL dst src ∨
    i = GetB dst src ∨
    i = GetE dst src ∨
    i = GetA dst src.

  Lemma regs_of_is_Get i dst src :
    is_Get i dst src →
    regs_of i = {[ dst; src ]}.
  Proof.
    intros HH. destruct_or! HH; subst i; reflexivity.
  Qed.

  Inductive Get_failure (i: instr) (regs: Reg) (dst src: RegName) :=
    | Get_fail_src_noncap : forall n,
        regs !! src = Some (inl n) →
        Get_failure i regs dst src
    | Get_fail_overflow_PC : forall (c:Cap),
        regs !! src = Some (inr c) →
        incrementPC (<[ dst := inl (denote i c) ]> regs) = None →
        Get_failure i regs dst src.

  Inductive Get_spec (i: instr) (regs: Reg) (dst src: RegName) (regs': Reg): cap_lang.val -> Prop :=
  | Get_spec_success (c: Cap):
      regs !! src = Some (inr c) →
      incrementPC (<[ dst := inl (denote i c) ]> regs) = Some regs' →
      Get_spec i regs dst src regs' NextIV
  | Get_spec_failure:
      Get_failure i regs dst src →
      Get_spec i regs dst src regs' FailedV.

  Lemma wp_Get Ep pc_p pc_g pc_b pc_e pc_a pc_p' w get_i dst src regs :
    decodeInstrW w = get_i →
    is_Get get_i dst src →

    PermFlows pc_p pc_p' →
    isCorrectPC (inr ((pc_p, pc_g), pc_b, pc_e, pc_a)) →
    regs !! PC = Some (inr ((pc_p, pc_g), pc_b, pc_e, pc_a)) →
    regs_of get_i ⊆ dom _ regs →
    {{{ ▷ pc_a ↦ₐ[pc_p'] w ∗
        ▷ [∗ map] k↦y ∈ regs, k ↦ᵣ y }}}
      Instr Executable @ Ep
    {{{ regs' retv, RET retv;
        ⌜ Get_spec (decodeInstrW w) regs dst src regs' retv ⌝ ∗
        pc_a ↦ₐ[pc_p'] w ∗
        [∗ map] k↦y ∈ regs', k ↦ᵣ y }}}.
  Proof.
    iIntros (Hdecode Hinstr Hfl Hvpc HPC Dregs φ) "(>Hpc_a & >Hmap) Hφ".
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1 l1 l2 n) "Hσ1 /=". destruct σ1; simpl.
    iDestruct "Hσ1" as "[Hr Hm]".
    assert (pc_p' ≠ O).
    { destruct pc_p'; auto. destruct pc_p; inversion Hfl. inversion Hvpc; subst; naive_solver. }
    iPoseProof (gen_heap_valid_inclSepM with "Hr Hmap") as "#H".
    iDestruct "H" as %Hregs.
    have HPC' := regs_lookup_eq _ _ _ HPC.
    have ? := lookup_weaken _ _ _ _ HPC Hregs.
    iDestruct (@gen_heap_valid_cap with "Hm Hpc_a") as %Hpc_a; auto.
    iModIntro. iSplitR. by iPureIntro; apply normal_always_head_reducible.
    iNext. iIntros (e2 σ2 efs Hpstep).
    apply prim_step_exec_inv in Hpstep as (-> & -> & (c & -> & Hstep)).
    iSplitR; auto. eapply step_exec_inv in Hstep; eauto.

    specialize (indom_regs_incl _ _ _ Dregs Hregs) as Hri.
    erewrite regs_of_is_Get in Hri; eauto.
    destruct (Hri src) as [wsrc [H'src Hsrc]]. by set_solver+.
    destruct (Hri dst) as [wdst [H'dst Hdst]]. by set_solver+.
    destruct wsrc as [| (([[p g] b] & e) & a) ] eqn:Hwsrc.
    { (* Failure: src is not a capability *)
      assert (c = Failed ∧ σ2 = (r, m)) as (-> & ->).
      { destruct_or! Hinstr; rewrite Hinstr in Hstep; cbn in Hstep.
        all: rewrite /RegLocate Hsrc in Hstep; inversion Hstep; auto. }
      iFailWP "Hφ" Get_fail_src_noncap. }

    assert ((c, σ2) = updatePC (update_reg (r, m) dst (inl (denote get_i (p,g,b,e,a))))) as HH.
    { destruct_or! Hinstr; rewrite Hinstr /= in Hstep |- *; auto; cbn in Hstep.
      all: destruct b, e, a; rewrite /RegLocate /update_reg Hsrc /= in Hstep |-*; auto. }
    clear Hstep. rewrite /update_reg /= in HH.

    destruct (incrementPC (<[ dst := inl (denote get_i (p, g, b, e, a)) ]> regs))
      as [regs'|] eqn:Hregs'; pose proof Hregs' as H'regs'; cycle 1.
    { (* Failure: incrementing PC overflows *)
      apply incrementPC_fail_updatePC with (m:=m) in Hregs'.
      eapply updatePC_fail_incl with (m':=m) in Hregs'.
      2: by apply lookup_insert_is_Some'; eauto.
      2: by apply insert_mono; eauto.
      rewrite Hdecode. clear Hdecode. simplify_pair_eq.
      iMod ((gen_heap_update_inSepM _ _ dst) with "Hr Hmap") as "[Hr Hmap]"; eauto.
      iFailWP "Hφ" Get_fail_overflow_PC. }

    (* Success *)

    eapply (incrementPC_success_updatePC _ m) in Hregs'
        as (p' & g' & b' & e' & a'' & a_pc' & HPC'' & Ha_pc' & HuPC & ->).
    eapply updatePC_success_incl with (m':=m) in HuPC. 2: by eapply insert_mono; eauto.
    simplify_pair_eq. iFrame.
    iMod ((gen_heap_update_inSepM _ _ dst) with "Hr Hmap") as "[Hr Hmap]"; eauto.
    iMod ((gen_heap_update_inSepM _ _ PC) with "Hr Hmap") as "[Hr Hmap]"; eauto.
    iFrame. iModIntro. iApply "Hφ". iFrame. iPureIntro. econstructor; eauto.
  Qed.

  Lemma wp_Get_PC_success E get_i dst pc_p pc_g pc_b pc_e pc_a w wdst pc_a' pc_p' :
    decodeInstrW w = get_i →
    is_Get get_i dst PC →
    PermFlows pc_p pc_p' → isCorrectPC (inr ((pc_p,pc_g),pc_b,pc_e,pc_a)) →
    (pc_a + 1)%a = Some pc_a' ->
    dst <> PC ->

    {{{ ▷ PC ↦ᵣ inr ((pc_p,pc_g),pc_b,pc_e,pc_a)
        ∗ ▷ pc_a ↦ₐ[pc_p'] w
        ∗ ▷ dst ↦ᵣ wdst }}}
      Instr Executable @ E
      {{{ RET NextIV;
          PC ↦ᵣ inr ((pc_p,pc_g),pc_b,pc_e,pc_a')
          ∗ pc_a ↦ₐ[pc_p'] w
          ∗ dst ↦ᵣ inl (denote get_i (pc_p, pc_g, pc_b, pc_e, pc_a)) }}}.
  Proof.
    iIntros (Hdecode Hinstr Hfl Hvpc Hpca' HnePC φ) "(>HPC & >Hpc_a & >Hdst) Hφ".
    iDestruct (map_of_regs_2 with "HPC Hdst") as "[Hmap %]".
    iApply (wp_Get with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto.
    by erewrite regs_of_is_Get; eauto; rewrite !dom_insert; set_solver+.
    iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.

    destruct Hspec as [| * Hfail].
    { (* Success *)
      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
      rewrite insert_commute // insert_insert insert_commute // insert_insert.
      iDestruct (regs_of_map_2 with "Hmap") as "[? ?]"; eauto; iFrame. }
    { (* Failure (contradiction) *)
      destruct Hfail; try incrementPC_inv; simplify_map_eq; eauto. congruence. }
  Qed.

  Lemma wp_Get_same_success E get_i r pc_p pc_g pc_b pc_e pc_a w (c:Cap) pc_a' pc_p' :
    decodeInstrW w = get_i →
    is_Get get_i r r →
    PermFlows pc_p pc_p' → isCorrectPC (inr ((pc_p,pc_g),pc_b,pc_e,pc_a)) →
    (pc_a + 1)%a = Some pc_a' ->
    r <> PC ->

    {{{ ▷ PC ↦ᵣ inr ((pc_p,pc_g),pc_b,pc_e,pc_a)
        ∗ ▷ pc_a ↦ₐ[pc_p'] w
        ∗ ▷ r ↦ᵣ inr c }}}
      Instr Executable @ E
      {{{ RET NextIV;
          PC ↦ᵣ inr ((pc_p,pc_g),pc_b,pc_e,pc_a')
          ∗ pc_a ↦ₐ[pc_p'] w
          ∗ r ↦ᵣ inl (denote get_i c) }}}.
  Proof.
    iIntros (Hdecode Hinstr Hfl Hvpc Hpca' HnePC φ) "(>HPC & >Hpc_a & >Hr) Hφ".
    iDestruct (map_of_regs_2 with "HPC Hr") as "[Hmap %]".
    iApply (wp_Get with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto.
    by erewrite regs_of_is_Get; eauto; rewrite !dom_insert; set_solver+.
    iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.

    destruct Hspec as [| * Hfail].
    { (* Success *)
      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
      rewrite insert_commute // insert_insert insert_commute // insert_insert.
      iDestruct (regs_of_map_2 with "Hmap") as "[? ?]"; eauto; iFrame. }
    { (* Failure (contradiction) *)
      destruct Hfail; try incrementPC_inv; simplify_map_eq; eauto. congruence. }
  Qed.

  Lemma wp_Get_success E get_i dst src pc_p pc_g pc_b pc_e pc_a w wdst csrc pc_a' pc_p' :
    decodeInstrW w = get_i →
    is_Get get_i dst src →
    PermFlows pc_p pc_p' → isCorrectPC (inr ((pc_p,pc_g),pc_b,pc_e,pc_a)) →
    (pc_a + 1)%a = Some pc_a' ->
    dst <> PC -> src <> PC ->

    {{{ ▷ PC ↦ᵣ inr ((pc_p,pc_g),pc_b,pc_e,pc_a)
        ∗ ▷ pc_a ↦ₐ[pc_p'] w
        ∗ ▷ src ↦ᵣ inr csrc
        ∗ ▷ dst ↦ᵣ wdst }}}
      Instr Executable @ E
      {{{ RET NextIV;
          PC ↦ᵣ inr ((pc_p,pc_g),pc_b,pc_e,pc_a')
          ∗ pc_a ↦ₐ[pc_p'] w
          ∗ src ↦ᵣ inr csrc
          ∗ dst ↦ᵣ inl (denote get_i csrc) }}}.
  Proof.
    iIntros (Hdecode Hinstr Hfl Hvpc Hpca' Hdst Hsrc φ) "(>HPC & >Hpc_a & >Hsrc & >Hdst) Hφ".
    iDestruct (map_of_regs_3 with "HPC Hdst Hsrc") as "[Hmap (%&%&%)]".
    iApply (wp_Get with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto.
    by erewrite regs_of_is_Get; eauto; rewrite !dom_insert; set_solver+.
    iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.

    destruct Hspec as [| * Hfail].
    { (* Success *)
      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
      rewrite insert_commute // insert_insert (insert_commute _ PC dst) // insert_insert.
      iDestruct (regs_of_map_3 with "Hmap") as "(?&?&?)"; eauto; iFrame. }
    { (* Failure (contradiction) *)
      destruct Hfail; try incrementPC_inv; simplify_map_eq; eauto. congruence. }
  Qed.

End cap_lang_rules.

(* Hints to automate proofs of is_Get *)

Lemma is_Get_GetP dst src : is_Get (GetP dst src) dst src.
Proof. intros; unfold is_Get; eauto. Qed.
Lemma is_Get_GetL dst src : is_Get (GetL dst src) dst src.
Proof. intros; unfold is_Get; eauto. Qed.
Lemma is_Get_GetB dst src : is_Get (GetB dst src) dst src.
Proof. intros; unfold is_Get; eauto. Qed.
Lemma is_Get_GetE dst src : is_Get (GetE dst src) dst src.
Proof. intros; unfold is_Get; eauto. Qed.
Lemma is_Get_GetA dst src : is_Get (GetA dst src) dst src.
Proof. intros; unfold is_Get; eauto. Qed.

Global Hint Resolve is_Get_GetP : core.
Global Hint Resolve is_Get_GetL : core.
Global Hint Resolve is_Get_GetB : core.
Global Hint Resolve is_Get_GetE : core.
Global Hint Resolve is_Get_GetA : core.

repo: cerise-stack

save_path: github-repos/coq/logsem-cerise-stack


(* Copyright 2012-2015 by Adam Petcher.				*
 * Use of this source code is governed by the license described	*
 * in the LICENSE file at the root of the source tree.		*)

Set Implicit Arguments.

Require Import fcf.Crypto.
Require Import fcf.RndNat.
Require Import fcf.NotationV1.

Definition Bernoulli(r : Rat) : Comp bool :=
  match r with
    | RatIntro n d =>
      v <-$ RndNat d; ret (if (lt_dec v n) then true else false)
  end.

Theorem Bernoulli_correct :
  forall (r : Rat),
    r <= 1 ->
    Pr[Bernoulli r] == r.

  unfold Bernoulli.
  intuition.
  destruct r.

  rewrite RndNat_seq.

  rewrite (sumList_filter_partition (fun z => if (lt_dec z n) then true else false)).
  eapply eqRat_trans.
  eapply ratMult_eqRat_compat.
  eapply eqRat_refl.
  eapply ratAdd_eqRat_compat.

  eapply sumList_all.
  intros.
  destruct ( lt_dec a n).
  simpl.
  destruct ( EqDec_dec bool_EqDec true true).
  eapply eqRat_refl.
  intuition.
  apply filter_In in H0.
  intuition.
  exfalso.
  destruct (lt_dec a n); intuition.

  eapply sumList_0.
  intros.
  apply filter_In in H0.
  intuition.
  destruct (lt_dec a n); simpl in *.
  discriminate.
  destruct (EqDec_dec bool_EqDec false true); intuition.

  rewrite allNatsLt_filter_lt.
  rewrite <- ratAdd_0_r.
  rewrite ratMult_1_r.
  rewrite allNatsLt_length.
  rewrite <- ratMult_num_den.
  eapply eqRat_terms.
  omega.
  unfold posnatMult, posnatToNat, natToPosnat.
  destruct p.
  omega.

  eapply rat_le_1_if; trivial.

Qed.

Theorem Bernoulli_wf :
  forall r,
    well_formed_comp (Bernoulli r).

  intuition.
  unfold Bernoulli.
  destruct r.
  wftac.

Qed.

Theorem Bernoulli_correct_complement :
  forall (r : Rat),
    r <= 1 ->
    evalDist (Bernoulli r) false ==
    ratSubtract 1 r.

  intuition.
  eapply eqRat_trans.
  eapply evalDist_complement.
  eapply Bernoulli_wf.
  eapply ratSubtract_eqRat_compat; intuition.
  eapply Bernoulli_correct.
  trivial.
Qed.


text:
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

Require Import Sumbool.
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis1.
Open Local Scope R_scope.

Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
  match N with
    | O => x
    | S n =>
      let down := Dichotomy_lb x y P n in
        let up := Dichotomy_ub x y P n in
          let z := (down + up) / 2 in if P z then down else z
  end

  with Dichotomy_ub (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
    match N with
      | O => y
      | S n =>
        let down := Dichotomy_lb x y P n in
          let up := Dichotomy_ub x y P n in
            let z := (down + up) / 2 in if P z then z else up
    end.

Definition dicho_lb (x y:R) (P:R -> bool) (N:nat) : R := Dichotomy_lb x y P N.
Definition dicho_up (x y:R) (P:R -> bool) (N:nat) : R := Dichotomy_ub x y P N.

(**********)
Lemma dicho_comp :
  forall (x y:R) (P:R -> bool) (n:nat),
    x <= y -> dicho_lb x y P n <= dicho_up x y P n.
Proof.
  intros.
  induction  n as [| n Hrecn].
  simpl in |- *; assumption.
  simpl in |- *.
  case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
  unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
  prove_sup0.
  pattern 2 at 1 in |- *; rewrite Rmult_comm.
  rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
  rewrite Rmult_1_r.
  rewrite double.
  apply Rplus_le_compat_l.
  assumption.
  unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
  prove_sup0.
  rewrite Rmult_comm.
  rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
  rewrite Rmult_1_r.
  rewrite double.
  rewrite <- (Rplus_comm (Dichotomy_ub x y P n)).
  apply Rplus_le_compat_l.
  assumption.
Qed.

Lemma dicho_lb_growing :
  forall (x y:R) (P:R -> bool), x <= y -> Un_growing (dicho_lb x y P).
Proof.
  intros.
  unfold Un_growing in |- *.
  intro.
  simpl in |- *.
  case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
  right; reflexivity.
  unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
  prove_sup0.
  pattern 2 at 1 in |- *; rewrite Rmult_comm.
  rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
  rewrite Rmult_1_r.
  rewrite double.
  apply Rplus_le_compat_l.
  replace (Dichotomy_ub x y P n) with (dicho_up x y P n);
  [ apply dicho_comp; assumption | reflexivity ].
Qed.

Lemma dicho_up_decreasing :
  forall (x y:R) (P:R -> bool), x <= y -> Un_decreasing (dicho_up x y P).
Proof.
  intros.
  unfold Un_decreasing in |- *.
  intro.
  simpl in |- *.
  case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
  unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
  prove_sup0.
  rewrite Rmult_comm.
  rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
  rewrite Rmult_1_r.
  rewrite double.
  replace (Dichotomy_ub x y P n) with (dicho_up x y P n);
  [ idtac | reflexivity ].
  replace (Dichotomy_lb x y P n) with (dicho_lb x y P n);
  [ idtac | reflexivity ].
  rewrite <- (Rplus_comm (dicho_up x y P n)).
  apply Rplus_le_compat_l.
  apply dicho_comp; assumption.
  right; reflexivity.
Qed.

Lemma dicho_lb_maj_y :
  forall (x y:R) (P:R -> bool), x <= y -> forall n:nat, dicho_lb x y P n <= y.
Proof.
  intros.
  induction  n as [| n Hrecn].
  simpl in |- *; assumption.
  simpl in |- *.
  case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
  assumption.
  unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
  prove_sup0.
  rewrite Rmult_comm.
  rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ rewrite Rmult_1_r | discrR ].
  rewrite double; apply Rplus_le_compat.
  assumption.
  pattern y at 2 in |- *; replace y with (Dichotomy_ub x y P 0);
    [ idtac | reflexivity ].
  apply decreasing_prop.
  assert (H0 := dicho_up_decreasing x y P H).
  assumption.
  apply le_O_n.
Qed.

Lemma dicho_lb_maj :
  forall (x y:R) (P:R -> bool), x <= y -> has_ub (dicho_lb x y P).
Proof.
  intros.
  cut (forall n:nat, dicho_lb x y P n <= y).
  intro.
  unfold has_ub in |- *.
  unfold bound in |- *.
  exists y.
  unfold is_upper_bound in |- *.
  intros.
  elim H1; intros.
  rewrite H2; apply H0.
  apply dicho_lb_maj_y; assumption.
Qed.

Lemma dicho_up_min_x :
  forall (x y:R) (P:R -> bool), x <= y -> forall n:nat, x <= dicho_up x y P n.
Proof.
  intros.
  induction  n as [| n Hrecn].
  simpl in |- *; assumption.
  simpl in |- *.
  case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
  unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
  prove_sup0.
  pattern 2 at 1 in |- *; rewrite Rmult_comm.
  rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ rewrite Rmult_1_r | discrR ].
  rewrite double; apply Rplus_le_compat.
  pattern x at 1 in |- *; replace x with (Dichotomy_lb x y P 0);
    [ idtac | reflexivity ].
  apply tech9.
  assert (H0 := dicho_lb_growing x y P H).
  assumption.
  apply le_O_n.
  assumption.
  assumption.
Qed.

Lemma dicho_up_min :
  forall (x y:R) (P:R -> bool), x <= y -> has_lb (dicho_up x y P).
Proof.
  intros.
  cut (forall n:nat, x <= dicho_up x y P n).
  intro.
  unfold has_lb in |- *.
  unfold bound in |- *.
  exists (- x).
  unfold is_upper_bound in |- *.
  intros.
  elim H1; intros.
  rewrite H2.
  unfold opp_seq in |- *.
  apply Ropp_le_contravar.
  apply H0.
  apply dicho_up_min_x; assumption.
Qed.

Lemma dicho_lb_cv :
  forall (x y:R) (P:R -> bool),
    x <= y -> { l:R | Un_cv (dicho_lb x y P) l }.
Proof.
  intros.
  apply growing_cv.
  apply dicho_lb_growing; assumption.
  apply dicho_lb_maj; assumption.
Qed.

Lemma dicho_up_cv :
  forall (x y:R) (P:R -> bool),
    x <= y -> { l:R | Un_cv (dicho_up x y P) l }.
Proof.
  intros.
  apply decreasing_cv.
  apply dicho_up_decreasing; assumption.
  apply dicho_up_min; assumption.
Qed.

Lemma dicho_lb_dicho_up :
  forall (x y:R) (P:R -> bool) (n:nat),
    x <= y -> dicho_up x y P n - dicho_lb x y P n = (y - x) / 2 ^ n.
Proof.
  intros.
  induction  n as [| n Hrecn].
  simpl in |- *.
  unfold Rdiv in |- *; rewrite Rinv_1; ring.
  simpl in |- *.
  case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
  unfold Rdiv in |- *.
  replace
  ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) * / 2 - Dichotomy_lb x y P n)
    with ((dicho_up x y P n - dicho_lb x y P n) / 2).
  unfold Rdiv in |- *; rewrite Hrecn.
  unfold Rdiv in |- *.
  rewrite Rinv_mult_distr.
  ring.
  discrR.
  apply pow_nonzero; discrR.
  pattern (Dichotomy_lb x y P n) at 2 in |- *;
    rewrite (double_var (Dichotomy_lb x y P n));
      unfold dicho_up, dicho_lb, Rminus, Rdiv in |- *; ring.
  replace
  (Dichotomy_ub x y P n - (Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)
    with ((dicho_up x y P n - dicho_lb x y P n) / 2).
  unfold Rdiv in |- *; rewrite Hrecn.
  unfold Rdiv in |- *.
  rewrite Rinv_mult_distr.
  ring.
  discrR.
  apply pow_nonzero; discrR.
  pattern (Dichotomy_ub x y P n) at 1 in |- *;
    rewrite (double_var (Dichotomy_ub x y P n));
      unfold dicho_up, dicho_lb, Rminus, Rdiv in |- *; ring.
Qed.

Definition pow_2_n (n:nat) := 2 ^ n.

Lemma pow_2_n_neq_R0 : forall n:nat, pow_2_n n <> 0.
Proof.
  intro.
  unfold pow_2_n in |- *.
  apply pow_nonzero.
  discrR.
Qed.

Lemma pow_2_n_growing : Un_growing pow_2_n.
Proof.
  unfold Un_growing in |- *.
  intro.
  replace (S n) with (n + 1)%nat;
  [ unfold pow_2_n in |- *; rewrite pow_add | ring ].
  pattern (2 ^ n) at 1 in |- *; rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l.
  left; apply pow_lt; prove_sup0.
  simpl in |- *.
  rewrite Rmult_1_r.
  pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
    apply Rlt_0_1.
Qed.

Lemma pow_2_n_infty : cv_infty pow_2_n.
Proof.
  cut (forall N:nat, INR N <= 2 ^ N).
  intros.
  unfold cv_infty in |- *.
  intro.
  case (total_order_T 0 M); intro.
  elim s; intro.
  set (N := up M).
  cut (0 <= N)%Z.
  intro.
  elim (IZN N H0); intros N0 H1.
  exists N0.
  intros.
  apply Rlt_le_trans with (INR N0).
  rewrite INR_IZR_INZ.
  rewrite <- H1.
  unfold N in |- *.
  assert (H3 := archimed M).
  elim H3; intros; assumption.
  apply Rle_trans with (pow_2_n N0).
  unfold pow_2_n in |- *; apply H.
  apply Rge_le.
  apply growing_prop.
  apply pow_2_n_growing.
  assumption.
  apply le_IZR.
  unfold N in |- *.
  simpl in |- *.
  assert (H0 := archimed M); elim H0; intros.
  left; apply Rlt_trans with M; assumption.
  exists 0%nat; intros.
  rewrite <- b.
  unfold pow_2_n in |- *; apply pow_lt; prove_sup0.
  exists 0%nat; intros.
  apply Rlt_trans with 0.
  assumption.
  unfold pow_2_n in |- *; apply pow_lt; prove_sup0.
  simple induction N.
  simpl in |- *.
  left; apply Rlt_0_1.
  intros.
  pattern (S n) at 2 in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ].
  rewrite S_INR; rewrite pow_add.
  simpl in |- *.
  rewrite Rmult_1_r.
  apply Rle_trans with (2 ^ n).
  rewrite <- (Rplus_comm 1).
  rewrite <- (Rmult_1_r (INR n)).
  apply (poly n 1).
  apply Rlt_0_1.
  pattern (2 ^ n) at 1 in |- *; rewrite <- Rplus_0_r.
  rewrite <- (Rmult_comm 2).
  rewrite double.
  apply Rplus_le_compat_l.
  left; apply pow_lt; prove_sup0.
Qed.

Lemma cv_dicho :
  forall (x y l1 l2:R) (P:R -> bool),
    x <= y ->
    Un_cv (dicho_lb x y P) l1 -> Un_cv (dicho_up x y P) l2 -> l1 = l2.
Proof.
  intros.
  assert (H2 := CV_minus _ _ _ _ H0 H1).
  cut (Un_cv (fun i:nat => dicho_lb x y P i - dicho_up x y P i) 0).
  intro.
  assert (H4 := UL_sequence _ _ _ H2 H3).
  symmetry  in |- *; apply Rminus_diag_uniq_sym; assumption.
  unfold Un_cv in |- *; unfold R_dist in |- *.
  intros.
  assert (H4 := cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty).
  case (total_order_T x y); intro.
  elim s; intro.
  unfold Un_cv in H4; unfold R_dist in H4.
  cut (0 < y - x).
  intro Hyp.
  cut (0 < eps / (y - x)).
  intro.
  elim (H4 (eps / (y - x)) H5); intros N H6.
  exists N; intros.
  replace (dicho_lb x y P n - dicho_up x y P n - 0) with
  (dicho_lb x y P n - dicho_up x y P n); [ idtac | ring ].
  rewrite <- Rabs_Ropp.
  rewrite Ropp_minus_distr'.
  rewrite dicho_lb_dicho_up.
  unfold Rdiv in |- *; rewrite Rabs_mult.
  rewrite (Rabs_right (y - x)).
  apply Rmult_lt_reg_l with (/ (y - x)).
  apply Rinv_0_lt_compat; assumption.
  rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
  rewrite Rmult_1_l.
  replace (/ 2 ^ n) with (/ 2 ^ n - 0);
  [ unfold pow_2_n, Rdiv in H6; rewrite <- (Rmult_comm eps); apply H6;
    assumption
    | ring ].
  red in |- *; intro; rewrite H8 in Hyp; elim (Rlt_irrefl _ Hyp).
  apply Rle_ge.
  apply Rplus_le_reg_l with x; rewrite Rplus_0_r.
  replace (x + (y - x)) with y; [ assumption | ring ].
  assumption.
  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; assumption ].
  apply Rplus_lt_reg_r with x; rewrite Rplus_0_r.
  replace (x + (y - x)) with y; [ assumption | ring ].
  exists 0%nat; intros.
  replace (dicho_lb x y P n - dicho_up x y P n - 0) with
  (dicho_lb x y P n - dicho_up x y P n); [ idtac | ring ].
  rewrite <- Rabs_Ropp.
  rewrite Ropp_minus_distr'.
  rewrite dicho_lb_dicho_up.
  rewrite b.
  unfold Rminus, Rdiv in |- *; rewrite Rplus_opp_r; rewrite Rmult_0_l;
    rewrite Rabs_R0; assumption.
  assumption.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
Qed.

Definition cond_positivity (x:R) : bool :=
  match Rle_dec 0 x with
    | left _ => true
    | right _ => false
  end.

(** Sequential caracterisation of continuity *)
Lemma continuity_seq :
  forall (f:R -> R) (Un:nat -> R) (l:R),
    continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
Proof.
  unfold continuity_pt, Un_cv in |- *; unfold continue_in in |- *.
  unfold limit1_in in |- *.
  unfold limit_in in |- *.
  unfold dist in |- *.
  simpl in |- *.
  unfold R_dist in |- *.
  intros.
  elim (H eps H1); intros alp H2.
  elim H2; intros.
  elim (H0 alp H3); intros N H5.
  exists N; intros.
  case (Req_dec (Un n) l); intro.
  rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
    assumption.
  apply H4.
  split.
  unfold D_x, no_cond in |- *.
  split.
  trivial.
  apply (sym_not_eq (A:=R)); assumption.
  apply H5; assumption.
Qed.

Lemma dicho_lb_car :
  forall (x y:R) (P:R -> bool) (n:nat),
    P x = false -> P (dicho_lb x y P n) = false.
Proof.
  intros.
  induction  n as [| n Hrecn].
  simpl in |- *.
  assumption.
  simpl in |- *.
  assert
    (X :=
      sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))).
  elim X; intro.
  rewrite a.
  unfold dicho_lb in Hrecn; assumption.
  rewrite b.
  assumption.
Qed.

Lemma dicho_up_car :
  forall (x y:R) (P:R -> bool) (n:nat),
    P y = true -> P (dicho_up x y P n) = true.
Proof.
  intros.
  induction  n as [| n Hrecn].
  simpl in |- *.
  assumption.
  simpl in |- *.
  assert
    (X :=
      sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))).
  elim X; intro.
  rewrite a.
  unfold dicho_lb in Hrecn; assumption.
  rewrite b.
  assumption.
Qed.

(** Intermediate Value Theorem *)
Lemma IVT :
  forall (f:R -> R) (x y:R),
    continuity f ->
    x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }.
Proof.
  intros.
  cut (x <= y).
  intro.
  generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3).
  generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3).
  intros X X0.
  elim X; intros.
  elim X0; intros.
  assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
  rewrite H4 in p0.
  exists x0.
  split.
  split.
  apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0).
  simpl in |- *.
  right; reflexivity.
  apply growing_ineq.
  apply dicho_lb_growing; assumption.
  assumption.
  apply Rle_trans with (dicho_up x y (fun z:R => cond_positivity (f z)) 0).
  apply decreasing_ineq.
  apply dicho_up_decreasing; assumption.
  assumption.
  right; reflexivity.
  2: left; assumption.
  set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n).
  set (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n).
  cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0).
  cut ((forall n:nat, 0 <= f (Wn n)) -> 0 <= f x0).
  intros.
  cut (forall n:nat, f (Vn n) <= 0).
  cut (forall n:nat, 0 <= f (Wn n)).
  intros.
  assert (H9 := H6 H8).
  assert (H10 := H5 H7).
  apply Rle_antisym; assumption.
  intro.
  unfold Wn in |- *.
  cut (forall z:R, cond_positivity z = true <-> 0 <= z).
  intro.
  assert (H8 := dicho_up_car x y (fun z:R => cond_positivity (f z)) n).
  elim (H7 (f (dicho_up x y (fun z:R => cond_positivity (f z)) n))); intros.
  apply H9.
  apply H8.
  elim (H7 (f y)); intros.
  apply H12.
  left; assumption.
  intro.
  unfold cond_positivity in |- *.
  case (Rle_dec 0 z); intro.
  split.
  intro; assumption.
  intro; reflexivity.
  split.
  intro feqt;discriminate feqt.
  intro.
  elim n0; assumption.
  unfold Vn in |- *.
  cut (forall z:R, cond_positivity z = false <-> z < 0).
  intros.
  assert (H8 := dicho_lb_car x y (fun z:R => cond_positivity (f z)) n).
  left.
  elim (H7 (f (dicho_lb x y (fun z:R => cond_positivity (f z)) n))); intros.
  apply H9.
  apply H8.
  elim (H7 (f x)); intros.
  apply H12.
  assumption.
  intro.
  unfold cond_positivity in |- *.
  case (Rle_dec 0 z); intro.
  split.
  intro feqt; discriminate feqt.
  intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
  split.
  intro; auto with real.
  intro; reflexivity.
  cut (Un_cv Wn x0).
  intros.
  assert (H7 := continuity_seq f Wn x0 (H x0) H5).
  case (total_order_T 0 (f x0)); intro.
  elim s; intro.
  left; assumption.
  rewrite <- b; right; reflexivity.
  unfold Un_cv in H7; unfold R_dist in H7.
  cut (0 < - f x0).
  intro.
  elim (H7 (- f x0) H8); intros.
  cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ].
  assert (H11 := H9 x2 H10).
  rewrite Rabs_right in H11.
  pattern (- f x0) at 1 in H11; rewrite <- Rplus_0_r in H11.
  unfold Rminus in H11; rewrite (Rplus_comm (f (Wn x2))) in H11.
  assert (H12 := Rplus_lt_reg_r _ _ _ H11).
  assert (H13 := H6 x2).
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H12)).
  apply Rle_ge; left; unfold Rminus in |- *; apply Rplus_le_lt_0_compat.
  apply H6.
  exact H8.
  apply Ropp_0_gt_lt_contravar; assumption.
  unfold Wn in |- *; assumption.
  cut (Un_cv Vn x0).
  intros.
  assert (H7 := continuity_seq f Vn x0 (H x0) H5).
  case (total_order_T 0 (f x0)); intro.
  elim s; intro.
  unfold Un_cv in H7; unfold R_dist in H7.
  elim (H7 (f x0) a); intros.
  cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ].
  assert (H10 := H8 x2 H9).
  rewrite Rabs_left in H10.
  pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10.
  rewrite Ropp_minus_distr' in H10.
  unfold Rminus in H10.
  assert (H11 := Rplus_lt_reg_r _ _ _ H10).
  assert (H12 := H6 x2).
  cut (0 < f (Vn x2)).
  intro.
  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H13 H12)).
  rewrite <- (Ropp_involutive (f (Vn x2))).
  apply Ropp_0_gt_lt_contravar; assumption.
  apply Rplus_lt_reg_r with (f x0 - f (Vn x2)).
  rewrite Rplus_0_r; replace (f x0 - f (Vn x2) + (f (Vn x2) - f x0)) with 0;
    [ unfold Rminus in |- *; apply Rplus_lt_le_0_compat | ring ].
  assumption.
  apply Ropp_0_ge_le_contravar; apply Rle_ge; apply H6.
  right; rewrite <- b; reflexivity.
  left; assumption.
  unfold Vn in |- *; assumption.
Qed.

Lemma IVT_cor :
  forall (f:R -> R) (x y:R),
    continuity f ->
    x <= y -> f x * f y <= 0 -> { z:R | x <= z <= y /\ f z = 0 }.
Proof.
  intros.
  case (total_order_T 0 (f x)); intro.
  case (total_order_T 0 (f y)); intro.
  elim s; intro.
  elim s0; intro.
  cut (0 < f x * f y);
    [ intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 H2))
      | apply Rmult_lt_0_compat; assumption ].
  exists y.
  split.
  split; [ assumption | right; reflexivity ].
  symmetry  in |- *; exact b.
  exists x.
  split.
  split; [ right; reflexivity | assumption ].
  symmetry  in |- *; exact b.
  elim s; intro.
  cut (x < y).
  intro.
  assert (H3 := IVT (- f)%F x y (continuity_opp f H) H2).
  cut ((- f)%F x < 0).
  cut (0 < (- f)%F y).
  intros.
  elim (H3 H5 H4); intros.
  exists x0.
  elim p; intros.
  split.
  assumption.
  unfold opp_fct in H7.
  rewrite <- (Ropp_involutive (f x0)).
  apply Ropp_eq_0_compat; assumption.
  unfold opp_fct in |- *; apply Ropp_0_gt_lt_contravar; assumption.
  unfold opp_fct in |- *.
  apply Rplus_lt_reg_r with (f x); rewrite Rplus_opp_r; rewrite Rplus_0_r;
    assumption.
  inversion H0.
  assumption.
  rewrite H2 in a.
  elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
  exists x.
  split.
  split; [ right; reflexivity | assumption ].
  symmetry  in |- *; assumption.
  case (total_order_T 0 (f y)); intro.
  elim s; intro.
  cut (x < y).
  intro.
  apply IVT; assumption.
  inversion H0.
  assumption.
  rewrite H2 in r.
  elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
  exists y.
  split.
  split; [ assumption | right; reflexivity ].
  symmetry  in |- *; assumption.
  cut (0 < f x * f y).
  intro.
  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H2 H1)).
  rewrite <- Rmult_opp_opp; apply Rmult_lt_0_compat;
    apply Ropp_0_gt_lt_contravar; assumption.
Qed.

(** We can now define the square root function as the reciprocal
   transformation of the square root function *)
Lemma Rsqrt_exists :
  forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }.
Proof.
  intros.
  set (f := fun x:R => Rsqr x - y).
  cut (f 0 <= 0).
  intro.
  cut (continuity f).
  intro.
  case (total_order_T y 1); intro.
  elim s; intro.
  cut (0 <= f 1).
  intro.
  cut (f 0 * f 1 <= 0).
  intro.
  assert (X := IVT_cor f 0 1 H1 (Rlt_le _ _ Rlt_0_1) H3).
  elim X; intros t H4.
  exists t.
  elim H4; intros.
  split.
  elim H5; intros; assumption.
  unfold f in H6.
  apply Rminus_diag_uniq_sym; exact H6.
  rewrite Rmult_comm; pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f 1)).
  apply Rmult_le_compat_l; assumption.
  unfold f in |- *.
  rewrite Rsqr_1.
  apply Rplus_le_reg_l with y.
  rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *;
    rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
      left; assumption.
  exists 1.
  split.
  left; apply Rlt_0_1.
  rewrite b; symmetry  in |- *; apply Rsqr_1.
  cut (0 <= f y).
  intro.
  cut (f 0 * f y <= 0).
  intro.
  assert (X := IVT_cor f 0 y H1 H H3).
  elim X; intros t H4.
  exists t.
  elim H4; intros.
  split.
  elim H5; intros; assumption.
  unfold f in H6.
  apply Rminus_diag_uniq_sym; exact H6.
  rewrite Rmult_comm; pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y)).
  apply Rmult_le_compat_l; assumption.
  unfold f in |- *.
  apply Rplus_le_reg_l with y.
  rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *;
    rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
  pattern y at 1 in |- *; rewrite <- Rmult_1_r.
  unfold Rsqr in |- *; apply Rmult_le_compat_l.
  assumption.
  left; exact r.
  replace f with (Rsqr - fct_cte y)%F.
  apply continuity_minus.
  apply derivable_continuous; apply derivable_Rsqr.
  apply derivable_continuous; apply derivable_const.
  reflexivity.
  unfold f in |- *; rewrite Rsqr_0.
  unfold Rminus in |- *; rewrite Rplus_0_l.
  apply Rge_le.
  apply Ropp_0_le_ge_contravar; assumption.
Qed.

(* Definition of the square root: R+->R *)
Definition Rsqrt (y:nonnegreal) : R :=
  let (a,_) := Rsqrt_exists (nonneg y) (cond_nonneg y) in a.

(**********)
Lemma Rsqrt_positivity : forall x:nonnegreal, 0 <= Rsqrt x.
Proof.
  intro.
  assert (X := Rsqrt_exists (nonneg x) (cond_nonneg x)).
  elim X; intros.
  cut (x0 = Rsqrt x).
  intros.
  elim p; intros.
  rewrite H in H0; assumption.
  unfold Rsqrt in |- *.
  case (Rsqrt_exists x (cond_nonneg x)).
  intros.
  elim p; elim a; intros.
  apply Rsqr_inj.
  assumption.
  assumption.
  rewrite <- H0; rewrite <- H2; reflexivity.
Qed.

(**********)
Lemma Rsqrt_Rsqrt : forall x:nonnegreal, Rsqrt x * Rsqrt x = x.
Proof.
  intros.
  assert (X := Rsqrt_exists (nonneg x) (cond_nonneg x)).
  elim X; intros.
  cut (x0 = Rsqrt x).
  intros.
  rewrite <- H.
  elim p; intros.
  rewrite H1; reflexivity.
  unfold Rsqrt in |- *.
  case (Rsqrt_exists x (cond_nonneg x)).
  intros.
  elim p; elim a; intros.
  apply Rsqr_inj.
  assumption.
  assumption.
  rewrite <- H0; rewrite <- H2; reflexivity.
Qed.

repo: Coq-misc


text:
(*===========================================================================
    Monadic syntax and monad laws
  ===========================================================================*)
From mathcomp Require Import ssreflect ssrnat.

(* Collect the monad operations in their own class, and define nice Fsharp-like notation *)
(*=MonadOps *)
Class MonadOps T :=
{ retn {X} : X -> T X
; bind {X Y} : T X -> (X -> T Y) -> T Y }.
(*=End *)

Notation "'let!' x = c ; d" :=
  (bind c (fun x => d))
  (at level 200, x ident, c at level 150, d at level 200, right associativity).

Notation "'let!' ( x , y ) = c ; d" :=
  (bind c (fun z => match z with ( x , y ) => d end))
  (at level 200, x ident, y ident, c at level 150, d at level 200).

Notation "'let!' ( x , y , z ) = c ; d" :=
  (bind c (fun z => match z with ( x , y , z ) => d end))
  (at level 200, x ident, y ident, z ident, c at level 150, d at level 200).

Notation "'let!' ( x , y , z , w ) = c ; d" :=
  (bind c (fun z => match z with ( x , y , z, w ) => d end))
  (at level 200, x ident, y ident, z ident, w ident, c at level 150, d at level 200).

Notation "'do!' c ; d" :=
  (bind c (fun _ => d))
  (at level 200, c at level 150, d at level 200).

Fixpoint doMany {T} {ops: MonadOps T} n (c:T unit) : T unit :=
if n is n.+1
then (do! c; doMany n c)
else retn tt.

(*=Monad *)
Class Monad T {ops: MonadOps T} :=
{ id_l X Y (x: X) (f: X -> T Y) : bind (retn x) f = f x
; id_r X (c: T X) : bind c retn = c
; assoc X Y Z (c: T X) (f: X -> T Y) (g : Y -> T Z) :
  bind (bind c f) g = bind c (fun x => bind (f x) g) }.
(*=End *)
Lemma doManyAdd {T} {ops: MonadOps T} {laws: Monad T}  n c :
  forall n', doMany (n+n') c = do! doMany n c; doMany n' c.
Proof. induction n; move => n'. by rewrite add0n id_l. by rewrite /= assoc IHn. Qed.

Require Import Coq.Logic.FunctionalExtensionality.

Lemma doLet {T}{X} `{HT: Monad T} (c1: T unit) (c2: unit -> T X) :
  (let! u = c1; c2 u) = (do! c1; c2 tt).
Proof.
  f_equal. extensionality u. by case: u.
Qed.

Lemma doRet {T} `{HT: Monad T} c :
  (do! c; retn tt) = c.
Proof.
  by rewrite -doLet id_r.
Qed.

Definition fmap {M} `{MonadOps M} A B (f : A -> B) (m : M A) : M B
  := let! m' = m;
     retn (f m').

author: maximedenes