val 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)
val 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)
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
    )
)
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
/
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.pred a -> Steel.Coinduction.pred a) -> m: Steel.Memory.mem -> x: a
  -> FStar.Pervasives.Lemma
    (ensures
      (exists (p: (_: a -> Steel.Memory.slprop)).
          Steel.Memory.interp (p x) m /\ Steel.Coinduction.implies p (f p)) <==>
      Steel.Memory.interp (Steel.Coinduction.gfp f x) m)
Steel.Coinduction.pred Steel.Memory.mem FStar.Classical.Sugar.implies_intro Steel.Memory.interp Steel.Coinduction.gfp Prims.squash Prims.l_Exists Steel.Memory.slprop Prims.l_and Steel.Coinduction.implies FStar.Classical.Sugar.forall_intro Prims.l_imp Steel.Coinduction.inner_gfp Steel.Coinduction.inner_gfp_equiv Prims.unit Steel.Memory.elim_h_exists Steel.Memory.h_and Steel.Memory.pure Steel.Memory.intro_h_exists Prims.l_True Prims.l_iff Prims.Nil FStar.Pervasives.pattern
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))