Library UniMath.Tactics.Nat_Tactics

Author: Michael A. Warren (maw@mawarren.net) in consultation with Vladimir Voevodsky. Date: Spring - Summer 2015. Description: Some tactics for natural numbers.
Tactics for natural numbers. by Michael A. Warren, April - June 2015.
ADD: Disclaimer regarding connection with other tactics files.

Require Import
        UniMath.Foundations.NaturalNumbers
        UniMath.Tactics.Utilities
        UniMath.Tactics.Abmonoids_Tactics.

Local Open Scope nat_scope.

Basic definitions and hints.


Definition natneqtwist n (p : ¬ (0 = n)) : ¬ (n = 0) :=
  λ f, p (pathsinv0 f).

Definition nat_plus_perm021 :
  ∏ n0 n1 n2,
    n0 + n1 + n2 = n0 + n2 + n1 :=
  λ n0 n1 n2,
    pathscomp0
      (pathscomp0
         (natplusassoc n0 n1 n2)
         (maponpaths (λ z, n0 + z) (natpluscomm n1 n2)))
      (pathsinv0 (natplusassoc n0 n2 n1)).

Definition nat_plus_perm102 :
  ∏ n0 n1 n2,
    n0 + n1 + n2 = n1 + n0 + n2 :=
  λ n0 n1 n2, maponpaths (λ z, z + n2) (natpluscomm n0 n1).

Definition nat_plus_perm120 :
  ∏ n0 n1 n2,
    n0 + n1 + n2 = n2 + n0 + n1 :=
  λ n0 n1 n2,
    pathscomp0 (natpluscomm (n0 + n1) n2) (pathsinv0 (natplusassoc n2 n0 n1)).

Definition nat_plus_perm201 :
  ∏ n0 n1 n2,
    n0 + n1 + n2 = n1 + n2 + n0 :=
  λ n0 n1 n2,
    pathscomp0 (natplusassoc n0 n1 n2) (natpluscomm n0 (n1 + n2)).

Definition nat_plus_perm210 :
  ∏ n0 n1 n2,
    n0 + n1 + n2 = n2 + n1 + n0 :=
  λ n0 n1 n2,
    pathscomp0 (nat_plus_perm102 n0 n1 n2) (nat_plus_perm120 n1 n0 n2).

Definition nat_mult_perm021 :
  ∏ n0 n1 n2,
    n0 × n1 × n2 = n0 × n2 × n1 :=
  λ n0 n1 n2,
    pathscomp0
      (pathscomp0
         (natmultassoc n0 n1 n2)
         (maponpaths (λ z, n0 × z) (natmultcomm n1 n2)))
      (pathsinv0 (natmultassoc n0 n2 n1)).

Definition nat_mult_perm102 :
  ∏ n0 n1 n2,
    n0 × n1 × n2 = n1 × n0 × n2 :=
  λ n0 n1 n2, maponpaths (λ z, z × n2) (natmultcomm n0 n1).

Definition nat_mult_perm120 :
  ∏ n0 n1 n2,
    n0 × n1 × n2 = n2 × n0 × n1 :=
  λ n0 n1 n2,
    pathscomp0 (natmultcomm (n0 × n1) n2) (pathsinv0 (natmultassoc n2 n0 n1)).

Definition nat_mult_perm201 :
  ∏ n0 n1 n2,
    n0 × n1 × n2 = n1 × n2 × n0 :=
  λ n0 n1 n2,
    pathscomp0 (natmultassoc n0 n1 n2) (natmultcomm n0 (n1 × n2)).

Definition nat_mult_perm210 :
  ∏ n0 n1 n2,
    n0 × n1 × n2 = n2 × n1 × n0 :=
  λ n0 n1 n2,
    pathscomp0 (nat_mult_perm102 n0 n1 n2) (nat_mult_perm120 n1 n0 n2).

Definition minus0r : ∏ n, n - 0 = n :=
  λ n, match n with
             | 0 ⇒ (idpath _)
             | S _ ⇒ (idpath _)
           end.

Definition minusnn0 n : n - n = 0.
Proof.
  induction n as [|n IHn]; [exact (idpath 0) | exact IHn].
Defined.

minus0l and Lemma minussn1 n : (S n) - 1 change to n - 0 should be changed in tactics.

Definition minusgeh n m : n ≥ (n - m).
Proof.
  revert m. induction n as [|n IHn]; intros. apply isreflnatgeh.
  destruct m. rewrite minus0r. apply isreflnatgeh.
  apply (istransnatgeh _ n _). apply natgthtogeh. apply natgthsnn.
  apply IHn.
Defined.

Tactics for rearranging subterms of goals and hypotheses.

Tactics for performing ternary permutations of words written in + and ×.

