Library Waterproof.Tactics.Unfold


Require Import Ltac2.Ltac2.
Require Import Ltac2.Std.
Require Import Ltac2.Message.
Local Ltac2 concat_list (ls : message list) : message :=
  List.fold_right concat (of_string "") ls.

Require Import Util.Goals.
Require Import Util.MessagesToUser.

Local Ltac2 _is_empty (ls : 'a list) :=
  match ls with
  | _::_ => false
  | [] => true
  end.

Ltac2 Type exn ::= [ Inner ].

Attempts to unfold definition(s) in every statement according to specified method. If succesful it prints a list of suitable tactics that can be used to incorporate the unfolded statements into the user's proof script. E.g. if the defition was unfolded in the proof goal, the list will include 'We need to show that (statement with unfolded definiton)'.
Arguments:
  • unfold method: constr -> constr, method to be used for unfolding unfolding is deemed to be succesful if unfold_method statement =\= statement
  • def_name: string, optional string used for error message when unfolding is unsuccesful
  • throw_error : bool, whether the tactic should throw an error which suggests user to remove this tactic in final version of the proof.
Raises fatal exceptions:
  • always/none depending on value of throw_error.

Ltac2 unfold_in_all (unfold_method: constr -> constr)
  (def_name : string option) (throw_error : bool) :=


  let goal := Control.goal () in
  let unfolded_goal := unfold_method goal in
  let did_unfold_goal := Bool.neg (Constr.equal unfolded_goal goal) in

  let hyps := List.map (fun (i, def, t) => t) (Control.hyps ()) in
  let unfolded_hyps := List.map unfold_method hyps in
  let only_unfolded_hyps :=
    List.map (fun (uh, h) => uh) (
      List.filter_out (fun (uh, h) => Constr.equal uh h) (
        List.combine unfolded_hyps hyps
      )
    ) in

  
  if (Bool.or did_unfold_goal (Bool.neg (_is_empty only_unfolded_hyps)))
    then
      
      info_notice (of_string "Expanded definition in statements where applicable.");
      let total_messages := Int.add
        (if did_unfold_goal then 1 else 0)
        (List.length only_unfolded_hyps) in
      
      let print_tactic :=
        if (Int.lt 1 total_messages) then
          fun m => insert_msg (to_string m) (to_string (concat m (of_string "${}")))
        else
          fun m => replace_msg (to_string m) (to_string (concat m (of_string "${}")))
        in
      
      
      if did_unfold_goal
        then
          print_tactic (concat_list [of_string "We need to show that ";
            of_constr unfolded_goal; of_string "."])
        else ();

      
      if (Bool.neg (_is_empty only_unfolded_hyps))
        then
          let it_holds_msg := fun (x : constr) => concat_list
            [of_string "It holds that "; of_constr x; of_string "."] in
          List.fold_left (fun _ unfolded_h => print_tactic (it_holds_msg unfolded_h))
            only_unfolded_hyps ()
        else ()

    else
      
      match def_name with
      | None => info_notice (of_string "Definition does not appear in any statement.")
      | Some def_name => info_notice (concat_list
          [of_string "'"; of_string def_name; of_string "'";
            of_string " does not appear in any statement."])
      end;

  
  if throw_error
    then throw (of_string "Remove this line in the final version of your proof.")
    else ().

Either attempts to unfold definition(s) in every statement according to specified method, or attempts to unfold definition(s) in the provided statement. If succesful it prints a list of suitable tactics that can be used to incorporate the unfolded statements into the user's proof script. E.g. if the defition was unfolded in the proof goal, the list will include 'We need to show that (statement with unfolded definiton)'.
Arguments:
  • unfold method: constr -> constr, method to be used for unfolding unfolding is deemed to be succesful if unfold_method statement =\= statement
  • def_name: string, optional string used for error message when unfolding is unsuccesful
  • throw_error : bool, whether the tactic should throw an error which suggests user to remove this tactic in final version of the proof.
  • x : constr option, unused, kept for compatibility.
Raises fatal exceptions:
  • always/none depending on value of throw_error.
Ltac2 wp_unfold (unfold_method: constr -> constr)
  (def_name : string option) (throw_error : bool) (x : constr option):=
  panic_if_goal_wrapped ();
  unfold_in_all unfold_method def_name throw_error.


Ltac2 Notation "Expand" "the" "definition" "of" targets(list1(seq(reference, occurrences), ",")) :=

  wp_unfold (eval_unfold targets) None true None.

Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" targets(list1(seq(reference, occurrences), ",")) :=
  wp_unfold (eval_unfold targets) None false None.