val closure_one_aux: #a:Type u#a -> r:binrel u#a u#r a -> x:a -> y:a
  -> xy:_closure r x y
  -> Tot (either (squash (x == y))
                (z:a & squash (r x z) & _closure r z y))
    (decreases xy)
let rec closure_one_aux #a r x y xy =
  match xy with
  | Refl _ -> Inl ()
  | Step _ _ pr -> Inr (| y, pr, Refl y |)
  | Closure x i y xi iy ->
    match closure_one_aux r i y iy with
    | Inl _ -> closure_one_aux r x y xi
    | Inr (| z, r_i_z, c_z_y |) ->
      let c_z_y : _closure r z y = c_z_y in
      match closure_one_aux r x i xi with
      | Inl _ -> Inr (| z, r_i_z, c_z_y |)
      | Inr (| w, r_x_w, c_w_i |) ->
        let step : _closure r i z = Step #a #r i z r_i_z in
        let c_i_y : _closure r i y = Closure i z y step c_z_y in
        let c_w_y : _closure r w y =  Closure w i y c_w_i c_i_y in
        Inr (| w, r_x_w, c_w_y |)
val closure_one_aux: #a:Type u#a -> r:binrel u#a u#r a -> x:a -> y:a
  -> xy:_closure r x y
  -> Tot (either (squash (x == y))
                (z:a & squash (r x z) & _closure r z y))
    (decreases xy)
let rec closure_one_aux #a r x y xy =
match xy with
| Refl _ -> Inl ()
| Step _ _ pr -> Inr (| y, pr, Refl y |)
| Closure x i y xi iy ->
  match closure_one_aux r i y iy with
  | Inl _ -> closure_one_aux r x y xi
  | Inr (| z , r_i_z , c_z_y |) ->
    let c_z_y:_closure r z y = c_z_y in
    match closure_one_aux r x i xi with
    | Inl _ -> Inr (| z, r_i_z, c_z_y |)
    | Inr (| w , r_x_w , c_w_i |) ->
      let step:_closure r i z = Step #a #r i z r_i_z in
      let c_i_y:_closure r i y = Closure i z y step c_z_y in
      let c_w_y:_closure r w y = Closure w i y c_w_i c_i_y in
      Inr (| w, r_x_w, c_w_y |)
FStar.ReflexiveTransitiveClosure.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Squash.fsti.checked FStar.Pervasives.fsti.checked
FStar.ReflexiveTransitiveClosure.fst
FStar.ReflexiveTransitiveClosure.binrel FStar.ReflexiveTransitiveClosure._closure FStar.Pervasives.Inl Prims.squash Prims.eq2 FStar.Pervasives.dtuple3 FStar.Pervasives.Inr FStar.Pervasives.Mkdtuple3 FStar.ReflexiveTransitiveClosure.Refl FStar.ReflexiveTransitiveClosure.closure_one_aux FStar.ReflexiveTransitiveClosure.Closure FStar.ReflexiveTransitiveClosure.Step FStar.Pervasives.either
(*
   Copyright 2008-2019 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.ReflexiveTransitiveClosure

open FStar.Tactics.V2
#set-options "--max_ifuel 1 --max_fuel 0"

noeq
type _closure (#a:Type u#a) (r:binrel u#a u#r a) : a -> a -> Type u#(max a r) =
| Refl: x:a -> _closure r x x
| Step: x:a -> y:a -> squash (r x y) ->_closure r x y
| Closure: x:a -> y:a -> z:a -> _closure r x y -> _closure r y z -> _closure r x z

let _closure0 (#a:Type) (r:binrel a) (x y: a) : prop =
  squash (_closure r x y)

let get_squash (#a:Type) (r:binrel a) (x:a) (y:a{_closure0 r x y})
  : Tot (squash (_closure r x y))
  = assert_norm (_closure0 r x y ==> squash (_closure r x y))

val closure_reflexive: #a:Type u#a -> r:binrel u#a u#r a -> Lemma (reflexive (_closure0 r))
let closure_reflexive #a r =
  assert (forall x. _closure0 r x x) by
    (let x = forall_intro () in
     mapply (`FStar.Squash.return_squash);
     mapply (`Refl))

#push-options "--warn_error -271"
val closure_transitive: #a:Type u#a -> r:binrel u#a u#r a -> Lemma (transitive (_closure0 r))
let closure_transitive #a r =
  let open FStar.Squash in
  let aux (x y z:a)
          (s0:squash (_closure r x y))
          (s1:squash (_closure r y z))
    : GTot (squash (_closure r x z))
    = bind_squash s0 (fun p0 ->
      bind_squash s1 (fun p1 ->
      return_squash (Closure x y z p0 p1)))
  in
  let aux (x y z:a)
    : Lemma (requires (_closure0 r x y /\ _closure0 r y z))
            (ensures _closure0 r x z)
            [SMTPat ()]
    = get_squash r x y; get_squash r y z; aux x y z () ()
  in
  ()
#pop-options

let closure #a r =
  closure_reflexive r;
  closure_transitive r;
  _closure0 r

let closure_step #a r x y =
  let q : squash (r x y)  = () in
  assert (squash (r x y) ==> closure r x y) by
    (let xy = implies_intro () in
     let xy : squash (r x y) = unquote (binding_to_term xy) in
     squash_intro ();
     mapply (`Step);
     assumption())

val closure_one_aux: #a:Type u#a -> r:binrel u#a u#r a -> x:a -> y:a
  -> xy:_closure r x y
  -> Tot (either (squash (x == y))
                (z:a & squash (r x z) & _closure r z y))
    (decreases xy)
val closure_one_aux: #a:Type u#a -> r:binrel u#a u#r a -> x:a -> y:a
  -> xy:_closure r x y
  -> Tot (either (squash (x == y))
                (z:a & squash (r x z) & _closure r z y))
    (decreases xy)

    r: FStar.ReflexiveTransitiveClosure.binrel a ->
    x: a ->
    y: a ->
    xy: FStar.ReflexiveTransitiveClosure._closure r x y
  -> Prims.Tot
    (FStar.Pervasives.either (Prims.squash (x == y))
        (FStar.Pervasives.dtuple3 a
            (fun z -> Prims.squash (r x z))
            (fun z _ -> FStar.ReflexiveTransitiveClosure._closure r z y)))