TACTIC: nat_plus_ternary_perm
SUMMARY: nat_plus_ternary_perm permutes words of length 3 in +.
USAGE: Provided that the current goal is of the form lhs = rhs, nat_plus_ternary_perm x y z will permute a subterm of lhs so that it now appears in the form x + y + z.
EXAMPLE: If the current goal is x + y + z = y + z + x, then nat_plus_ternary_perm y z x will change the goal to y + z + x = y + z + x.
Ltac nat_plus_ternary_perm s t u :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | context[t + s + u] ⇒
          rewrite (nat_plus_perm102 t s u); idtac
        | context[t + u + s] ⇒
          rewrite (nat_plus_perm120 t u s); idtac
        | context[u + s + t] ⇒
          rewrite (nat_plus_perm201 u s t); idtac
        | context[u + t + s] ⇒
          rewrite (nat_plus_perm210 u t s); idtac
        | context[s + u + t] ⇒
          rewrite (nat_plus_perm021 s u t); idtac
        | context[?x + t + s + u] ⇒
          rewrite (natplusassoc x t s); rewrite (natplusassoc x (t + s) u);
          rewrite (nat_plus_perm102 t s u);
          rewrite <- (natplusassoc x (s + t) u);
          rewrite <- (natplusassoc x s t); idtac
        | context[?x + t + u + s] ⇒
          rewrite (natplusassoc x t u); rewrite (natplusassoc x (t + u) s);
          rewrite (nat_plus_perm120 t u s);
          rewrite <- (natplusassoc x (s + t) u);
          rewrite <- (natplusassoc x s t); idtac
        | context[?x + u + s + t] ⇒
          rewrite (natplusassoc x u s); rewrite (natplusassoc x (u + s) t);
          rewrite (nat_plus_perm201 u s t);
          rewrite <- (natplusassoc x (s + t) u);
          rewrite <- (natplusassoc x s t); idtac
        | context[?x + u + t + s] ⇒
          rewrite (natplusassoc x u t); rewrite (natplusassoc x (u + t) s);
          rewrite (nat_plus_perm210 u t s);
          rewrite <- (natplusassoc x (s + t) u);
          rewrite <- (natplusassoc x s t); idtac
        | context[?x + s + u + t] ⇒
          rewrite (natplusassoc x s u); rewrite (natplusassoc x (s + u) t);
          rewrite (nat_plus_perm021 s u t);
          rewrite <- (natplusassoc x (s + t) u);
          rewrite <- (natplusassoc x s t); idtac
      end
  end.

TACTIC: nat_mult_ternary_perm
SUMMARY: nat_mult_ternary_perm permutes words of length 3 in ×.
USAGE: See nat_plus_ternary_perm above.
Ltac nat_mult_ternary_perm s t u :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | context[t × s × u] ⇒
          rewrite (nat_mult_perm102 t s u); idtac
        | context[t × u × s] ⇒
          rewrite (nat_mult_perm120 t u s); idtac
        | context[u × s × t] ⇒
          rewrite (nat_mult_perm201 u s t); idtac
        | context[u × t × s] ⇒
          rewrite (nat_mult_perm210 u t s); idtac
        | context[s × u × t] ⇒
          rewrite (nat_mult_perm021 s u t); idtac
        | context[?x × t × s × u] ⇒
          rewrite (natmultassoc x t s); rewrite (natmultassoc x (t × s) u);
          rewrite (nat_mult_perm102 t s u);
          rewrite <- (natmultassoc x (s × t) u);
          rewrite <- (natmultassoc x s t); idtac
        | context[?x × t × u × s] ⇒
          rewrite (natmultassoc x t u); rewrite (natmultassoc x (t × u) s);
          rewrite (nat_mult_perm120 t u s);
          rewrite <- (natmultassoc x (s × t) u);
          rewrite <- (natmultassoc x s t); idtac
        | context[?x × u × s × t] ⇒
          rewrite (natmultassoc x u s); rewrite (natmultassoc x (u × s) t);
          rewrite (nat_mult_perm201 u s t);
          rewrite <- (natmultassoc x (s × t) u);
          rewrite <- (natmultassoc x s t); idtac
        | context[?x × u × t × s] ⇒
          rewrite (natmultassoc x u t); rewrite (natmultassoc x (u × t) s);
          rewrite (nat_mult_perm210 u t s);
          rewrite <- (natmultassoc x (s × t) u);
          rewrite <- (natmultassoc x s t); idtac
        | context[?x × s × u × t] ⇒
          rewrite (natmultassoc x s u); rewrite (natmultassoc x (s × u) t);
          rewrite (nat_mult_perm021 s u t);
          rewrite <- (natmultassoc x (s × t) u);
          rewrite <- (natmultassoc x s t); idtac
      end
  end.

Tactics for grouping pairs of terms appearing in words written in + and ×.

Helper tactics (which should not be considered as part of the public interface for these tactics).


Ltac nat_plus_not_word s :=
  match s with
    | ?x + ?y ⇒ fail 1
    | _ ⇒ idtac
  end.

Ltac nat_plus_not_at_front t s :=
  match t with
    | s ⇒ fail 1
    | context[s + ?x] ⇒ fail 1
    | _ ⇒ idtac
  end.

