Library Vtac
This file collects a number of basic lemmas and tactics for better
proof automation, structuring large proofs, or rewriting. Most of
the rewriting support is ported from ss-reflect.
Symbols starting with vlib__ are internal.
Require Import Bool.
Require Import Arith.
Require Import ZArith.
Require Import String.
Require Import Program.
Set Implicit Arguments.
Hint Unfold not iff.
Notation "p <1= q" :=
(forall a (PR: p a : Prop), q a : Prop)
(at level 100, no associativity).
Notation "p <2= q" :=
(forall a b (PR: p a b : Prop), q a b : Prop)
(at level 100, no associativity).
Notation "p <3= q" :=
(forall a b c (PR: p a b c : Prop), q a b c : Prop)
(at level 100, no associativity).
Notation "p <4= q" :=
(forall a b c d (PR: p a b c d : Prop), q a b c d : Prop)
(at level 100, no associativity).
Notation "p <5= q" :=
(forall a b c d e (PR: p a b c d e : Prop), q a b c d e : Prop)
(at level 100, no associativity).
Notation "p <6= q" :=
(forall a b c d e f (PR: p a b c d e f : Prop), q a b c d e f : Prop)
(at level 100, no associativity).
Notation "p <7= q" :=
(forall a b c d e f g (PR: p a b c d e f g : Prop), q a b c d e f g : Prop)
(at level 100, no associativity).
Notation "p <8= q" :=
(forall a b c d e f g h (PR: p a b c d e f g h : Prop), q a b c d e f g h : Prop)
(at level 100, no associativity).
Notation "p <9= q" :=
(forall a b c d e f g h i (PR: p a b c d e f g h i : Prop), q a b c d e f g h i : Prop)
(at level 100, no associativity).
Notation "p <10= q" :=
(forall a b c d e f g h i j (PR: p a b c d e f g h i j : Prop), q a b c d e f g h i j : Prop)
(at level 100, no associativity).
Notation "p <11= q" :=
(forall a b c d e f g h i j k (PR: p a b c d e f g h i j k : Prop), q a b c d e f g h i j k : Prop)
(at level 100, no associativity).
Notation "p <12= q" :=
(forall a b c d e f g h i j k l (PR: p a b c d e f g h i j k l : Prop), q a b c d e f g h i j k l : Prop)
(at level 100, no associativity).
Coersion of bools into Prop
Hints for auto
Lemma vlib__true_is_true : true.
Proof. reflexivity. Qed.
Lemma vlib__not_false_is_true : ~ false.
Proof. discriminate. Qed.
Lemma vlib__negb_rewrite: forall {b}, negb b -> b = false.
Proof. intros []; (reflexivity || discriminate). Qed.
Lemma vlib__andb_split: forall {b1 b2}, b1 && b2 -> b1 /\ b2.
Proof. intros [] []; try discriminate; auto. Qed.
Hint Resolve vlib__true_is_true vlib__not_false_is_true.
Proof. reflexivity. Qed.
Lemma vlib__not_false_is_true : ~ false.
Proof. discriminate. Qed.
Lemma vlib__negb_rewrite: forall {b}, negb b -> b = false.
Proof. intros []; (reflexivity || discriminate). Qed.
Lemma vlib__andb_split: forall {b1 b2}, b1 && b2 -> b1 /\ b2.
Proof. intros [] []; try discriminate; auto. Qed.
Hint Resolve vlib__true_is_true vlib__not_false_is_true.
Set up for basic simplification
Create HintDb vlib discriminated.
Adaptation of the ss-reflect "done" tactic.
Ltac vlib__basic_done :=
solve [trivial with vlib | apply sym_equal; trivial | discriminate | contradiction].
Ltac done := trivial with vlib; hnf; intros;
solve [try vlib__basic_done; split;
try vlib__basic_done; split;
try vlib__basic_done; split;
try vlib__basic_done; split;
try vlib__basic_done; split; vlib__basic_done
| match goal with H : ~ _ |- _ => solve [case H; trivial] end].
A variant of the ssr "done" tactic that performs "eassumption".
Ltac edone := try eassumption; trivial; hnf; intros;
solve [try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; vlib__basic_done
| match goal with H : ~ _ |- _ => solve [case H; trivial] end].
Tactic Notation "by" tactic(tac) := (tac; done).
Tactic Notation "eby" tactic(tac) := (tac; edone).
Ltac vlib__complaining_inj f H :=
let X := fresh in
(match goal with | [|- ?P ] => set (X := P) end);
injection H;
(lazymatch goal with | [ |- f _ = f _ -> _] => fail | _ => idtac end);
clear H; intros;
subst X;
try subst.
Ltac vlib__clarify1 :=
try subst;
repeat match goal with
| [H: is_true (andb _ _) |- _] => case (vlib__andb_split H); clear H; intros ? H
| [H: is_true (negb ?x) |- _] => rewrite (vlib__negb_rewrite H) in *
| [H: is_true ?x |- _] => rewrite H in *
| [H: ?x = true |- _] => rewrite H in *
| [H: ?x = false |- _] => rewrite H in *
| [H: ?f _ = ?f _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ = ?f _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ = ?f _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ = ?f _ _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ _ _ _ = ?f _ _ _ _ _ _ _ |- _] => vlib__complaining_inj f H
end; try done.
Perform injections & discriminations on all hypotheses
Ltac clarify :=
vlib__clarify1;
repeat match goal with
| H1: ?x = Some _, H2: ?x = None |- _ => rewrite H2 in H1; vlib__clarify1
| H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; vlib__clarify1
end.
Kill simple goals that require up to two econstructor calls.
Ltac vauto :=
(clarify; try edone;
try (econstructor (solve [edone | econstructor (edone) ]))).
Check that the hypothesis id is defined. This is useful to make sure that
an assert has been completely finished.
Ltac end_assert id :=
let m := fresh in
pose (m := refl_equal id); clear m.
Ltac inv x := inversion x; clarify.
Ltac simpls := simpl in *; try done.
Ltac ins := simpl in *; try done; intros.
Tactic Notation "case_eq" constr(x) := case_eq (x).
Tactic Notation "case_eq" constr(x) "as" simple_intropattern(H) :=
destruct x as [] _eqn: H; try done.
Ltac vlib__clarsimp1 :=
clarify; (autorewrite with vlib in * ); try done;
match goal with
| [H: is_true ?x |- _] => rewrite H in *; vlib__clarsimp1
| [H: ?x = true |- _] => rewrite H in *; vlib__clarsimp1
| [H: ?x = false |- _] => rewrite H in *; vlib__clarsimp1
| _ => clarify; auto 1 with vlib
end.
Ltac clarsimp := intros; simpl in *; vlib__clarsimp1.
Ltac autos := clarsimp; auto with vlib.
Named case tactics (taken from Libtactics)
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move x at top
| assert_eq x name
| fail 1 "because we are working on a different case." ].
Ltac Case name := Case_aux case name.
Ltac SCase name := Case_aux subcase name.
Ltac SSCase name := Case_aux subsubcase name.
Ltac SSSCase name := Case_aux subsubsubcase name.
Ltac SSSSCase name := Case_aux subsubsubsubcase name.
Lightweight case tactics (without names)
Tactic Notation "-" tactic(c) :=
first [
assert (WithinCaseM := True); move WithinCaseM at top
| fail 1 "because we are working on a different case." ]; c.
Tactic Notation "+" tactic(c) :=
first [
assert (WithinCaseP := True); move WithinCaseP at top
| fail 1 "because we are working on a different case." ]; c.
Tactic Notation "*" tactic(c) :=
first [
assert (WithinCaseS := True); move WithinCaseS at top
| fail 1 "because we are working on a different case." ]; c.
Tactic Notation ":" tactic(c) :=
first [
assert (WithinCaseC := True); move WithinCaseC at top
| fail 1 "because we are working on a different case." ]; c.
Exploit an assumption (adapted from CompCert).
Ltac exploit x :=
refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _) _)
|| refine ((fun x y => y x) (x _ _) _)
|| refine ((fun x y => y x) (x _) _).
Lemma mp: forall P Q: Type, P -> (P -> Q) -> Q.
Proof. intuition. Defined.
Ltac hexploit x := eapply mp; [eapply x|].
Ltac set_prop N T A :=
let b := fresh in let ty := type of T in
match ty with (forall (_:?P), _) => assert (A: P); [|set (N := T A)] end.
Tactic Notation "induction" "[" ident_list(y) "]" ident(x) :=
first [ try (intros until x); revert y; induction x
| red; try (intros until x); revert y; induction x ].
Tactic Notation "induction" "[" ident_list(y) "]" ident(x) "[" ident(z) "]" :=
first [ try (intros until x); revert y; induction x; destruct z
| red; try (intros until x); revert y; induction x; destruct z ].
Tactic Notation "edestructs" ident(a) :=
(edestruct a).
Tactic Notation "edestructs" ident(a) ident(b) :=
(edestruct a; edestruct b).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) :=
(edestruct a; edestruct b; edestruct c).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) :=
(edestruct a; edestruct b; edestruct c; edestruct d).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(edestruct a; edestruct b; edestruct c; edestruct d; edestruct e).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) :=
(edestruct a; edestruct b; edestruct c; edestruct d; edestruct e; edestruct f).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) :=
(edestruct a; edestruct b; edestruct c; edestruct d; edestruct e; edestruct f; edestruct g).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) :=
(edestruct a; edestruct b; edestruct c; edestruct d; edestruct e; edestruct f; edestruct g; edestruct h).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) :=
(edestruct a; edestruct b; edestruct c; edestruct d; edestruct e; edestruct f; edestruct g; edestruct h; edestruct i).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) ident(j) :=
(edestruct a; edestruct b; edestruct c; edestruct d; edestruct e; edestruct f; edestruct g; edestruct h; edestruct i; edestruct j).
Tactic Notation "destructs" ident(a) :=
(destruct a).
Tactic Notation "destructs" ident(a) ident(b) :=
(destruct a; destruct b).
Tactic Notation "destructs" ident(a) ident(b) ident(c) :=
(destruct a; destruct b; destruct c).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) :=
(destruct a; destruct b; destruct c; destruct d).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(destruct a; destruct b; destruct c; destruct d; destruct e).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) :=
(destruct a; destruct b; destruct c; destruct d; destruct e; destruct f).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) :=
(destruct a; destruct b; destruct c; destruct d; destruct e; destruct f; destruct g).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) :=
(destruct a; destruct b; destruct c; destruct d; destruct e; destruct f; destruct g; destruct h).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) :=
(destruct a; destruct b; destruct c; destruct d; destruct e; destruct f; destruct g; destruct h; destruct i).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) ident(j) :=
(destruct a; destruct b; destruct c; destruct d; destruct e; destruct f; destruct g; destruct h; destruct i; destruct j).
Tactic Notation "depdes" ident(a) :=
(dependent destruction a).
Tactic Notation "depdes" ident(a) ident(b) :=
(dependent destruction a; dependent destruction b).
Tactic Notation "depdes" ident(a) ident(b) ident(c) :=
(dependent destruction a; dependent destruction b; dependent destruction c).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) :=
(dependent destruction a; dependent destruction b; dependent destruction c; dependent destruction d).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(dependent destruction a; dependent destruction b; dependent destruction c; dependent destruction d; dependent destruction e).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) :=
(dependent destruction a; dependent destruction b; dependent destruction c; dependent destruction d; dependent destruction e; dependent destruction f).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) :=
(dependent destruction a; dependent destruction b; dependent destruction c; dependent destruction d; dependent destruction e; dependent destruction f; dependent destruction g).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) :=
(dependent destruction a; dependent destruction b; dependent destruction c; dependent destruction d; dependent destruction e; dependent destruction f; dependent destruction g; dependent destruction h).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) :=
(dependent destruction a; dependent destruction b; dependent destruction c; dependent destruction d; dependent destruction e; dependent destruction f; dependent destruction g; dependent destruction h; dependent destruction i).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) ident(j) :=
(dependent destruction a; dependent destruction b; dependent destruction c; dependent destruction d; dependent destruction e; dependent destruction f; dependent destruction g; dependent destruction h; dependent destruction i; dependent destruction j).
Ltac esplits :=
repeat match goal with
| [ |- @ex _ _ ] => eexists
| [ |- _ /\ _ ] => split
end.
Tactic Notation "replace_all" constr(e) :=
let X := fresh in assert (X: e) by (clarify; eauto; done);
first [rewrite !X | setoid_rewrite X]; clear X.
Destruct but give useful names
Definition NW A (P: unit -> A) : A := P tt.
Notation "<< x : t >>" := (NW (fun x => t)) (at level 80, x ident, no associativity).
Notation "<< t >>" := (NW (fun _ => t)) (at level 79, no associativity).
Ltac unnw := unfold NW in *.
Ltac rednw := red; unnw.
Hint Unfold NW.
Destruct, but no case split
Ltac desc :=
repeat match goal with
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
end.
Ltac des :=
repeat match goal with
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
| H : ?p <-> ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => unfold NW at 1 in x'; red in y' | _ => idtac end;
match q with | NW _ => unfold NW at 1 in y'; red in x' | _ => idtac end
| H : ?p \/ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => H end in
destruct H as [x' | y'];
[ match p with | NW _ => red in x' | _ => idtac end
| match q with | NW _ => red in y' | _ => idtac end]
end.
Ltac des_if :=
clarify;
repeat
match goal with
| |- context[match ?x with _ => _ end] =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
| H: context[ match ?x with _ => _ end ] |- _ =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
end.
Ltac des_eqrefl :=
match goal with
| H: context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] |- _ =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'; intros H
| |- context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'
end.
Ltac desf := clarify; des; des_if.
repeat match goal with
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
end.
Ltac des :=
repeat match goal with
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
| H : ?p <-> ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => unfold NW at 1 in x'; red in y' | _ => idtac end;
match q with | NW _ => unfold NW at 1 in y'; red in x' | _ => idtac end
| H : ?p \/ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => H end in
destruct H as [x' | y'];
[ match p with | NW _ => red in x' | _ => idtac end
| match q with | NW _ => red in y' | _ => idtac end]
end.
Ltac des_if :=
clarify;
repeat
match goal with
| |- context[match ?x with _ => _ end] =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
| H: context[ match ?x with _ => _ end ] |- _ =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
end.
Ltac des_eqrefl :=
match goal with
| H: context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] |- _ =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'; intros H
| |- context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'
end.
Ltac desf := clarify; des; des_if.