Require Export Coq.Bool.Bool.
Require Export Coq.Lists.List.
Require Export Coq.Strings.String.
Require Export Coq.ZArith.ZArith.
Require Export Coq.ZArith.Znumtheory.
Require Import Coq.micromega.Lia.

Require Export TVSMT.Coqlib.
(* Require Import compcert.lib.Integers. *)
Require Export TVSMT.Errors.

(* This tactic due to Clement Pit-Claudel with some minor additions by JDP to
   allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *)
Inductive Learnt {A: Type} (a: A) :=
  | AlreadyKnown : Learnt a.

Ltac learn_tac fact name :=
  lazymatch goal with
  | [ H: Learnt fact |- _ ] =>
    fail 0 "fact" fact "has already been learnt"
  | _ => let type := type of fact in
        lazymatch goal with
        | [ H: @Learnt type _ |- _ ] =>
          fail 0 "fact" fact "of type" type "was already learnt through" H
        | _ => let learnt := fresh "Learn" in
              pose proof (AlreadyKnown fact) as learnt; pose proof fact as name
        end
  end.

Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name.
Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name.

Ltac unfold_rec c := unfold c; fold c.

Ltac solve_by_inverts n :=
  match goal with | H : ?T |- _ =>
    match type of T with Prop =>
      inversion H;
      match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end
    end
  end.

Ltac solve_by_invert := solve_by_inverts 1.

Ltac invert x := inversion x; subst; clear x.

Ltac destruct_match :=
  match goal with
  | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:?
  | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:?
  end.

Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence.

Ltac nicify_hypotheses :=
  repeat match goal with
         | [ H : ex _ |- _ ] => invert H
         | [ H : Some _ = Some _ |- _ ] => invert H
         | [ H : OK _ = OK _ |- _ ] => invert H
         | [ H : ?x = ?x |- _ ] => clear H
         | [ H : _ /\ _ |- _ ] => invert H
         | [ H : (_, _) = (_, _) |- _ ] => invert H
         end.

Ltac nicify_goals :=
  repeat match goal with
         | [ |- _ /\ _ ] => split
         | [ |- Some _ = Some _ ] => f_equal
         | [ |- OK _ = OK _ ] => f_equal
         | [ |- S _ = S _ ] => f_equal
         end.

Ltac kill_bools :=
  repeat match goal with
         | [ H : _ && _ = true |- _ ] => apply andb_prop in H
         | [ H : _ || _ = false |- _ ] => apply orb_false_elim in H
         | [ H : negb _ = true |- _ ] => apply negb_true_iff in H
         | [ H : negb _ = false |- _ ] => apply negb_false_iff in H

         | [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H
         | [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H
         | [ H : _ <? _ = true |- _ ] => apply Z.ltb_lt in H
         | [ H : _ <? _ = false |- _ ] => apply Z.ltb_ge in H
         | [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H
         | [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H

         | [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H
         | [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H

         | [ H : (_ <=? _)%positive = true |- _ ] => apply Pos.leb_le in H
         | [ H : (_ <=? _)%positive = false |- _ ] => apply Pos.leb_gt in H
         | [ H : (_ <? _)%positive = true |- _ ] => apply Pos.ltb_lt in H
         | [ H : (_ <? _)%positive = false |- _ ] => apply Pos.ltb_ge in H

         | [ H : (_ =? _)%positive = true |- _ ] => apply Pos.eqb_eq in H
         | [ H : (_ =? _)%positive = false |- _ ] => apply Pos.eqb_neq in H
         end.

Ltac substpp :=
  repeat match goal with
         | [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] =>
           let EQ := fresh "EQ" in
           learn H1 as EQ; rewrite H2 in EQ; invert EQ
         | _ => idtac
         end.

Ltac simplify := intros; simpl in *;
                 repeat progress (try nicify_hypotheses; try nicify_goals; try kill_bools; substpp);
                 simpl in *.

Ltac crush := simplify; try discriminate; try congruence; try (zify; lia);
              try assumption; try (solve [auto]).

Ltac ecrush m := simplify; try discriminate; try congruence; try (zify; lia);
                 try assumption; try (solve [eauto with m]).