val combine_optional_terms (ots: list (option term)) : Tac (option term)
val combine_optional_terms (ots: list (option term)) : Tac (option term)
let rec combine_optional_terms (ots: list (option term)) : Tac (option term) =
  match ots with
  | [] -> None
  | [ot] -> ot
  | Some t1 :: remaining_ots ->
      (match combine_optional_terms remaining_ots with
       | Some t2 -> Some (`(let _ = (`#t1) in (`#t2)))
       | None -> Some t1)
  | None :: remaining_ots -> combine_optional_terms remaining_ots
module Util.Tactics

open FStar.Printf
open FStar.Tactics.V2
open FStar.Reflection.V2.TermEq

/// Replacing a function in the current goal
///
/// Using the tactic `replace_fn_in_goal` will replace all instances
/// of a given function invocation in the goal with an invocation of
/// another function.  You give it the name of the function to be
/// replaced (`fn`), the number of arguments to that function
/// (`argc`), and a lemma that demonstrates that the function is
/// equivalent to another function (`lem`).  That lemma must take
/// `argc` arguments and have a postcondition that says that `fn`
/// applied to that many arguments is `==` to another function.  You
/// don't have to supply the name of that second function since it's
/// taken from that postcondition automatically.
///
/// NOTE: The lemma must have as a postcondition that f a1 a2 ... ==
/// f' a1 a2 where f is the replaced function.  If it says that f' a1
/// a2 ... == f a1 a2 instead (i.e., in the wrong order) then
/// `replace_fn_in_goal` won't work.

let rec is_term_an_invocation_of_function (t: term) (fn: term) (argc: nat) : Tac bool =
  if argc = 0 then
    term_eq t fn
  else
    match t with
    | Tv_App fn' arg -> is_term_an_invocation_of_function fn' fn (argc - 1)
    | _ -> false

let replace_fn_in_goal (fn: term) (argc: nat) (lem: term) : Tac unit =
  let my_ctrl (t: term) : Tac (bool & ctrl_flag) =
    (is_term_an_invocation_of_function t fn argc, Continue) in
  let my_rw () : Tac unit =
    apply_lemma lem in
  ctrl_rewrite BottomUp my_ctrl my_rw

/// Synthesizing a lemma invocation for each instance of a function in a term
///
/// The tactic `fn_to_lemma_invocations_in_term` creates an optional
/// term that includes an invocation of lemma `lem` for each time a
/// given function `fn` appears in a given term `t`.  You must also supply
/// `argc`, the number of arguments to the function.  The lemma should take
/// the same arguments as the function, in the same order.
///
/// Once you have optional terms from one or more invocations of
/// `fn_to_lemma_invocations_in_term`, you can use them to synthesize
/// a proof of a squashed proposition.  To do this, use
/// `synthesize_proof_term_from_optional_terms`.  This will invoke the
/// `t_exact` tactic using a term that concatenates all the optional
/// terms.
/
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Util.Tactics.fst
ots: Prims.list (FStar.Pervasives.Native.option FStar.Tactics.NamedView.term)
  -> FStar.Tactics.Effect.Tac (FStar.Pervasives.Native.option FStar.Tactics.NamedView.term)
Prims.list FStar.Pervasives.Native.option FStar.Tactics.NamedView.term FStar.Pervasives.Native.None FStar.Pervasives.Native.Some Util.Tactics.combine_optional_terms
let rec combine_optional_terms (ots: list (option term)) : Tac (option term) =
  
match ots with
| [] -> None
| [ot] -> ot
| Some t1 :: remaining_ots ->
  (match combine_optional_terms remaining_ots with
    | Some t2 ->
      Some
      (`(let _ = (`#t1) in
          (`#t2)))
    | None -> Some t1)
| None :: remaining_ots -> combine_optional_terms remaining_ots