Library Waterproof.Waterprove

Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.
Ltac2 Type exn ::= [ Inner
                    | FailedToUse (constr)
                    | FailedToProve (constr) ].

Require Import Waterproof.
Require Import Notations.Sets.

Require Import Ltac2.Bool.
Require Import Ltac2.Init.

Require Import Chains.Inequalities.

Local Ltac2 Type database_type_ffi.

Local Ltac2 @ external database_type_main: unit -> database_type_ffi := "coq-waterproof" "database_type_main".
Local Ltac2 @ external database_type_decidability: unit -> database_type_ffi := "coq-waterproof" "database_type_decidability".
Local Ltac2 @ external database_type_shorten: unit -> database_type_ffi := "coq-waterproof" "database_type_shorten".

Local Ltac2 @ external waterprove_ffi: int -> bool -> (unit -> constr) list -> database_type_ffi -> unit := "coq-waterproof" "waterprove".
Local Ltac2 @ external rwaterprove_ffi: int -> bool -> (unit -> constr) list -> database_type_ffi -> constr list -> constr list -> unit := "coq-waterproof" "rwaterprove".

Ltac2 Type database_type := [ Main | Decidability | Shorten ].

Local Ltac2 database_type_to_ffi (db_type: database_type): database_type_ffi :=
  match db_type with
    | Main => database_type_main ()
    | Decidability => database_type_decidability ()
    | Shorten => database_type_shorten ()
  end.

Open Scope subset_scope.

Local Ltac2 contains_shielded_pattern (): bool :=
  lazy_match! goal with
    | [ |- forall _, _ ] => true
    | [ |- ∀ _ _ , _] => true
    | [ |- exists _, _ ] => true
    | [ |- ∃ _ _ , _] => true
    | [ |- _ /\ _] => true
    | [ |- _ \/ _] => true
    | [ |- _] => false
  end.

Close Scope subset_scope.

Internal versions of waterprove and rwaterprove.

Local Ltac2 _waterprove (depth: int) (shield: bool) (lems: (unit -> constr) list) (db_type: database_type): unit :=
waterprove_ffi depth (shield && contains_shielded_pattern ()) lems (database_type_to_ffi db_type).

Local Ltac2 _risky_rwaterprove (depth: int) (shield: bool) (lems: (unit -> constr) list) (db_type: database_type) (must : constr list) (forbidden : constr list) : unit :=
rwaterprove_ffi depth (shield && contains_shielded_pattern ()) lems (database_type_to_ffi db_type) must forbidden.

Checks whether x is in the current list of hypotheses

Local Ltac2 in_hypotheses (x : constr) :=
  match! goal with
  | [ h_id : _ |- _ ] =>

    let h := Control.hyp h_id in
    match Constr.equal x h with
    | false => Control.zero Inner
    | true => true
    end
  | [ |- _ ] => false
  end.

Local Ltac2 _rwaterprove (depth: int) (shield: bool) (db_type: database_type)
  (xtr_lemma : constr) : unit :=


  match in_hypotheses xtr_lemma with
  | false =>

    _risky_rwaterprove depth shield [fun () => xtr_lemma] db_type [xtr_lemma] []
  | true =>
    _waterprove depth shield [] Main
  end.

Subroutine to solve conjunction of statements piece by piece. Throws FailedToProve error with statement that could not be proven.

Local Ltac2 rec waterprove_iterate_conj (depth: int) (shield: bool)
(db_type: database_type) (xtr_lemma : constr option) :=

  let list_lemmas :=
    match xtr_lemma with
    | None => []
    | Some lem => [fun () => lem]
    end
  in
  lazy_match! goal with

  | [ |- ?g1 /\ ?remainder ] =>
    split;

    match Control.case (fun () => Control.focus 1 1 (fun () =>
      _waterprove depth shield list_lemmas db_type))
    with
    | Val _ => waterprove_iterate_conj depth shield db_type xtr_lemma
    | Err exn => Control.zero (FailedToProve g1)
    end

  | [ |- _ ] =>

    match Control.case (fun () =>
      _waterprove depth shield list_lemmas db_type)
    with
    | Val _ => ()
    | Err exn => Control.zero (FailedToProve (Control.goal ()))
    end
  end.

Subroutine to solve conjunction of statements piece by piece using an extra lemma which has to be used. Throws FailedToProve error with statement that could not be proven. Throws FailedToUse error if no proof of the statements used the extra lemma.

Local Ltac2 rec rwaterprove_iterate_conj (depth: int) (shield: bool)
(db_type: database_type) (xtr_lemma : constr) :=
  lazy_match! goal with

  | [ |- ?g1 /\ _ ] =>
    split;

    match Control.case (fun () => Control.focus 1 1 (fun () =>
      _rwaterprove depth shield db_type xtr_lemma))
    with
    | Val _ =>

      waterprove_iterate_conj depth shield db_type (Some xtr_lemma)
    | Err exn =>

      match Control.case (fun () => Control.focus 1 1 (fun () =>
        _waterprove depth shield [] db_type))
      with
      | Val _ =>

        rwaterprove_iterate_conj depth shield db_type xtr_lemma
      | Err exn => Control.zero (FailedToProve g1)
      end
    end

  | [ |- _ ] =>

    match Control.case (fun () =>
      _rwaterprove depth shield db_type xtr_lemma)
    with
    | Val _ => ()
    | Err exn =>

      match Control.case (fun () =>
        _waterprove depth shield [] db_type)
      with
      | Err exn => Control.zero (FailedToProve (Control.goal ()))
      | Val _ =>
        Control.zero (FailedToUse xtr_lemma)
      end
    end
  end.

External versions of (restricted) automation. (In)equality chains are attempted piece by piece.

Lemma _and_assoc1 (A B C : Prop) : A /\ B /\ C -> (A /\ B ) /\ C.
Proof. apply and_assoc. Qed.

Attempts to prove current goal. Throws FailedToProve error with statement that could not be proven. (In)equality chains are attempted piece by piece.

Ltac2 waterprove (depth: int) (shield: bool) (db_type: database_type) :=
  lazy_match! goal with

  | [ |- total_statement _ ] =>
    cbn; repeat (apply _and_assoc1);
    waterprove_iterate_conj depth shield db_type None

  | [ |- _] =>
    match Control.case (fun () =>
      _waterprove depth shield [] db_type)
    with
    | Val _ => ()
    | Err exn => Control.zero (FailedToProve (Control.goal ()))
    end
  end.

Attempts to prove current goal. Throws FailedToProve error with statement that could not be proven. Throws FailedToUse error with xtr_lemma if no proof could be found that uses it. (In)equality chains are attempted piece by piece.

Ltac2 rwaterprove (depth: int) (shield: bool) (db_type: database_type) (xtr_lemma : constr) :=
  lazy_match! goal with

  | [ |- total_statement _ ] =>
    cbn; repeat (apply _and_assoc1);
    rwaterprove_iterate_conj depth shield db_type xtr_lemma

  | [ |- _] =>

    match Control.case (fun () =>
      _rwaterprove depth shield db_type xtr_lemma)
    with
    | Val _ => ()
    | Err exn =>

      match Control.case (fun () =>
        _waterprove depth shield [] db_type)
      with
      | Err exn => Control.zero (FailedToProve (Control.goal ()))
      | Val _ =>
        Control.zero (FailedToUse xtr_lemma)
      end
    end
  end.