val gfp_implies_than_itself (#a: _) (f: mono_fun a)
    : Lemma (forall m x. interp (gfp f x) m ==> interp (f (gfp f) x) m)
val gfp_implies_than_itself (#a: _) (f: mono_fun a)
    : Lemma (forall m x. interp (gfp f x) m ==> interp (f (gfp f) x) m)
let gfp_implies_than_itself
    #a (f: mono_fun a)
: Lemma// (implies (gfp f) (f (gfp f)))
    (forall m x. interp (gfp f x) m ==> interp (f (gfp f) x) m)
= gfp_sat f; lemma_D f
module Steel.Coinduction

open Steel.Memory

#push-options "--print_universes"

unfold
let inner_gfp #a (f: pred a -> pred a) (x: a) (p: pred a)
= h_and (p x) (pure (implies p (f p)))

let h_and_equiv (p q: slprop) (m:mem)
  : Lemma ((interp p m /\ interp q m) <==> interp (h_and p q) m)
= elim_h_and p q m; intro_h_and p q m

let inner_gfp_equiv
#a (f: pred a -> pred a) (x: a) (p: pred a) m
: Lemma (
    interp (inner_gfp f x p) m 
    <==> interp (p x) m /\ implies p (f p)
)
= h_and_equiv (p x) (pure (implies p (f p))) m;
  pure_interp (implies p (f p)) m

let gfp_sat_aux #a (f: pred a -> pred a) m x:
Lemma ((exists p. interp (p x) m /\ implies p (f p) ) <==> interp (gfp f x) m)
= introduce forall p. ((interp (p x) m /\ implies p (f p)) ==> interp (gfp f x) m) with (
    inner_gfp_equiv f x p m;
    intro_h_exists p (
        fun p -> h_and (p x) (pure (implies p (f p)))
    ) m
);
introduce interp (gfp f x) m ==> (exists p. interp (p x) m /\ implies p (f p) )
with _. (
    elim_h_exists (
        fun p -> h_and (p x) (pure (implies p (f p)))
    ) m;
    introduce forall p.
    (
        interp (inner_gfp f x p) m ==> (interp (p x) m /\ implies p (f p) )
    )
    with (
        inner_gfp_equiv f x p m
    )
)

let gfp_sat #a (f: pred a -> pred a):
Lemma (forall m x. (exists p. interp (p x) m /\ implies p (f p) ) <==> interp (gfp f x) m)
=  introduce forall m x. ((exists p. interp (p x) m /\ implies p (f p) ) <==> interp (gfp f x) m)
with (gfp_sat_aux f m x)

let set_D #a (f: pred a -> pred a) (p: pred a)
= (implies p (f p))


let in_D_implies_than_u #a (f: mono_fun a) p
: Lemma (requires set_D f p)
    (ensures implies p (gfp f))
= gfp_sat f

let lemma_D_aux #a (f: mono_fun a) p
: Lemma (requires set_D f p)
        (ensures implies p (f (gfp f)))
= 
let u = gfp f in
  in_D_implies_than_u f p;
  assert (implies (f p) (f u))

let lemma_D #a (f: mono_fun a)
: Lemma (forall p. set_D f p ==> implies p (f (gfp f)))
=
introduce forall p. (set_D f p ==> implies p (f (gfp f)))
with (
    introduce set_D f p ==> implies p (f (gfp f))
    with _. lemma_D_aux f p)
/
Steel.Memory.fsti.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Calc.fsti.checked
Steel.Coinduction.fst
f: Steel.Coinduction.mono_fun a
  -> FStar.Pervasives.Lemma
    (ensures
      forall (m: Steel.Memory.mem) (x: a).
        Steel.Memory.interp (Steel.Coinduction.gfp f x) m ==>
        Steel.Memory.interp (f (Steel.Coinduction.gfp f) x) m)
Steel.Coinduction.mono_fun Steel.Coinduction.lemma_D Prims.unit Steel.Coinduction.gfp_sat Prims.l_True Prims.squash Prims.l_Forall Steel.Memory.mem Prims.l_imp Steel.Memory.interp Steel.Coinduction.gfp Prims.Nil FStar.Pervasives.pattern
let gfp_implies_than_itself #a (f: mono_fun a)
    : Lemma (forall m x. interp (gfp f x) m ==> interp (f (gfp f) x) m) =
  
gfp_sat f;
lemma_D f