Ltac nat_plus_not_at_back t s :=
  match t with
    | s ⇒ fail 1 "A"
    | ?x + s ⇒ fail 1 "B"
    | _ ⇒ idtac
  end.

Ltac nat_plus_move_to_back s :=
  repeat
    let lhs := get_current_lhs in
    nat_plus_not_at_back lhs s;
      match lhs with
        | s + ?x ⇒ rewrite (natpluscomm s x)
        | context[?x + s + ?y] ⇒
          rewrite (nat_plus_perm021 x s y)
        | context[s + ?x + ?y] ⇒
          rewrite (nat_plus_perm201 s x y)
      end.

Ltac nat_plus_move_to_back_in H s :=
  repeat
    let lhs := get_current_lhs_in H in
    nat_plus_not_at_back lhs s;
      match lhs with
        | s + ?x ⇒ rewrite (natpluscomm s x) in H
        | context[?x + s + ?y] ⇒
          rewrite (nat_plus_perm021 x s y) in H
        | context[s + ?x + ?y] ⇒
          rewrite (nat_plus_perm201 s x y) in H
      end.

Ltac nat_plus_move_to_front s :=
  repeat
    let lhs := get_current_lhs in
    nat_plus_not_at_front lhs s;
      match lhs with
        | context[?x + s] ⇒
          nat_plus_not_word x; rewrite (natpluscomm x s)
        | context[?x + ?y + s] ⇒ nat_plus_not_word y;
            rewrite (nat_plus_perm021 x y s)
      end.

Ltac nat_plus_move_to_front_in H s :=
  repeat
    let lhs := get_current_lhs_in H in
    nat_plus_not_at_front lhs s;
      match lhs with
        | context[?x + s] ⇒
          nat_plus_not_word x; rewrite (natpluscomm x s) in H
        | context[?x + ?y + s] ⇒ nat_plus_not_word y;
            rewrite (nat_plus_perm021 x y s) in H
      end.

Ltac nat_plus_move_to_front_goal s :=
  repeat
    let rhs := get_current_rhs in
    nat_plus_not_at_front rhs s;
      match rhs with
        | context[?x + s] ⇒
          nat_plus_not_word x; rewrite (natpluscomm x s)
        | context[?x + ?y + s] ⇒ nat_plus_not_word y;
            rewrite (nat_plus_perm021 x y s)
      end.

Ltac nat_plus_move_to_front_both_in H s :=
  repeat
    let rhs := get_current_rhs_in H in
    nat_plus_not_at_front rhs s;
      match rhs with
        | context[?x + s] ⇒
          nat_plus_not_word x; rewrite (natpluscomm x s) in H
        | context[?x + ?y + s] ⇒ nat_plus_not_word y;
            rewrite (nat_plus_perm021 x y s) in H
      end.

Ltac nat_plus_move_to_back_goal s :=
  repeat
    let rhs := get_current_rhs in
    nat_plus_not_at_back rhs s;
      match rhs with
        | context [s + ?x] ⇒ rewrite (natpluscomm s x)
        | context[?x + s + ?y] ⇒ nat_plus_not_word y;
            rewrite (nat_plus_perm021 x s y)
        | context[s + ?x + ?y] ⇒
          nat_plus_not_word x; nat_plus_not_word y;
          rewrite (nat_plus_perm201 s x y)
      end.

Ltac nat_plus_move_to_back_both_in H s :=
  repeat
    let rhs := get_current_rhs_in H in
    nat_plus_not_at_back rhs s;
      match rhs with
        | context [s + ?x] ⇒ rewrite (natpluscomm s x)
        | context[?x + s + ?y] ⇒ nat_plus_not_word y;
            rewrite (nat_plus_perm021 x s y) in H
        | context[s + ?x + ?y] ⇒
          nat_plus_not_word x; nat_plus_not_word y;
          rewrite (nat_plus_perm201 s x y) in H
      end.

Ltac nat_mult_not_word s :=
  match s with
    | ?x × ?y ⇒ fail 1
    | _ ⇒ idtac
  end.

Ltac nat_mult_not_at_front t s :=
  match t with
    | s ⇒ fail 1
    | context[s × ?x] ⇒ fail 1
    | _ ⇒ idtac
  end.

Ltac nat_mult_not_at_back t s :=
  match t with
    | s ⇒ fail 1 "A"
    | ?x × s ⇒ fail 1 "B"
    | _ ⇒ idtac
  end.

Ltac nat_mult_move_to_back s :=
  repeat
    let lhs := get_current_lhs in
    nat_mult_not_at_back lhs s;
      match lhs with
        | s × ?x ⇒ rewrite (natmultcomm s x)
        | context[?x × s × ?y] ⇒
          rewrite (nat_mult_perm021 x s y)
        | context[s × ?x × ?y] ⇒
          rewrite (nat_mult_perm201 s x y)
      end.

