Library prosa.util.tactics
Lemmas & tactics adopted (with permission) from V. Vafeiadis' Vbase.v.
Lemma neqP: ∀ (T: eqType) (x y: T), reflect (x ≠ y) (x != y).
Ltac ins := simpl in *; try done; intros.
(* ************************************************************************** *)
(* ************************************************************************** *)
Exploit an assumption (adapted from CompCert).
Lemma modusponens : ∀ (P Q : Prop), P → (P → Q) → Q.
Ltac exploit x :=
refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _) _)
|| refine (modusponens _ _ (x _ _) _)
|| refine (modusponens _ _ (x _) _).
(* This tactic feeds the precondition of an implication in order to derive the conclusion
(taken from http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/7013).
Usage: feed H.
H: P -> Q ==becomes==> H: P
____
Q
After completing this proof, Q becomes a hypothesis in the context. *)
Ltac feed H :=
match type of H with
| ?foo → _ ⇒
let FOO := fresh in
assert foo as FOO; [|specialize (H FOO); clear FOO]
end.
(* Generalization of feed for multiple hypotheses.
feed_n is useful for accessing conclusions of long implications.
Usage: feed_n 3 H.
H: P1 -> P2 -> P3 -> Q.
We'll be asked to prove P1, P2 and P3, so that Q can be inferred. *)
Ltac feed_n n H := match constr:(n) with
| O ⇒ idtac
| (S ?m) ⇒ feed H ; [| feed_n m H]
end.
(* ************************************************************************** *)
(* ************************************************************************** *)
Ltac move_neq_down H :=
exfalso;
(move: H; rewrite ltnNge; move ⇒ /negP H; apply: H; clear H)
|| (move: H; rewrite leqNgt; move ⇒ /negP H; apply: H; clear H).
Ltac move_neq_up H :=
(rewrite ltnNge; apply/negP; intros H)
|| (rewrite leqNgt; apply/negP; intros H).
Ltac move_neq_down H :=
exfalso;
(move: H; rewrite ltnNge; move ⇒ /negP H; apply: H; clear H)
|| (move: H; rewrite leqNgt; move ⇒ /negP H; apply: H; clear H).
Ltac move_neq_up H :=
(rewrite ltnNge; apply/negP; intros H)
|| (rewrite leqNgt; apply/negP; intros H).
The following tactic converts inequality t1 ≤ t2 into a constant
k such that t2 = t1 + k and substitutes all the occurrences of
t2.
Ltac interval_to_duration t1 t2 k :=
match goal with
| [ H: (t1 ≤ t2) = true |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto | ];
destruct EX as [k EQ]; subst t2; clear H
)
| [ H: (t1 < t2) = true |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto using ltnW | ];
destruct EX as [k EQ]; subst t2; clear H
)
| [ H: is_true (t1 ≤ t2) |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto | ];
destruct EX as [k EQ]; subst t2; clear H
)
| [ H: is_true (t1 < t2) |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto using ltnW | ];
destruct EX as [k EQ]; subst t2; clear H
)
end.
match goal with
| [ H: (t1 ≤ t2) = true |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto | ];
destruct EX as [k EQ]; subst t2; clear H
)
| [ H: (t1 < t2) = true |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto using ltnW | ];
destruct EX as [k EQ]; subst t2; clear H
)
| [ H: is_true (t1 ≤ t2) |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto | ];
destruct EX as [k EQ]; subst t2; clear H
)
| [ H: is_true (t1 < t2) |- _ ] ⇒
ltac:(
assert (EX : ∃ (k: nat), t2 = t1 + k);
[∃ (t2 - t1); rewrite subnKC; auto using ltnW | ];
destruct EX as [k EQ]; subst t2; clear H
)
end.