Library CompOptCert.sflib
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 ssreflect.
Symbols starting with sflib__ are internal.
Require Import Bool List Arith ZArith String Program.
Set Implicit Arguments.
#[export] Hint Unfold not iff id: core.
Export ListNotations.
Notation "f <*> g" := (compose f g) (at level 49, left associativity).
Coersion of bool into Prop
Coersion of bools into Prop
Hints for auto
Lemma sflib__true_is_true : true.
Proof. reflexivity. Qed.
Lemma sflib__not_false_is_true : ¬ false.
Proof. discriminate. Qed.
Lemma sflib__negb_rewrite: ∀ {b}, negb b → b = false.
Proof. intros []; (reflexivity || discriminate). Qed.
Lemma sflib__andb_split: ∀ {b1 b2}, b1 && b2 → b1 ∧ b2.
Proof. intros [] []; try discriminate; auto. Qed.
#[export] Hint Resolve sflib__true_is_true sflib__not_false_is_true: core.
Proof. reflexivity. Qed.
Lemma sflib__not_false_is_true : ¬ false.
Proof. discriminate. Qed.
Lemma sflib__negb_rewrite: ∀ {b}, negb b → b = false.
Proof. intros []; (reflexivity || discriminate). Qed.
Lemma sflib__andb_split: ∀ {b1 b2}, b1 && b2 → b1 ∧ b2.
Proof. intros [] []; try discriminate; auto. Qed.
#[export] Hint Resolve sflib__true_is_true sflib__not_false_is_true: core.
Set up for basic simplification
Create HintDb sflib discriminated.
Adaptation of the ss-reflect "done" tactic.
Ltac sflib__basic_done :=
solve [trivial with sflib | apply sym_equal; trivial | discriminate | contradiction].
Ltac done := unfold not in *; trivial with sflib; hnf; intros;
solve [try sflib__basic_done; split;
try sflib__basic_done; split;
try sflib__basic_done; split;
try sflib__basic_done; split;
try sflib__basic_done; split; sflib__basic_done
| match goal with H : _ → False |- _ ⇒ 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 sflib__basic_done; split;
try eassumption; try sflib__basic_done; split;
try eassumption; try sflib__basic_done; split;
try eassumption; try sflib__basic_done; split;
try eassumption; try sflib__basic_done; split;
try eassumption; sflib__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 sflib__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 sflib__clarify1 :=
try subst;
repeat match goal with
| [H: is_true (andb _ _) |- _] ⇒ case (sflib__andb_split H); clear H; intros ? H
| [H: is_true (negb ?x) |- _] ⇒ rewrite (sflib__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 _ |- _] ⇒ sflib__complaining_inj f H
| [H: ?f _ _ = ?f _ _ |- _] ⇒ sflib__complaining_inj f H
| [H: ?f _ _ _ = ?f _ _ _ |- _] ⇒ sflib__complaining_inj f H
| [H: ?f _ _ _ _ = ?f _ _ _ _ |- _] ⇒ sflib__complaining_inj f H
| [H: ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _] ⇒ sflib__complaining_inj f H
| [H: ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _] ⇒ sflib__complaining_inj f H
| [H: ?f _ _ _ _ _ _ _ = ?f _ _ _ _ _ _ _ |- _] ⇒ sflib__complaining_inj f H
end; try done.
Perform injections & discriminations on all hypotheses
Ltac clarify :=
sflib__clarify1;
repeat match goal with
| H1: ?x = Some _, H2: ?x = None |- _ ⇒ rewrite H2 in H1; sflib__clarify1
| H1: ?x = Some _, H2: ?x = Some _ |- _ ⇒ rewrite H2 in H1; sflib__clarify1
end.
Kill simple goals that require up to two econstructor calls.
Ltac inv H := inversion H; clear H; subst.
Ltac hinv x := move x at bottom; inversion x; clarify.
Tactic Notation "hinv" ident(a) :=
(hinv a).
Tactic Notation "hinv" ident(a) ident(b) :=
(hinv a; hinv b).
Tactic Notation "hinv" ident(a) ident(b) ident(c) :=
(hinv a; hinv b c).
Tactic Notation "hinv" ident(a) ident(b) ident(c) ident(d) :=
(hinv a b; hinv c d).
Ltac hinvc x := hinv x; clear x.
Tactic Notation "hinvc" ident(a) :=
(hinvc a).
Tactic Notation "hinvc" ident(a) ident(b) :=
(hinvc a; hinvc b).
Tactic Notation "hinvc" ident(a) ident(b) ident(c) :=
(hinvc a; hinvc b c).
Tactic Notation "hinvc" ident(a) ident(b) ident(c) ident(d) :=
(hinvc a b; hinvc c d).
Tactic Notation "hinvc" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(hinvc a b c; hinvc d e).
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 sflib__clarsimp1 :=
clarify; (autorewrite with sflib in × ); try done;
match goal with
| [H: is_true ?x |- _] ⇒ rewrite H in *; sflib__clarsimp1
| [H: ?x = true |- _] ⇒ rewrite H in *; sflib__clarsimp1
| [H: ?x = false |- _] ⇒ rewrite H in *; sflib__clarsimp1
| _ ⇒ clarify; auto 1 with sflib
end.
Ltac clarsimp := intros; simpl in *; sflib__clarsimp1.
Ltac autos := clarsimp; auto with sflib.
Definition NW A (P: () → A) : A := P ().
Notation "<< x : t >>" := (NW (fun x ⇒ (t):Prop)) (at level 80, x name, no associativity).
Notation "<< t >>" := (NW (fun _ ⇒ t)) (at level 79, no associativity, only printing).
Notation "<< t >>" := (NW (fun _ ⇒ (t):Prop)) (at level 79, no associativity, only printing).
Ltac unnw := unfold NW in ×.
Ltac rednw := red; unnw.
#[export] Hint Unfold NW: core.
Ltac get_concl := lazymatch goal with [ |- ?G ] ⇒ G end.
Ltac des1 :=
match goal with
| H : NW _ |- _ ⇒ red in H
| H : ∃ x, NW (fun y ⇒ _) |- _ ⇒
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : ∃ 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 : ?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 := repeat des1.
Ltac desc :=
repeat match goal with
| H : ∃ x, NW (fun y ⇒ _) |- _ ⇒
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : ∃ 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 (sflib__andb_split H); clear H; intros H H'
| H : ?x = ?x |- _ ⇒ clear H
end.
Ltac nbdes1 :=
match goal with
| H : NW _ |- _ ⇒ red in H
| H : ∃ x, NW (fun y ⇒ _) |- _ ⇒
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : ∃ 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 : ?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
end.
Ltac nbdes := repeat nbdes1.
Ltac rrnbdes H := move H at bottom; repeat red in H; nbdes.
Ltac forall_split :=
let H := fresh "__forall_split__" in first [intro; forall_split; match goal with [H:_|-_] ⇒ revert H end | split].
Definition _HID_ (A : Type) (a : A) := a.
Ltac hdesHi H P x y :=
let FF := fresh "__hdesfalse__" in
let TMP := fresh "__hdesHi__" in
let P1 := fresh "__hdesHi__" in
let P2 := fresh "__hdesHi__" in
evar (P1 : Prop); evar (P2 : Prop);
assert (TMP: False → P) by
(intro FF; forall_split;
[ let G := get_concl in set (TMP := G); revert P1; instantiate (1:=G)
| let G := get_concl in set (TMP := G); revert P2; instantiate (1:=G) ];
destruct FF);
try clear TMP;
try (try (match goal with [Def := ?G : _ |- _] ⇒
match Def with P1 ⇒
match goal with [_ : G |- _] ⇒ fail 4 end end end);
assert (x: P1) by (unfold P1; repeat (let x := fresh "__xhj__" in intro x; specialize (H x)); apply H));
try unfold P1 in x; try clear P1;
try (try (match goal with [Def := ?G : _ |- _] ⇒
match Def with P2 ⇒
match goal with [_ : G |- _] ⇒ fail 4 end end end);
assert (y: P2) by (unfold P2; repeat (let x := fresh "__xhj__" in intro x; specialize (H x)); apply H));
try unfold P2 in y; try clear P2;
fold (_HID_ P) in H;
try clear H.
Ltac hdesHP H P :=
let H' := fresh H in let H'' := fresh H in
match P with
| context[ NW (fun x ⇒ _) ∧ NW (fun y ⇒ _) ] ⇒
let x' := fresh x in let y' := fresh y in
hdesHi H P x' y'; red in x'; red in y'
| context[ NW (fun x ⇒ _) ∧ _ ] ⇒
let x' := fresh x in
hdesHi H P x' H'; red in x'
| context[ _ ∧ NW (fun y ⇒ _) ] ⇒
let y' := fresh y in
hdesHi H P H' y'; red in y'
| context[ _ ∧ _ ] ⇒
hdesHi H P H' H''
| context[ NW (fun x ⇒ _) ↔ NW (fun y ⇒ _) ] ⇒
let x' := fresh x in let y' := fresh y in
hdesHi H P x' y'; red in x'; red in y'
| context[ NW (fun x ⇒ _) ↔ _ ] ⇒
let x' := fresh x in
hdesHi H P x' H'; red in x'
| context[ _ ↔ NW (fun y ⇒ _) ] ⇒
let y' := fresh y in
hdesHi H P H' y'; red in y'
| context[ _ ↔ _ ] ⇒
hdesHi H P H' H''
end.
Ltac hdesH H := let P := type of H in hdesHP H P; unfold _HID_ in ×.
Ltac hdesF P :=
match P with | _ ∧ _ ⇒ idtac | _ ↔ _ ⇒ idtac | ∀ _, _ ⇒
match P with | ∀ _, _ ∧ _ ⇒ idtac | ∀ _, _ ↔ _ ⇒ idtac | ∀ _ _, _ ⇒
match P with | ∀ _ _, _ ∧ _ ⇒ idtac | ∀ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _, _ ⇒
match P with | ∀ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ⇒
match P with | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ∧ _ ⇒ idtac | ∀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, _ ↔ _ ⇒ idtac
end end end end end end end end end end end end end end end end end end end end end.
Fail if hypothesis H doesn't exist.
Ltac check_hyp H := match H with _ ⇒ idtac end.
Fail if hypothesis H1 is not H2.
Ltac check_equal H1 H2 := match H1 with H2 ⇒ idtac end.
Ltac hdes :=
repeat match goal with | H : ?P |- _ ⇒ hdesF P; hdesHP H P end;
unfold _HID_ in ×.
Ltac rdes H := red in H; des.
Ltac rrdes H := move H at bottom; repeat red in H; des.
Ltac rhdes H := red in H; hdes.
Ltac rrhdes H := check_hyp H; repeat red in H; hdes.
Tactic Notation "rrdes" ident(a) :=
(rrdes a).
Tactic Notation "rrdes" ident(a) ident(b) :=
(rrdes a; rrdes b).
Tactic Notation "rrdes" ident(a) ident(b) ident(c) :=
(rrdes a; rrdes b c).
Tactic Notation "rrdes" ident(a) ident(b) ident(c) ident(d) :=
(rrdes a b; rrdes c d).
Ltac hdes :=
repeat match goal with | H : ?P |- _ ⇒ hdesF P; hdesHP H P end;
unfold _HID_ in ×.
Ltac rdes H := red in H; des.
Ltac rrdes H := move H at bottom; repeat red in H; des.
Ltac rhdes H := red in H; hdes.
Ltac rrhdes H := check_hyp H; repeat red in H; hdes.
Tactic Notation "rrdes" ident(a) :=
(rrdes a).
Tactic Notation "rrdes" ident(a) ident(b) :=
(rrdes a; rrdes b).
Tactic Notation "rrdes" ident(a) ident(b) ident(c) :=
(rrdes a; rrdes b c).
Tactic Notation "rrdes" ident(a) ident(b) ident(c) ident(d) :=
(rrdes a b; rrdes c d).
Destruct the condition of an if expression occuring in the goal.
Ltac des_if :=
match goal with
| [ |- context[if ?X then _ else _] ] ⇒ destruct X
end.
match goal with
| [ |- context[if ?X then _ else _] ] ⇒ destruct X
end.
Destruct the condition of an if expression occuring in the given hypothesis.
Ltac des_ifH H :=
match goal with
| [ H' : context[if ?X then _ else _] |- _ ] ⇒ check_equal H' H; destruct X
end.
Ltac des_ifs :=
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 desf := clarify; des; des_ifs.
Ltac isd := ins; desf.
match goal with
| [ H' : context[if ?X then _ else _] |- _ ] ⇒ check_equal H' H; destruct X
end.
Ltac des_ifs :=
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 desf := clarify; des; des_ifs.
Ltac isd := ins; desf.
Create a copy of hypothesis H.
Tactic Notation "dup" hyp(H) :=
let H' := fresh H in assert (H' := H).
Ltac clarassoc := clarsimp; autorewrite with sflib sflibA in *; try done.
Ltac sflib__hacksimp1 :=
clarsimp;
match goal with
| H: _ |- _ ⇒ solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| _ ⇒ solve [f_equal; clarsimp]
end.
Ltac hacksimp :=
clarsimp;
try match goal with
| H: _ |- _ ⇒ solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| |- context[if ?p then _ else _] ⇒ solve [destruct p; sflib__hacksimp1]
| _ ⇒ solve [f_equal; clarsimp]
end.
let H' := fresh H in assert (H' := H).
Ltac clarassoc := clarsimp; autorewrite with sflib sflibA in *; try done.
Ltac sflib__hacksimp1 :=
clarsimp;
match goal with
| H: _ |- _ ⇒ solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| _ ⇒ solve [f_equal; clarsimp]
end.
Ltac hacksimp :=
clarsimp;
try match goal with
| H: _ |- _ ⇒ solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| |- context[if ?p then _ else _] ⇒ solve [destruct p; sflib__hacksimp1]
| _ ⇒ solve [f_equal; clarsimp]
end.
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: ∀ P Q: Type, P → (P → Q) → Q.
Proof. intuition. Defined.
Lemma mp': ∀ P Q : Type, (P → Q) → P → Q.
Proof. intuition. Qed.
Ltac hexploit x := eapply mp; [eapply x|].
Ltac hexploit' x := let H := fresh in set (H := x); clear H; eapply mp; [eapply x|].
Ltac set_prop N T A :=
let b := fresh in let ty := type of T in
match ty with (∀ (_:?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 ].
Versions with hacksimp
Tactic Notation "induct" ident(x) := induction x; hacksimp.
Tactic Notation "induct" ident(x) "[" ident(z) "]" :=
induction x; destruct z; hacksimp.
Tactic Notation "induct" "[" ident_list(y) "]" ident(x) :=
first [ try (intros until x); revert y; induction x; hacksimp
| red; try (intros until x); revert y; induction x; hacksimp ].
Tactic Notation "induct" "[" ident_list(y) "]" ident(x) "[" ident(z) "]" :=
first [ try (intros until x); revert y; induction x; destruct z; hacksimp
| red; try (intros until x); revert y; induction x; destruct z; hacksimp ].
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; edestructs b c).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) :=
(edestruct a; edestructs b c d).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(edestruct a; edestructs b c d e).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) :=
(edestruct a; edestructs b c d e f).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) :=
(edestruct a; edestructs b c d e f g).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) :=
(edestruct a; edestructs b c d e f g h).
Tactic Notation "edestructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) :=
(edestruct a; edestructs b c d e f g h 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; edestructs b c d e f g h i 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; destructs b c).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) :=
(destruct a; destructs b c d).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(destruct a; destructs b c d e).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) :=
(destruct a; destructs b c d e f).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) :=
(destruct a; destructs b c d e f g).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) :=
(destruct a; destructs b c d e f g h).
Tactic Notation "destructs" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) :=
(destruct a; destructs b c d e f g h 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; destructs b c d e f g h i j).
Tactic Notation "depdes" ident(_something_which_shold_not_occur_in_the_goal_) :=
(let _x_ := type of _something_which_shold_not_occur_in_the_goal_
in dependent destruction _something_which_shold_not_occur_in_the_goal_).
Tactic Notation "depdes" ident(a) ident(b) :=
(depdes a; depdes b).
Tactic Notation "depdes" ident(a) ident(b) ident(c) :=
(depdes a; depdes b c).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) :=
(depdes a; depdes b c d).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(depdes a; depdes b c d e).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) :=
(depdes a; depdes b c d e f).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) :=
(depdes a; depdes b c d e f g).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) :=
(depdes a; depdes b c d e f g h).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) :=
(depdes a; depdes b c d e f g h i).
Tactic Notation "depdes" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) ident(g) ident(h) ident(i) ident(j) :=
(depdes a; depdes b c d e f g h i j).
Tactic Notation "depgen" ident(x) := generalize dependent x.
Ltac eappleft H :=
let X := fresh "__lem__" in let X1 := fresh "__lem__" in let X2 := fresh "__lem__" in
assert (X:= H); let P := type of X in hdesHi X P X1 X2;
eapply X1; clear X1 X2.
Ltac eappright H :=
let X := fresh "__lem__" in let X1 := fresh "__lem__" in let X2 := fresh "__lem__" in
assert (X:= H); let P := type of X in hdesHi X P X1 X2;
eapply X2; clear X1 X2.
Definition __guard__ A (a : A) : A := a.
Definition __GUARD__ A (a : A) : A := a.
Arguments __guard__ A a : simpl never.
Arguments __GUARD__ A a : simpl never.
Tactic Notation "guard" constr(t) "in" hyp(H) := fold (__guard__ t) in H.
Tactic Notation "guardH" hyp(H) := let t := type of H in guard t in H.
Tactic Notation "guard" :=
repeat match goal with [H: ?P |- _] ⇒
try (match P with __guard__ _ ⇒ fail 2 end); guardH H
end.
Tactic Notation "sguard" constr(t) "in" hyp(H) := fold (__GUARD__ t) in H.
Tactic Notation "sguard" "in" hyp(H) := let t := type of H in sguard t in H.
Ltac unguard := unfold __guard__ in ×.
Ltac unguardH H := unfold __guard__ in H.
Ltac unsguard H := unfold __GUARD__ in H.
Ltac desH H := guard; unguardH H; des; unguard.
Ltac splits :=
intros; unfold NW;
repeat match goal with
| [ |- _ ∧ _ ] ⇒ split
end.
Ltac esplits :=
intros; unfold NW;
repeat match goal with
| [ |- @ex _ _ ] ⇒ eexists
| [ |- _ ∧ _ ] ⇒ split
| [ |- @sig _ _ ] ⇒ eexists
| [ |- @sigT _ _ ] ⇒ eexists
| [ |- @prod _ _ ] ⇒ split
end.
Tactic Notation "replace_all" constr(e) := repeat (
let X := fresh in assert (X: e) by (clarify; eauto; done);
first [rewrite !X | setoid_rewrite X]; clear X).
Lemma all_conj_dist: ∀ A (P Q: A → Prop),
(∀ a, P a ∧ Q a) → (∀ a, P a) ∧ (∀ a, Q a).
Proof. intros; hdes; eauto. Qed.
Tactic Notation "extensionalities" :=
repeat let x := fresh in extensionality x.
Tactic Notation "extensionalities" ident(a) :=
(extensionality a).
Tactic Notation "extensionalities" ident(a) ident(b) :=
(extensionality a; extensionality b).
Tactic Notation "extensionalities" ident(a) ident(b) ident(c) :=
(extensionality a; extensionalities b c).
Tactic Notation "extensionalities" ident(a) ident(b) ident(c) ident(d) :=
(extensionality a; extensionalities b c d).
Tactic Notation "extensionalities" ident(a) ident(b) ident(c) ident(d) ident(e) :=
(extensionality a; extensionalities b c d e).
Tactic Notation "extensionalities" ident(a) ident(b) ident(c) ident(d) ident(e) ident(f) :=
(extensionality a; extensionalities b c d e f).
Tactic Notation "inst" := instantiate.
Tactic Notation "econs" := econstructor.
Tactic Notation "econs" int_or_var(x) := econstructor x.
Tactic Notation "i" := intros.
Tactic Notation "ii" := repeat intro.
Tactic Notation "s" := simpl.
Tactic Notation "s" ident(a) := simpl a.
Tactic Notation "s" constr(t) := simpl t.
Tactic Notation "s" "in" hyp(H) := simpl in H.
Tactic Notation "ss" := simpls.
Tactic Notation "r" := red.
Tactic Notation "r" "in" hyp(H) := red in H.
Tactic Notation "rr" := repeat red.
Tactic Notation "rr" "in" hyp(H) := repeat red in H.
Definition __mark__ A (a : A) : A := a.
Tactic Notation "M" :=
match goal with [|-?G] ⇒ fold (__mark__ G) end.
Tactic Notation "Mdo" tactic(tac) :=
first [ try match goal with [|- __mark__ _ ] ⇒ fail 2 end | unfold __mark__; tac ].
Tactic Notation "Mskip" tactic(tac) :=
first [ match goal with [|- __mark__ _ ] ⇒ unfold __mark__ end | tac ].
Tactic Notation "Mfirst" tactic(main) ";;" tactic(post) :=
main; (Mdo (post; M)); (Mskip post).
Ltac on_last_hyp tac :=
match goal with [ H : _ |- _ ] ⇒ first [ tac H | fail 1 ] end.
Ltac revert_until id :=
on_last_hyp ltac:(fun id' ⇒
match id' with
| id ⇒ idtac
| _ ⇒ revert id' ; revert_until id
end).
Open Scope string_scope.
Open Scope list_scope.
Fixpoint beq_str (s1 s2: string) : bool :=
match s1, s2 with
| "", "" ⇒ true
| String a s1', String b s2' ⇒ if Ascii.ascii_dec a b then beq_str s1' s2' else false
| _, _ ⇒ false
end.
Ltac uf := (autounfold with × in *).
Tactic Notation "patout" constr(z) "in" hyp(a) :=
pattern z in a; match goal with [a:=?f z|-_] ⇒ unfold a; clear a; set (a:=f) end.
Ltac clear_upto H :=
repeat (match goal with [Hcrr : _ |- _ ] ⇒ first [ check_equal Hcrr H; fail 2
| clear Hcrr ] end).
Definition _Evar_sflib_ (A:Type) (x:A) := x.
Tactic Notation "hide_evar" int_or_var(n) := let QQ := fresh "QQ" in
hget_evar n; intro;
lazymatch goal with [ H := ?X |- _] ⇒
set (QQ := X) in *; fold (_Evar_sflib_ X) in QQ; clear H
end.
Ltac hide_evars := repeat (hide_evar 1).
Ltac show_evars := repeat (match goal with [ H := @_Evar_sflib_ _ _ |- _ ] ⇒ unfold
_Evar_sflib_ in H; unfold H in *; clear H end).
Ltac revert1 := match goal with [H: _|-_] ⇒ revert H end.
Lemma eqimpl: ∀ P Q : Prop, P = Q → P → Q.
Proof. by i; subst; auto. Qed.
Ltac ginduction H :=
move H at top; revert_until H; induction H.
Tactic Notation "greflgen" constr(t) "as" ident(g) :=
let EQ := fresh "XEQ" in
generalize (eq_refl t); generalize t at -2 as g
; intros ? EQ ?; revert EQ.
Ltac eadmit :=
exfalso; clear; admit.
Ltac special H :=
match type of H with
| ?A → ?B ⇒
let a := fresh in assert (a: A); [|specialize (H a)]
end.
Ltac ex x := eapply (ex_intro _ (x _)).
Ltac inst_pairs :=
repeat first
[instantiate (9 := (_, _))
|instantiate (8 := (_, _))
|instantiate (7 := (_, _))
|instantiate (6 := (_, _))
|instantiate (5 := (_, _))
|instantiate (4 := (_, _))
|instantiate (3 := (_, _))
|instantiate (2 := (_, _))
|instantiate (1 := (_, _))].
Ltac simpl_proj :=
do 5 (simpl (fst (_, _)) in *; simpl (snd (_, _)) in *).
Ltac clean :=
repeat match goal with
| H: True |- _
⇒ clear H
| H: ?x = ?y |- _
⇒ try (has_evar x; fail 2); try (has_evar y; fail 2);
change x with y in H; clear H
end
; simpl_proj.
Tactic Notation "lhs" tactic(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := rhs); tac; unfold tmp; clear tmp
end.
Tactic Notation "lhs3" tactic3(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := rhs); tac; unfold tmp; clear tmp
end.
Tactic Notation "rhs" tactic(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := lhs); tac; unfold tmp; clear tmp
end.
Tactic Notation "rhs3" tactic3(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := lhs); tac; unfold tmp; clear tmp
end.
Ltac inst_pairs :=
repeat first
[instantiate (9 := (_, _))
|instantiate (8 := (_, _))
|instantiate (7 := (_, _))
|instantiate (6 := (_, _))
|instantiate (5 := (_, _))
|instantiate (4 := (_, _))
|instantiate (3 := (_, _))
|instantiate (2 := (_, _))
|instantiate (1 := (_, _))].
Ltac simpl_proj :=
do 5 (simpl (fst (_, _)) in *; simpl (snd (_, _)) in *).
Ltac clean :=
repeat match goal with
| H: True |- _
⇒ clear H
| H: ?x = ?y |- _
⇒ try (has_evar x; fail 2); try (has_evar y; fail 2);
change x with y in H; clear H
end
; simpl_proj.
Tactic Notation "lhs" tactic(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := rhs); tac; unfold tmp; clear tmp
end.
Tactic Notation "lhs3" tactic3(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := rhs); tac; unfold tmp; clear tmp
end.
Tactic Notation "rhs" tactic(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := lhs); tac; unfold tmp; clear tmp
end.
Tactic Notation "rhs3" tactic3(tac) :=
match goal with |- ?op ?lhs ?rhs ⇒
let tmp := fresh in set (tmp := lhs); tac; unfold tmp; clear tmp
end.
Execute a tactic only if the goal contains no evars.
Tactic Notation "safe" tactic(tac) :=
try match goal with |- ?G ⇒ try (has_evar G; fail 2); tac end.
try match goal with |- ?G ⇒ try (has_evar G; fail 2); tac end.
Rename a hypothesis to a fresh name.
Ltac ren H :=
let X := fresh H in rename H into X.
let X := fresh H in rename H into X.
Automation using econstructor.
What it does is clear from the definition below.
Tactic Notation "econsby" tactic(tac) :=
first [econstructor 1; (by tac)
|econstructor 2; (by tac)
|econstructor 3; (by tac)
|econstructor 4; (by tac)
|econstructor 5; (by tac)
|econstructor 6; (by tac)
|econstructor 7; (by tac)
|econstructor 8; (by tac)
|econstructor 9; (by tac)
|econstructor 10; (by tac)
|econstructor 11; (by tac)
|econstructor 12; (by tac)
|econstructor 13; (by tac)
|econstructor 14; (by tac)
|econstructor 15; (by tac)
|econstructor 16; (by tac)
|econstructor 17; (by tac)
|econstructor 18; (by tac)
|econstructor 19; (by tac)
|econstructor 20; (by tac)
].
first [econstructor 1; (by tac)
|econstructor 2; (by tac)
|econstructor 3; (by tac)
|econstructor 4; (by tac)
|econstructor 5; (by tac)
|econstructor 6; (by tac)
|econstructor 7; (by tac)
|econstructor 8; (by tac)
|econstructor 9; (by tac)
|econstructor 10; (by tac)
|econstructor 11; (by tac)
|econstructor 12; (by tac)
|econstructor 13; (by tac)
|econstructor 14; (by tac)
|econstructor 15; (by tac)
|econstructor 16; (by tac)
|econstructor 17; (by tac)
|econstructor 18; (by tac)
|econstructor 19; (by tac)
|econstructor 20; (by tac)
].