Ltac nat_mult_move_to_back_in H s :=
  repeat
    let lhs := get_current_lhs_in H in
    nat_mult_not_at_back lhs s;
      match lhs with
        | s × ?x ⇒ rewrite (natmultcomm s x) in H
        | context[?x × s × ?y] ⇒
          rewrite (nat_mult_perm021 x s y) in H
        | context[s × ?x × ?y] ⇒
          rewrite (nat_mult_perm201 s x y) in H
      end.

Ltac nat_mult_move_to_front s :=
  repeat
    let lhs := get_current_lhs in
    nat_mult_not_at_front lhs s;
      match lhs with
        | context[?x × s] ⇒
          nat_mult_not_word x; rewrite (natmultcomm x s)
        | context[?x × ?y × s] ⇒ nat_mult_not_word y;
            rewrite (nat_mult_perm021 x y s)
      end.

Ltac nat_mult_move_to_front_in H s :=
  repeat
    let lhs := get_current_lhs_in H in
    nat_mult_not_at_front lhs s;
      match lhs with
        | context[?x × s] ⇒
          nat_mult_not_word x; rewrite (natmultcomm x s) in H
        | context[?x × ?y × s] ⇒ nat_mult_not_word y;
            rewrite (nat_mult_perm021 x y s) in H
      end.

Ltac nat_mult_move_to_front_goal s :=
  repeat
    let rhs := get_current_rhs in
    nat_mult_not_at_front rhs s;
      match rhs with
        | context[?x × s] ⇒
          nat_mult_not_word x; rewrite (natmultcomm x s)
        | context[?x × ?y × s] ⇒ nat_mult_not_word y;
            rewrite (nat_mult_perm021 x y s)
      end.

Ltac nat_mult_move_to_front_both_in H s :=
  repeat
    let rhs := get_current_rhs_in H in
    nat_mult_not_at_front rhs s;
      match rhs with
        | context[?x × s] ⇒
          nat_mult_not_word x; rewrite (natmultcomm x s) in H
        | context[?x × ?y × s] ⇒ nat_mult_not_word y;
            rewrite (nat_mult_perm021 x y s) in H
      end.

Ltac nat_mult_move_to_back_goal s :=
  repeat
    let rhs := get_current_rhs in
    nat_mult_not_at_back rhs s;
      match rhs with
        | context [s × ?x] ⇒ rewrite (natmultcomm s x)
        | context[?x × s × ?y] ⇒ nat_mult_not_word y;
            rewrite (nat_mult_perm021 x s y)
        | context[s × ?x × ?y] ⇒
          nat_mult_not_word x; nat_mult_not_word y;
          rewrite (nat_mult_perm201 s x y)
      end.

Ltac nat_mult_move_to_back_both_in H s :=
  repeat
    let rhs := get_current_rhs_in H in
    nat_mult_not_at_back rhs s;
      match rhs with
        | context [s × ?x] ⇒ rewrite (natmultcomm s x)
        | context[?x × s × ?y] ⇒ nat_mult_not_word y;
            rewrite (nat_mult_perm021 x s y) in H
        | context[s × ?x × ?y] ⇒
          nat_mult_not_word x; nat_mult_not_word y;
          rewrite (nat_mult_perm201 s x y) in H
      end.

The tactics.

We employ the following naming conventions. By default a tactics given pertain only to equations and operate by default on the left-hand side of equations. Those that operate on both left- and right-hand sides of the goal are suffixed with _goal. Tactics that operate on the left-hand side of equations occurring as hypotheses are suffixed with _in. Those that operate on both left- and right-hand sides of equations occurring as hypotheses are suffixed with _both_in. Those that opexrate on all sides of goals and hypotheses are suffixeD with _all.

Ltac nat_plus_group s t :=
  nat_plus_move_to_front t; nat_plus_move_to_front s.

Ltac nat_plus_group_goal s t :=
  nat_plus_move_to_front_goal t; nat_plus_move_to_front_goal s.

Ltac nat_plus_group_in H s t :=
  nat_plus_move_to_front_in H t; nat_plus_move_to_front_in H s.

Ltac nat_plus_group_both_in H s t :=
  nat_plus_move_to_front_both_in H t; nat_plus_move_to_front_both_in H s.

Ltac nat_plus_group_all s t :=
  nat_plus_group_goal s t;
  repeat
    match goal with
      | H : _ |- _ ⇒ nat_plus_group_both_in H s t
    end.

t is a term of type nat and nat_plus_group_as attempts to reorganize the lhs of the goal to include as a subterm t.
Ltac nat_plus_group_as t :=
  match t with
    | ?x + ?y ⇒
      nat_plus_not_word y; nat_plus_move_to_front y;
      nat_plus_group_as x
    | ?x ⇒ nat_plus_not_word x; nat_plus_move_to_front x
  end.

t is a term of type x = y for x, y : nat and nat_plus_group_from attempts to reogranize the lhs of the goal to include as a subterm x.
Ltac nat_plus_group_from t :=
  let T := type of t in
  match T with
    | ?lhs = ?rhs ⇒ nat_plus_group_as lhs
  end.

Ltac nat_mult_group s t :=
  nat_mult_move_to_front t; nat_mult_move_to_front s.

