src/CoqUp/Tactics.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Module Tactics.

  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.
  
End Tactics.
Export Tactics.