Library Tact
Copyright (c) 2018 by Karl Crary
Permission is hereby granted, free of charge, to any person obtaining
a copy of this software and associated documentation files (the
"Software"), to deal in the Software without restriction, including
without limitation the rights to use, copy, modify, merge, publish,
distribute, sublicense, and/or sell copies of the Software, and to
permit persons to whom the Software is furnished to do so, subject to
the following conditions:
The above copyright notice and this permission notice shall be
included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
UIP
Lemma inj_pair2_UIP :
forall (A : Type),
(forall (x y : A) (p1 p2 : x = y), p1 = p2)
-> forall (P : A -> Type) (p : A) (x y: P p),
existT P p x = existT P p y
-> x = y.
Hint Resolve UIP_dec : uip.
Simpler induction.
Tactic Notation "clear" "codependent" hyp(H)
:=
let T := type of H
in
clear H;
repeat
(match goal with
x:_ |- _ =>
(match T with
context [x] =>
This might fail because:
x is mentioned in a hyp that should have been reverted but wasn't,
so leaving it is necessary; orx is fixed (ie, non-inductive) argument to H,
so leaving it is actually desired.
clear x
end)
end).
Tactic Notation "induct" hyp(H)
:=
elim H;
clear codependent H.
Tactic Notation "cases" hyp(H)
:=
case H;
clear codependent H.
Tactic Notation "induct" hyp(H) "using" constr(ind)
:=
elim H using ind;
clear codependent H.
Tactic Notation "wfinduct" hyp(H) "using" constr(T) :=
revert H;
match goal with
| |- forall x, @?P x => apply (well_founded_ind T P)
end.
end)
end).
Tactic Notation "induct" hyp(H)
:=
elim H;
clear codependent H.
Tactic Notation "cases" hyp(H)
:=
case H;
clear codependent H.
Tactic Notation "induct" hyp(H) "using" constr(ind)
:=
elim H using ind;
clear codependent H.
Tactic Notation "wfinduct" hyp(H) "using" constr(T) :=
revert H;
match goal with
| |- forall x, @?P x => apply (well_founded_ind T P)
end.
Better inversion
Intro down to marker, split equalities, subst redundant variables, and revert back.
Ltac invproc stac rtac :=
(lazymatch goal with
| |- Marker_invert -> _ => intros _; stac; rtac
| |- ?x = ?x -> _ => intros _; invproc stac rtac
| |- existT _ ?p ?x = existT _ ?p ?y -> _ =>
let H := fresh "Heq" in
let H' := fresh
in
intro H;
first
[
assert (x = y) as H';
[
refine (inj_pair2_UIP _ _ _ _ _ _ H); auto with uip eqdec; fail
|
clear H;
revert H';
invproc stac rtac
]
|
invproc stac ltac:(try (revert H); rtac)
]
| |- _ = _ -> _ =>
let H := fresh "Heq"
in
intro H;
first
[
injection H;
clear H;
invproc stac rtac
|
invproc stac ltac:(try (revert H); rtac)
]
| |- forall (x : _), _ =>
let y := fresh x
in
intro y;
invproc ltac:(try (subst y); stac) ltac:(try (revert y); rtac)
end).
Tactic Notation "invert" constr(t) :=
let Hinv := fresh in
let Hgoal := fresh in
let Hmark1 := fresh in
let Hmark2 := fresh
in
(lazymatch goal with
| |- Marker_invert -> _ => intros _; stac; rtac
| |- ?x = ?x -> _ => intros _; invproc stac rtac
| |- existT _ ?p ?x = existT _ ?p ?y -> _ =>
let H := fresh "Heq" in
let H' := fresh
in
intro H;
first
[
assert (x = y) as H';
[
refine (inj_pair2_UIP _ _ _ _ _ _ H); auto with uip eqdec; fail
|
clear H;
revert H';
invproc stac rtac
]
|
invproc stac ltac:(try (revert H); rtac)
]
| |- _ = _ -> _ =>
let H := fresh "Heq"
in
intro H;
first
[
injection H;
clear H;
invproc stac rtac
|
invproc stac ltac:(try (revert H); rtac)
]
| |- forall (x : _), _ =>
let y := fresh x
in
intro y;
invproc ltac:(try (subst y); stac) ltac:(try (revert y); rtac)
end).
Tactic Notation "invert" constr(t) :=
let Hinv := fresh in
let Hgoal := fresh in
let Hmark1 := fresh in
let Hmark2 := fresh
in
Keep inversion from messing with the goal.
(lazymatch goal with
| |- ?T => change (let Hgoal := T in Hgoal); intro Hgoal
end);
pose proof t as Hinv;
assert Marker_invert as Hmark1; [exact I | pose proof Hmark1 as Hmark2; revert Hmark2];
inversion Hinv;
clear Hinv;
subst Hgoal;
| |- ?T => change (let Hgoal := T in Hgoal); intro Hgoal
end);
pose proof t as Hinv;
assert Marker_invert as Hmark1; [exact I | pose proof Hmark1 as Hmark2; revert Hmark2];
inversion Hinv;
clear Hinv;
subst Hgoal;
Put the goal back.
repeat
(lazymatch goal with
| H : ?T |- _ =>
(lazymatch T with
| Marker_invert => fail
| _ => revert H
end)
end);
clear Hmark1;
invproc idtac idtac.
Tactic Notation "invertc" hyp(H) :=
invert H; clear H.
(lazymatch goal with
| H : ?T |- _ =>
(lazymatch T with
| Marker_invert => fail
| _ => revert H
end)
end);
clear Hmark1;
invproc idtac idtac.
Tactic Notation "invertc" hyp(H) :=
invert H; clear H.
Use a hypothesis/lemma.
Ltac exploit_main t T pat cleanup
:=
(lazymatch T with
| ?U1 -> ?U2 =>
let H := fresh
in
assert U1 as H;
[cleanup () | exploit_main (t H) U2 pat ltac:(fun _ => clear H; cleanup ())]
| _ =>
pose proof t as pat;
cleanup ()
end).
Tactic Notation "exploit" constr(t) "as" simple_intropattern(pat)
:=
exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
Tactic Notation "exploit" constr(t)
:=
let H := fresh "H"
in
exploit_main t ltac:(type of t) H ltac:(fun _ => idtac).
Tactic Notation "so" constr(T) "as" simple_intropattern(pat)
:=
pose proof T as pat.
Tactic Notation "so" constr(T)
:=
pose proof T.
Misc
Lemma eq_fn_apply :
forall {T U : Type} {x y : T} (f : T -> U),
x = y
-> f x = f y.
Ltac force_exact H :=
(match goal with
| |- ?C =>
let D := type of H
in
replace C with D; [exact H |]
end).
Ltac do2_main n tac :=
(lazymatch n with
| 0 => idtac
| S ?n' => tac; [| do2_main n' tac]
end).
Tactic Notation "do2" constr(n) tactic3(tac)
:=
do2_main n tac.
Ltac repeat2_main tac :=
try (tac; [| repeat2_main tac]).
Tactic Notation "repeat2" tactic3(tac)
:=
repeat2_main tac.
Tactic Notation "renameover" hyp(H1) "into" hyp(H2) :=
clear H2; rename H1 into H2.
Tactic Notation "injectionc" hyp(H) :=
injection H; clear H.
Ltac destruct_all_main H :=
(lazymatch type of H with
| exists _:_, _ =>
let H' := fresh "x"
in
destruct H as [H' H]; destruct_all_main H'; destruct_all_main H
| _ /\ _ => let H' := fresh "H"
in
destruct H as [H' H]; destruct_all_main H'; destruct_all_main H
| prod _ _ =>
let H' := fresh "x"
in
destruct H as [H' H]; destruct_all_main H'; destruct_all_main H
| _ => idtac
end).
Ltac destruct_all t :=
first [
destruct_all_main t
|
let H := fresh
in
pose proof t as H;
destruct_all_main H
].
Ltac done := fail.
Notation
Definition car {P Q : Prop} (x : P /\ Q) : P.
Defined.
Definition cdr {P Q : Prop} (x : P /\ Q) : Q.
Defined.
Notation "a 'andel'" := (car a)
(at level 11, left associativity, only parsing) : tactics_scope.
Notation "a 'ander'" := (cdr a)
(at level 11, left associativity, only parsing) : tactics_scope.
Open Scope tactics_scope.
Notation "a 'anderl'" := (a ander andel)
(at level 11, left associativity, only parsing) : tactics_scope.
Notation "a 'anderr'" := (a ander ander)
(at level 11, left associativity, only parsing) : tactics_scope.
Notation "a 'anderrl'" := (a ander ander andel)
(at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#2 " := (x _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#3 " := (x _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#4 " := (x _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#5 " := (x _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#6 " := (x _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#7 " := (x _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#8 " := (x _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#9 " := (x _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#10 " := (x _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#11 " := (x _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#12 " := (x _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#13 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#14 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#15 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#16 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#17 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#18 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#19 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.
Notation " x _#20 " := (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (at level 11, left associativity, only parsing) : tactics_scope.