Ltac nat_mult_group_goal s t :=
  nat_mult_move_to_front_goal t; nat_mult_move_to_front_goal s.

Ltac nat_mult_group_in H s t :=
  nat_mult_move_to_front_in H t; nat_mult_move_to_front_in H s.

Ltac nat_mult_group_both_in H s t :=
  nat_mult_move_to_front_both_in H t; nat_mult_move_to_front_both_in H s.

Ltac nat_mult_group_all s t :=
  nat_mult_group_goal s t;
  repeat
    match goal with
      | H : _ |- _ ⇒ nat_mult_group_both_in H s t
    end.

t is a term of type nat and nat_mult_group_as attempts to reorganize the lhs of the goal to include as a subterm t.
Ltac nat_mult_group_as t :=
  match t with
    | ?x + ?y ⇒
      nat_mult_not_word y; nat_mult_move_to_front y;
      nat_mult_group_as x
    | ?x ⇒ nat_mult_not_word x; nat_mult_move_to_front x
  end.

t is a term of type x = y for x y : nat and nat_mult_group_from attempts to reogranize the lhs of the goal to include as a subterm x.
Ltac nat_mult_group_from t :=
  let T := type of t in
  match T with
    | ?lhs = ?rhs ⇒ nat_mult_group_as lhs
  end.

Tactics pertaining to inequalities.

Preprocessing of the ambient goal and hypotheses.

Helper tactics (which should not be considered as part of the public interface for these tactics).

Ltac does_not_have_gth x y :=
  match goal with
    | _ : hProptoType (x > y) |- _ ⇒ fail 1
    | |- _ ⇒ idtac
  end.

Ltac does_not_have_geh x y :=
  match goal with
    | _ : hProptoType (x ≥ y) |- _ ⇒ fail 1
    | |- _ ⇒ idtac
  end.

It is convenient to have to only work with either hzgth/hzgeh or hzlth/hzleh. We choose the former and the following tactics replace instances of hzlth/hzleh with the corresponding inequalities involving hzgth/hzgeh.
Ltac reverse_lth :=
  repeat
    match goal with
      | H : hProptoType (?y < ?u) |- _ ⇒
        does_not_have_gth u y; assert (natgth u y); [apply H | ]
    end.

Ltac reverse_leh :=
  repeat
    match goal with
      | H : hProptoType (?y ≤ ?u) |- _ ⇒
        does_not_have_geh u y; assert (natgeh u y); [apply H | ]
    end.

Ltac gth_to_geh :=
  repeat
    match goal with
      | H : hProptoType (?x > ?y) |- _ ⇒
        does_not_have_geh x y; assert (natgeh x y);
        [apply natgthtogeh; assumption |]
    end.

Clean the hypotheses in preparation for searching.
Ltac nat_dfs_clean := reverse_lth; reverse_leh; gth_to_geh.

Tactics for solving inequalities involving natural numbers.

Tactics for solving very simple inequalities using known lemmas.

The following tactic allows immediate solution of common goals involving natgth provided that the appropriate hypotheses are available. We probably want to eventually add additional "hints" here.
Ltac natgth_simple :=
  match goal with
    | _ : hProptoType (?x > ?y) |- hProptoType (?x > ?y) ⇒ assumption
    | P : hProptoType ((S ?x) > (S ?y)) |- hProptoType (?x > ?y) ⇒ apply P
    | |- hProptoType ((S ?x) > ?x) ⇒ apply (natgthsnn x)
    | |- hProptoType ((S ?x) > 0) ⇒ apply (natgthsn0 x)
    | P : hProptoType (?x > ?y) |- hProptoType ((S ?x) > (S ?y)) ⇒ apply P
    | P : hProptoType (?x ≠ 0)%nat |- hProptoType (?x > 0) ⇒
      apply (natneq0togth0 x P)
    | P : hProptoType (0 ≠ ?x)%nat |- hProptoType (?x > 0) ⇒
      apply (natneq0togth0 x (natneqtwist x P))
    | P : (?x = 0) → empty |- hProptoType (?x > 0) ⇒
      apply (natneq0togth0 x P)
    | P : (0 = ?x) → empty |- hProptoType (?x > 0) ⇒
      apply (natneq0togth0 x (natneqtwist x P))
    | |- hProptoType ((S ?x) > ?x) ⇒ apply (natgthsnn x)
    | P : hProptoType (?x > ?y) |- hProptoType ((S ?x) > ?y) ⇒
      apply (natgthtogths x y P)
    | P : hProptoType (?x ≥ ?y) |- hProptoType ((S ?x) > ?y) ⇒
      apply (natgehtogthsn x y P)
    | P : hProptoType (?x > ?y),
          Q : hProptoType (?y > ?z) |- hProptoType (?x > ?z) ⇒
      apply (istransnatgth x y z P Q)
    | P : hProptoType (?x > ?y),
          Q : hProptoType (?y ≥ ?z) |- hProptoType (?x > ?z) ⇒
      apply (natgthgehtrans x y z P Q)
    | P : hProptoType (?x ≥ ?y),
          Q : hProptoType (?y > ?z) |- hProptoType (?x > ?z) ⇒
      apply (natgehgthtrans x y z P Q)
  end.

