val empty_relation (#a: Type u#a) (x1 x2: a) : Type0
let empty_relation (#a: Type u#a) (x1: a) (x2: a) : Type0 = False
val empty_relation (#a: Type u#a) (x1 x2: a) : Type0
let empty_relation (#a: Type u#a) (x1 x2: a) : Type0 =
False
FStar.WellFoundedRelation.fsti.checked
prims.fst.checked FStar.WellFounded.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
FStar.WellFoundedRelation.fsti
Prims.l_False
(*
   Copyright 2022 Jay Lorch and Nikhil Swamy, 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.
*)

(* This library is intended to simplify using well-founded relations
   in decreases clauses.

   The key data structure is `wfr_t a`, which encapsulates a
   well-founded relation on `a`. Specifically, the predicate
   `wfr.relation x1 x2` means that `x1` precedes `x2` in the
   well-founded relation described by `wfr`.

   You can then use this relatedness to show that a function is
   decreasing in a certain term. Whenever `wfr.relation x1 x2` holds,
   `wfr.decreaser x1 << wfr.decreaser x2` also holds. The library has
   an ambient lemma triggered by seeing two instances of
   `wfr.decreaser`, so you can use `wfr.decreaser x` in your decreases
   clause. For example:

     // Define `nat_nat_wfr` to represent the lexicographically-precedes
     // relation between two elements of type `nat * nat`. That is,
     // `(x1, y1)` is related to `(x2, y2)` if
     // `x1 < x2 \/ (x1 == x2 /\ y1 < y2)`.

     let nat_nat_wfr = lex_nondep_wfr (default_wfr nat) (default_wfr nat)

     // To show that `f` is well-defined, we use the decreases clause
     // `nat_nat_wfr.decreaser (x, y)`. We then need to show, on each
     // recursive call, that the parameters x2 and y2 to the nested
     // call satisfy `nat_nat_wfr.relation (x2, y2) (x, y)`.

     let rec f (x: nat) (y: nat)
       : Tot nat (decreases (nat_nat_wfr.decreaser (x, y))) =
       if x = 0 then
         0
       else if y = 0 then (
         // This assertion isn't necessary; it's just for illustration
         assert (nat_nat_wfr.relation (x - 1, 100) (x, y));
         f (x - 1) 100
       )
       else (
         // This assertion isn't necessary; it's just for illustration
         assert (nat_nat_wfr.relation (x, y - 1) (x, y));
         f x (y - 1)
       )

  One way `wfr_t` can be useful is that it simplifies debugging when
  the SMT solver can't verify termination. You can assert the
  relation explicitly (as in the examples above), and if the assertion
  doesn't hold you can try to prove it. If you instead use something
  like `decreases %[x, y]`, it's harder to debug because you can't
  `assert (%[x2, y2] << %[x, y])`.

  But where `wfr_t` is most useful is in writing a function that takes
  a well-founded relation as input. Here's an illustrative example:

    let rec count_steps_to_none
      (#a: Type)
      (wfr: wfr_t a)
      (stepper: (x: a) -> (y: option a{Some? y ==> wfr.relation (Some?.v y) x}))
      (start: option a)
      : Tot nat (decreases (option_wfr wfr).decreaser start) =
      match start with
      | None -> 0
      | Some x -> 1 + count_steps_to_none wfr stepper (stepper x)

  `wfr_t` is also useful when composing a well-founded relation
  produced using `acc` (from the FStar.WellFounded library) with one
  or more other well-founded relations.

  There are a few ways to build a `wfr_t`, described in more detail in
  comments throughout this file. Those ways are:

    `default_wfr a`
    `empty_wfr a`
    `acc_to_wfr r f`
    `subrelation_to_wfr r wfr`
    `inverse_image_to_wfr r f wfr`
    `lex_nondep_wfr wfr_a wfr_b`
    `lex_dep_wfr wfr_a a_to_wfr_b`
    `bool_wfr`
    `option_wfr wfr`
*)

module FStar.WellFoundedRelation

noeq type acc_classical (#a: Type u#a) (r: a -> a -> Type0) (x: a) : Type u#a =
  | AccClassicalIntro : access_smaller:(y: a{r y x} -> acc_classical r y) -> acc_classical r x

noeq type wfr_t (a: Type u#a) : Type u#(a + 1) =
  {
    relation: a -> a -> Type0;
    decreaser: (x: a -> acc_classical relation x);
    proof: (x1: a) -> (x2: a) -> 
           Lemma (requires relation x1 x2) (ensures decreaser x1 << decreaser x2);
  }

let ambient_wfr_lemma (#a: Type u#a) (wfr: wfr_t a) (x1: a) (x2: a)
  : Lemma (requires wfr.relation x1 x2)
          (ensures  wfr.decreaser x1 << wfr.decreaser x2)
          [SMTPat (wfr.decreaser x1); SMTPat (wfr.decreaser x2)] =
  wfr.proof x1 x2

/// `default_wfr a` is the well-founded relation built into F* for
/// type `a`. For instance, for `nat` it's the less-than relation.
/// For an inductive type it's the sub-term ordering.
///
/// `(default_wfr a).relation` is `default_relation` as defined below.

let default_relation (#a: Type u#a) (x1: a) (x2: a) : Type0 = x1 << x2

val default_wfr (a: Type u#a) : (wfr: wfr_t a{wfr.relation == default_relation})

/// `empty_wfr a` is the empty well-founded relation, which doesn't relate any
/// pair of values.
///
/// `(empty_wfr a).relation` is `empty_relation` as defined below.
val empty_relation (#a: Type u#a) (x1 x2: a) : Type0
x1: a -> x2: a -> Type0