Library Waterproof.Tactics.Assume


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

Require Import Util.Constr.
Require Import Util.Goals.
Require Import Util.Hypothesis.
Require Import Util.Init.
Require Import Util.MessagesToUser.
Require Import Util.TypeCorrector.

Require Import Waterproof.Tactics.Help.

Local Ltac2 expected_of_type_instead_of_message (e : constr) (t : constr) :=
  concat_list [of_string "Expected assumption of "; of_constr e;
    of_string " instead of "; of_constr t; of_string "."].
Attempts to assume a negated expression.
Arguments:
  • x : (constr * (ident option)) list: list of (expression optional name for expression)).
Does:
  • For the first pair of (expession (and name)) in x, assume the expression.
Raises fatal exceptions:
  • If the current goal does not require the assumption of an expression t where t is the expression from the first pair in x.
  • If x contains more than one element.
Local Ltac2 assume_negation (x : (constr * (ident option)) list) :=
  match x with
  | [] => ()
  | head::tail =>
      match head with
      | (t, n) =>
          lazy_match! goal with
          | [ |- not ?u ] =>
              let t := correct_type_by_wrapping t in
              match check_constr_equal u t with
              | false => throw (expected_of_type_instead_of_message u t)
              | true =>
                  match tail with
                  | h::t => throw (of_string "Nothing left to assume after the negated expression.")
                  | [] =>
                      match n with
                      | None => let h := Fresh.in_goal @_H in intro $h; change $t in $h
                      | Some n => intro $n; change $t in $n
                      end;
                      
                      HelpNewHyp.suggest_how_to_use t n
                  end
              end
          | [ |- _ ] => Control.zero (Unreachable "")
          end
      end
  end.

Attempts to recursively assume a list of hypotheses.
Arguments:
  • x : (constr * (ident option)) list): list of (hypothesis and optional hypothesis name).
Does:
  • For the first pair of (hypothesis (and name)) in x, assume the hypothesis (with specified name). If the assumed hypothesis did not come from a negated expression, proceeds to call itself with the remaining pairs in x as a new list x'.
Raises fatale xceptions:
  • If the current goal does not require the assumption of any more hypotheses in general or one of type t, where t is the type from the first pair in x.
Local Ltac2 rec process_ident_type_pairs (x : (constr * (ident option)) list) :=
  match x with
  | head::tail =>
      match head with
      | (t, n) =>
          lazy_match! goal with
          | [ |- not _ ] => assume_negation x
          | [ |- ?u -> _ ] =>
              let sort_u := get_value_of_hyp u in
              match check_constr_equal sort_u constr:(Prop) with
              | true =>
                  let t := correct_type_by_wrapping t in
                  match check_constr_equal u t with
                  | true =>
                      match n with
                      | None => let h := Fresh.in_goal @_H in intro $h; change $t in $h
                      | Some n => intro $n; change $t in $n
                      end;
                      
                      HelpNewHyp.suggest_how_to_use t n
                  | false => throw (expected_of_type_instead_of_message u t)
                  end
              | false => throw (of_string "`Assume ...` cannot be used to construct a map (→). Use [Take] instead.")
              end
          | [ |- _ ] => throw (of_string "Tried to assume too many properties.")
          end
      end;

      
      process_ident_type_pairs tail
    
    | [] => ()
  end.

Local Ltac2 remove_contra_wrapper (wrapped_assumption : constr) (assumption : constr) :=
  match (check_constr_equal wrapped_assumption assumption) with
  | true => apply (ByContradiction.wrap $wrapped_assumption)
  | false => throw (of_string "Wrong assumption specified.")
  end.

Checks whether the 'Assume' tactic can be applied to the current goal, attempts to introduce a list of hypotheses.
Local Ltac2 assume (x : (constr * (ident option)) list) :=
  
  lazy_match! goal with
  | [ |- ByContradiction.Wrapper ?a _ ] =>
      match x with
      | head::_ =>
        match head with
        | (t,_) => remove_contra_wrapper a t
        end
      | [] => panic_if_goal_wrapped ()
      end
  | [ |- _ ] => panic_if_goal_wrapped ()
  end;
  
  lazy_match! goal with
  | [ |- not _ ] => assume_negation x
  | [ |- _ -> _ ] => process_ident_type_pairs x
  | [ |- _ ] => throw (of_string "`Assume ...` can only be used to prove an implication (⇨) or a negation (¬).")
  end.

Version with type checking.
Ltac2 Notation "Assume" "that" x(list1(seq(constr, opt(seq("(", ident, ")"))), "and")) := assume x.

Simply alternative notation for Assume.
Ltac2 Notation "such" "that" x(list1(seq(constr, opt(seq("(", ident, ")"))), "and")) := assume x.