Ltac natgeh_simple :=
  match goal with
    | _ : hProptoType (?x ≥ ?y) |- hProptoType (?x ≥ ?y) ⇒ assumption
    | P : hProptoType (?x ≥ ?y) |- hProptoType ((S ?x) ≥ (S ?y)) ⇒ apply P
    | P : hProptoType ((S ?x) ≥ (S ?y)) |- hProptoType (?x ≥ ?y) ⇒
      apply P
    | |- hProptoType (?x ≥ ?x) ⇒ apply isreflnatgeh
    | |- hProptoType (?x ≥ 0) ⇒ apply natgehn0
    | |- hProptoType ((S ?x) ≥ ?x) ⇒ apply (natgehsnn x)
    | |- hProptoType (?x ≥ ?x - ?y) ⇒ apply (minusgeh x y)
    | H : hProptoType (?x > ?y) |- hProptoType (?x ≥ ?y) ⇒
      apply (natgthtogeh x y H)
    | P : hProptoType (?x ≥ ?y),
          Q : hProptoType (?y ≥ ?z) |- hProptoType (?x ≥ ?z) ⇒
      apply (istransnatgeh x y z P Q)
    | P : hProptoType ((S ?x) > ?y) |- hProptoType (?x ≥ ?y) ⇒
      apply (natgthsntogeh x y P)
  end.

General tactics for solving inequalities by depth-first search.

The approach taken here for solving inequalities is to construct from the given collection of hypotheses HH a corresponding directed graph and then to perform a depth-first search of the graph.
Although we will often employ our search method in order to traverse an acyclic graph, when we are proving that the hypotheses imply empty we are forced to consider the cyclic case. In these cases it may be possible to become trapped in a cycle. To prevent this from happening we must build helper functions that will allow us to check that the next goal we move to is not one we have previously considered.
Ltac make_gth_check x y :=
  let f T :=
      match T with
        | hProptoType (x > y) ⇒ fail 1
        | _ ⇒ idtac
      end
  in f.

Ltac make_geh_check x y :=
  let f T :=
      match T with
        | hProptoType (x ≥ y) ⇒ fail 1
        | _ ⇒ idtac
      end
  in f.

Perform depth first search of the graph corresponding to the hypotheses. In standard continuation passing style we allow a helper ltac function f which is admitted to perform certain checks (or which can be ignored as in nat_dfs below).
TODO: Try instead change. Think about strengthening clauses.
Ltac nat_dfs_body f :=
  natgth_simple
    || natgeh_simple
    || match goal with
         | |- hProptoType (?x < ?y) ⇒
           let X := fresh "X" in
           assert (natgth y x) as X; [nat_dfs_body f | apply X]
         | |- hProptoType (?x ≤ ?y) ⇒
           let X := fresh "X" in
           assert (natgeh y x) as X; [nat_dfs_body f | apply X]
         | _ : hProptoType (?u > ?y) |- hProptoType (?x > ?y) ⇒
           f (hProptoType (x ≥ u));
             let g := make_geh_check x u in
             let h := check_cons g f in
             apply (natgehgthtrans x u y); [nat_dfs_body h | assumption]
         | |- hProptoType (?x ≥ ?y) ⇒ f (hProptoType(x ≥ y));
             let g := make_geh_check x y in
             let h := check_cons g f in
             apply (natgthtogeh x y); nat_dfs_body h
         | _ : hProptoType (?u ≥ ?y) |- hProptoType (?x ≥ ?y) ⇒
           f (hProptoType (x ≥ u));
             let g := make_geh_check x u in
             let h := check_cons g f in
             apply (istransnatgeh x u y); [nat_dfs_body h | assumption]
         | _ : hProptoType (?x ≥ ?u) |- hProptoType (?x > ?y) ⇒
           f (hProptoType (u > y));
             let g := make_gth_check u y in
             let h := check_cons g f in
             apply (natgehgthtrans x u y); [assumption | nat_dfs_body h]
         | _ : hProptoType (?u ≥ ?y) |- hProptoType (?x > ?y) ⇒
           f (hProptoType (x > u));
             let g := make_gth_check x u in
             let h := check_cons g f in
             apply (natgthgehtrans x u y); [nat_dfs_body h | assumption]
         | |- hProptoType (?x ≥ S ?y) ⇒
           apply natgthtogehsn; nat_dfs_body f
         | |- hProptoType ((S ?x) > ?y) ⇒
           let g := make_geh_check x y in
           let h := check_cons g f in
           (apply (natgthgehtrans _ x _); [apply natlthnsn | nat_dfs_body h])

         | |- hProptoType (?x > ?y - ?z) ⇒
           let g := make_gth_check x (y - z) in
           let h := check_cons g f in
           apply (natgthgehtrans x y (y - z));
             [nat_dfs_body h | apply minusgeh]
       end.

Ltac nat_dfs := nat_dfs_clean; nat_dfs_body id_check.

Tactics for deriving contradictions.

Ltac nat_eq_contr :=
  let f X := assert empty; [apply X; assumption | contradiction] in
  let i X := assert empty; [apply X; apply idpath | contradiction] in
  match goal with
    | H : ?x = ?y → empty, _ : ?x = ?y |- _ ⇒ f H
    | H : neg (?x = ?y), _ : ?x = ?y |- _ ⇒ f H
    | H : ?x = ?x → empty |- _ ⇒ i H
    | H : neg (?x = ?x) |- _ ⇒ i H
    | H : hProptoType (?x ≠ ?y)%nat, _ : ?x = ?y |- _ ⇒ f H
    | H : hProptoType (?x ≠ ?x)%nat |- _ ⇒ i H
    | H : hProptoType (?x ≠ ?y)%nat, _ : ?x = ?y |- _ ⇒ f H
    | H : hProptoType (?x ≠ ?x)%nat |- _ ⇒ i H
  end.

Ltac nat_simple_contr :=
  assert empty; [
    match goal with
      | H : hProptoType (?x < 0) |- _ ⇒ exact (negnatlthn0 x H)
      | H : hProptoType (0 > ?x) |- _ ⇒ exact (negnatgth0n x H)
      | H : hProptoType ((S ?x) ≤ 0) |- _ ⇒ exact (negnatlehsn0 x H)
      | H : hProptoType (0 ≥ (S ?x)) |- _ ⇒ exact (negnatgeh0sn x H)
      | H : S ?x = 0 |- _ ⇒ exact (negpathssx0 x H)
    end | contradiction].

Note that the following tactic may not halt. SHOULD halt now.
Ltac nat_ineq_contr_isirrefl :=
  nat_dfs_clean;
  assert empty; [
    match goal with
      | _ : hProptoType (?x > ?x) |- _ ⇒ apply (isirreflnatgth x); assumption
      | N : nat |- _ ⇒
        let f := make_gth_check N N in
        apply (isirreflnatgth N); nat_dfs_body ltac:(f)
    end
  | contradiction].

Ltac nat_absurd :=
  (nat_simple_contr || nat_eq_contr || nat_ineq_contr_isirrefl).

Ltac nat_preclean_1 :=
  repeat
    match goal with
      | |- context [0 - ?n] ⇒ change (0 - n) with 0
      | |- context [(S ?n) - 1] ⇒ change ((S n) - 1) with (n - 0)
      | |- context[S ?x - S ?y] ⇒ change (S x - S y) with (x - y)
    end.

Ltac nat_preclean_2 :=
  repeat rewrite multsnm; repeat rewrite multnsm;
  repeat rewrite natldistr; repeat rewrite natrdistr;
  repeat rewrite natmultn0; repeat rewrite natmult0n;
  repeat rewrite natplusl0; repeat rewrite natplusr0;
  repeat rewrite natminuseqn; repeat rewrite natmultl1;
  repeat rewrite natmultr1; repeat rewrite <- natplusassoc;
  repeat rewrite <- natmultassoc; repeat rewrite minus0r;
  repeat rewrite minusnn0.

Ltac nat_clean := nat_preclean_1; nat_preclean_2.

Ltac nat_preclean_1_in H :=
  repeat
    let T := type of H in
    match T with
      | context [0 - ?n] ⇒ change (0 - n) with 0 in H
      | context [(S ?n) - 1] ⇒ change ((S n) - 1) with (n - 0) in H
      | context[S ?x - S ?y] ⇒ change (S x - S y) with (x - y) in H
    end.

Ltac nat_preclean_2_in H :=
  repeat rewrite multsnm in H; repeat rewrite multnsm in H;
  repeat rewrite natldistr in H; repeat rewrite natrdistr in H;
  repeat rewrite natmultn0 in H; repeat rewrite natmult0n in H;
  repeat rewrite natplusl0 in H; repeat rewrite natplusr0 in H;
  repeat rewrite natminuseqn in H; repeat rewrite natmultl1 in H;
  repeat rewrite natmultr1 in H; repeat rewrite <- natplusassoc in H;
  repeat rewrite <- natmultassoc in H; repeat rewrite minus0r in H;
  repeat rewrite minusnn0 in H.

Ltac nat_clean_in H := nat_preclean_1_in H; nat_preclean_2_in H.

Ltac nat_clean_all :=
  nat_clean;
  repeat
    match goal with
      | H : _ |- _ ⇒ nat_clean_in H
    end.

Several somewhat devious experimental tactics.


Ltac nat_devious_ineq :=
  match goal with
    | |- hProptoType (?x > ?y) ⇒
      destruct (natgthorleh x y); [assumption | nat_absurd]
    | |- hProptoType (?x ≥ ?y) ⇒
      destruct (natlthorgeh x y); [nat_absurd | assumption]
    | |- hProptoType (?x < ?y) ⇒
      destruct (natlthorgeh x y); [assumption | nat_absurd]
    | |- hProptoType (?x ≤ ?y) ⇒
      destruct (natgthorleh x y); [nat_absurd | assumption]
  end.

Tactics for solving equations.

Helper tactics.

Ltac make_check T :=
  let f S :=
      match S with
        | T ⇒ fail 1
      end
  in f.

Ltac nat_plus_strip :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | context [?x] ⇒
          match rhs with
            | context [x] ⇒ nat_plus_move_to_back_goal x;
                apply (ap (λ v, v + x))
          end
      end
  end.

Ltac nat_mult_strip :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | context [?x] ⇒
          match rhs with
            | context [x] ⇒ nat_mult_move_to_back_goal x;
                apply (ap (λ v, v × x))
          end
      end
  end.

Some simple solver tactics which are concerned exclusively with equations involving only + or only ×.

Ltac nat_plus_prezap_body f :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | rhs ⇒ apply idpath
        | 0 ⇒ apply pathsinv0; nat_plus_prezap_body f
        | ?x + ?y ⇒
          match rhs with
            | y + x ⇒ apply (natpluscomm x y)
          end
        | _ ⇒ (nat_plus_strip; nat_plus_prezap_body f)
      end
    | E : ?l = ?r |- ?lhs = ?rhs ⇒ f E;
        let g := make_hyp_check E in
        let h := check_cons g f in
        nat_plus_group_from E; matched_rewrite E; nat_plus_prezap_body h
  end.

Ltac nat_plus_prezap := nat_clean_all; nat_plus_prezap_body id_check.

Ltac nat_mult_prezap_body f :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | rhs ⇒ apply idpath
        | 0 ⇒ apply pathsinv0; nat_mult_prezap_body f
        | ?x × ?y ⇒
          match rhs with
            | y × x ⇒ apply (natmultcomm x y)
          end
        | _ ⇒ (nat_mult_strip; nat_mult_prezap_body f)
      end
    | E : ?l = ?r |- ?lhs = ?rhs ⇒ f E;
        let g := make_hyp_check E in
        let h := check_cons g f in
        nat_mult_group_from E; matched_rewrite E; nat_mult_prezap_body h
  end.

Ltac nat_mult_prezap := nat_clean_all; nat_mult_prezap_body id_check.

A simple solver tactic for mixed + × equations.


Ltac nat_plus_zap_body f :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match rhs with
        | ?x + ?y ⇒ nat_plus_not_word y;
            match lhs with
              | ?u + ?v ⇒
                (nat_plus_not_word v;
                 let F := fresh in
                 assert (v = y) as F;
                 [ nat_mult_prezap
                 | rewrite F; apply (ap (λ v, v + y));
                   nat_plus_zap_body f
                 ])
                  || (let l := get_current_lhs in
                      let g := make_check l in
                      let h := check_cons f g in
                      nat_plus_move_to_front v; nat_plus_zap_body h)
            end
        | ?x ⇒ nat_plus_not_word x;
            match lhs with
              | ?v ⇒ nat_plus_not_word v; nat_mult_prezap
            end
      end
  end.

Ltac nat_plus_zap := nat_plus_zap_body id_check.

Combined tactics for solving equations and inequalities of natural numbers.


Ltac nat_simple :=
  match goal with
    | H : hProptoType (?n ≤ 0) |- ?n = 0 ⇒ apply (natleh0tois0 n H)
    | H : hProptoType (0 ≥ ?n) |- ?n = 0 ⇒ apply (nat0gehtois0 n H)
    | H : hProptoType (?n ≤ 0) |- 0 = ?n ⇒
      apply pathsinv0; apply (natleh0tois0 n H)
    | H : hProptoType (0 ≥ ?n) |- 0 = ?n ⇒
      apply pathsinv0; apply (nat0gehtois0 n H)
    | |- ?x + ?y = ?y + ?x ⇒ apply natpluscomm
  end.

Ltac nat_intros :=
  repeat match goal with
           | |- ?x → ?y ⇒ intro
           | |- ∏ _, _ ⇒ intro
         end.

Ltac nat_try :=
  repeat
    match goal with
      | H : _ |- _ ⇒
        let T := type of H in
        match T with
          | nat ⇒ fail 1
          | _ ⇒ idtac "About to try " H; apply H
        end
    end.

Ltac nat_basic_destruct N := destruct N; nat_intros; nat_clean;
                             (auto || assumption || nat_simple || nat_absurd
                                   || nat_dfs ).

Ltac nat_basic_induction N := induction N; nat_intros; nat_clean;
                              (auto || assumption || nat_simple || nat_absurd
                                    || nat_dfs || nat_try ).

Ltac nat_zap :=
  nat_clean_all;
  try (auto || assumption || nat_simple || nat_absurd || nat_dfs
            || nat_plus_zap || nat_try);
  match goal with
    | N : nat |- _ ⇒
      nat_basic_destruct N || nat_basic_induction N
  end.

Close Scope nat_scope.

TESTS