Library prosa.classic.util.tactics
Require Export prosa.util.tactics.
(* *********************************************************************)
(* *)
(* Basic lemmas & tactics (based on Viktor Vafeiadis' Vbase.v) *)
(* *)
(* *********************************************************************)
(* *********************************************************************)
(* *)
(* Basic lemmas & tactics (based on Viktor Vafeiadis' Vbase.v) *)
(* *)
(* *********************************************************************)
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 vlib__ are internal.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype bigop.
Open Scope bool_scope.
Open Scope list_scope.
Set Implicit Arguments.
Unset Strict Implicit.
(* ************************************************************************** *)
(* ************************************************************************** *)
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).
(* ************************************************************************** *)
(* ************************************************************************** *)
Lemma vlib__internal_eqP :
∀ (T: eqType) (x y : T), reflect (x = y) (x == y).
Proof. by intros; apply/eqP. Qed.
Lemma beq_refl : ∀ (T : eqType) (x : T), x == x.
Proof. by intros; case eqP. Qed.
Lemma beq_sym : ∀ (T : eqType) (x y : T), (x == y) = (y == x).
Proof. intros; do 2 case eqP; congruence. Qed.
#[global] Hint Resolve beq_refl : vlib.
#[global] Hint Rewrite beq_refl : vlib_trivial.
Notation eqxx := beq_refl.
(* ************************************************************************** *)
Lemma vlib__internal_eqP :
∀ (T: eqType) (x y : T), reflect (x = y) (x == y).
Proof. by intros; apply/eqP. Qed.
Lemma beq_refl : ∀ (T : eqType) (x : T), x == x.
Proof. by intros; case eqP. Qed.
Lemma beq_sym : ∀ (T : eqType) (x y : T), (x == y) = (y == x).
Proof. intros; do 2 case eqP; congruence. Qed.
#[global] Hint Resolve beq_refl : vlib.
#[global] Hint Rewrite beq_refl : vlib_trivial.
Notation eqxx := beq_refl.
(* ************************************************************************** *)
(* ************************************************************************** *)
Lemma vlib__negb_rewrite : ∀ b, negb b → b = false.
Proof. by intros []. Qed.
Lemma vlib__andb_split : ∀ b1 b2, b1 && b2 → b1 ∧ b2.
Proof. by intros [] []. Qed.
Lemma vlib__nandb_split : ∀ b1 b2, b1 && b2 = false → b1 = false ∨ b2 = false.
Proof. intros [] []; auto. Qed.
Lemma vlib__orb_split : ∀ b1 b2, b1 || b2 → b1 ∨ b2.
Proof. intros [] []; auto. Qed.
Lemma vlib__norb_split : ∀ b1 b2, b1 || b2 = false → b1 = false ∧ b2 = false.
Proof. intros [] []; auto. Qed.
Lemma vlib__eqb_split : ∀ b1 b2 : bool, (b1 → b2) → (b2 → b1) → b1 = b2.
Proof. intros [] [] H H'; unfold is_true in *; auto using sym_eq. Qed.
Lemma vlib__beq_rewrite : ∀ (T : eqType) (x1 x2 : T), x1 == x2 → x1 = x2.
Proof. by intros *; case eqP. Qed.
Lemma vlib__leq_split : ∀ x1 x2 x3, x1 ≤ x2 → x2 ≤ x3 → x1 ≤ x2 ≤ x3.
Proof. by intros; apply/andP; split. Qed.
Lemma vlib__ltn_split1 : ∀ x1 x2 x3, x1 ≤ x2 → x2 < x3 → x1 ≤ x2 < x3.
Proof. by intros; apply/andP; split. Qed.
Lemma vlib__ltn_split2 : ∀ x1 x2 x3, x1 < x2 → x2 ≤ x3 → x1 < x2 ≤ x3.
Proof. by intros; apply/andP; split. Qed.
Lemma vlib__negb_rewrite : ∀ b, negb b → b = false.
Proof. by intros []. Qed.
Lemma vlib__andb_split : ∀ b1 b2, b1 && b2 → b1 ∧ b2.
Proof. by intros [] []. Qed.
Lemma vlib__nandb_split : ∀ b1 b2, b1 && b2 = false → b1 = false ∨ b2 = false.
Proof. intros [] []; auto. Qed.
Lemma vlib__orb_split : ∀ b1 b2, b1 || b2 → b1 ∨ b2.
Proof. intros [] []; auto. Qed.
Lemma vlib__norb_split : ∀ b1 b2, b1 || b2 = false → b1 = false ∧ b2 = false.
Proof. intros [] []; auto. Qed.
Lemma vlib__eqb_split : ∀ b1 b2 : bool, (b1 → b2) → (b2 → b1) → b1 = b2.
Proof. intros [] [] H H'; unfold is_true in *; auto using sym_eq. Qed.
Lemma vlib__beq_rewrite : ∀ (T : eqType) (x1 x2 : T), x1 == x2 → x1 = x2.
Proof. by intros *; case eqP. Qed.
Lemma vlib__leq_split : ∀ x1 x2 x3, x1 ≤ x2 → x2 ≤ x3 → x1 ≤ x2 ≤ x3.
Proof. by intros; apply/andP; split. Qed.
Lemma vlib__ltn_split1 : ∀ x1 x2 x3, x1 ≤ x2 → x2 < x3 → x1 ≤ x2 < x3.
Proof. by intros; apply/andP; split. Qed.
Lemma vlib__ltn_split2 : ∀ x1 x2 x3, x1 < x2 → x2 ≤ x3 → x1 < x2 ≤ x3.
Proof. by intros; apply/andP; split. Qed.
Set up for basic simplification: database of reflection lemmas
Create HintDb vlib_refl discriminated.
Global Hint Resolve andP orP nandP norP negP vlib__internal_eqP neqP : vlib_refl.
(* Add x <= y <= z splitting to the core hint database. *)
#[global] Hint Immediate vlib__leq_split vlib__ltn_split1 vlib__ltn_split2 : core.
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);
(* Previous statement no longer necessary in 8.4 *) *)
clear H; intros; subst X;
try subst.
Ltac vlib__clarify1 :=
try subst;
repeat match goal with
| [H: is_true (andb _ _) |- _] ⇒
let H' := fresh H in case (vlib__andb_split H); clear H; intros H' 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: is_true (_ == _) |- _] ⇒ generalize (vlib__beq_rewrite H); clear H; intro 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
| [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; discriminate
| H1: ?x = Some _, H2: ?x = Some _ |- _ ⇒ rewrite H2 in H1; vlib__clarify1
end; (* autorewrite with vlib_trivial; *) try done.
Ltac inv x := inversion x; clarify.
Ltac simpls := simpl in *; try done.
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_trivial vlib in × );
(autorewrite with vlib_trivial in × ); try done;
clarify; auto 1 with vlib.
Ltac clarsimp := intros; simpl in *; vlib__clarsimp1.
Ltac autos := clarsimp; auto with vlib.
(* ************************************************************************** *)
Destruct but give useful names
(* ************************************************************************** *)
Destruct, but no case split
Ltac desc :=
repeat match goal with
| H: is_true (_ == _) |- _ ⇒ generalize (vlib__beq_rewrite H); clear H; intro H
| H : ∃ x, ?p |- _ ⇒
let x' := fresh x in destruct H as [x' H]
| H : ?p ∧ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
| H : is_true (_ && _) |- _ ⇒
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ ⇒
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ ⇒ clear H
end.
Ltac des :=
repeat match goal with
| H: is_true (_ == _) |- _ ⇒ generalize (vlib__beq_rewrite H); clear H; intro H
| H : ∃ x, ?p |- _ ⇒
let x' := fresh x in destruct H as [x' H]
| H : exists2 x, ?p & ?q |- _ ⇒
let x' := fresh x in destruct H as [x' H1 H2]
| H : ?p ∧ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
| H : is_true (_ && _) |- _ ⇒
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ ⇒
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ ⇒ clear H
| H : ?p ↔ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
| H : ?p ∨ ?q |- _ ⇒
let x' := H in
let y' := H in
destruct H as [x' | y']
| H : is_true (_ || _) |- _ ⇒ case (vlib__orb_split H); clear H; intro H
| H : (_ && _) = false |- _ ⇒ case (vlib__nandb_split H); clear H; intro H
end.
Ltac des_if_asm :=
clarify;
repeat
match goal with
| H: context[ match ?x with _ ⇒ _ end ] |- _ ⇒
match (type of x) with
| { _ } + { _ } ⇒ destruct x; clarify
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ let Heq := fresh "Heq" in destruct x as [] eqn:Heq; clarify
end
end.
Ltac des_if_goal :=
clarify;
repeat
match goal with
| |- context[match ?x with _ ⇒ _ end] ⇒
match (type of x) with
| { _ } + { _ } ⇒ destruct x; clarify
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ let Heq := fresh "Heq" in destruct x as [] eqn:Heq; clarify
end
end.
Ltac des_if :=
clarify;
repeat
match goal with
| |- context[match ?x with _ ⇒ _ end] ⇒
match (type of x) with
| { _ } + { _ } ⇒ destruct x; clarify
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ 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
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ let Heq := fresh "Heq" in destruct x as [] eqn:Heq; clarify
end
end.
Ltac des_eqrefl :=
match goal with
| H: context[match ?X with |true ⇒ _ | false ⇒ _ end Logic.eq_refl] |- _ ⇒
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
generalize (Logic.eq_refl X);
try (generalize X at 1 3); try (generalize X at 2 3);
intros id' EQ; destruct id'; intros H
| |- context[match ?X with |true ⇒ _ | false ⇒ _ end Logic.eq_refl] ⇒
let EQ := fresh "EQ" in
let id' := fresh "x" in
generalize (Logic.eq_refl X);
try (generalize X at 1 3); try (generalize X at 2 3);
intros id' EQ; destruct id'
end.
Ltac desf_asm := clarify; des; des_if_asm.
Ltac desf := clarify; des; des_if.
Ltac clarassoc := clarsimp; autorewrite with vlib_trivial vlib vlibA in *; try done.
Ltac vlib__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[match ?p with _ ⇒ _ end] ⇒ solve [destruct p; vlib__hacksimp1]
| _ ⇒ solve [f_equal; clarsimp]
end.
(* ************************************************************************** *)
repeat match goal with
| H: is_true (_ == _) |- _ ⇒ generalize (vlib__beq_rewrite H); clear H; intro H
| H : ∃ x, ?p |- _ ⇒
let x' := fresh x in destruct H as [x' H]
| H : ?p ∧ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
| H : is_true (_ && _) |- _ ⇒
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ ⇒
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ ⇒ clear H
end.
Ltac des :=
repeat match goal with
| H: is_true (_ == _) |- _ ⇒ generalize (vlib__beq_rewrite H); clear H; intro H
| H : ∃ x, ?p |- _ ⇒
let x' := fresh x in destruct H as [x' H]
| H : exists2 x, ?p & ?q |- _ ⇒
let x' := fresh x in destruct H as [x' H1 H2]
| H : ?p ∧ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
| H : is_true (_ && _) |- _ ⇒
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ ⇒
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ ⇒ clear H
| H : ?p ↔ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
| H : ?p ∨ ?q |- _ ⇒
let x' := H in
let y' := H in
destruct H as [x' | y']
| H : is_true (_ || _) |- _ ⇒ case (vlib__orb_split H); clear H; intro H
| H : (_ && _) = false |- _ ⇒ case (vlib__nandb_split H); clear H; intro H
end.
Ltac des_if_asm :=
clarify;
repeat
match goal with
| H: context[ match ?x with _ ⇒ _ end ] |- _ ⇒
match (type of x) with
| { _ } + { _ } ⇒ destruct x; clarify
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ let Heq := fresh "Heq" in destruct x as [] eqn:Heq; clarify
end
end.
Ltac des_if_goal :=
clarify;
repeat
match goal with
| |- context[match ?x with _ ⇒ _ end] ⇒
match (type of x) with
| { _ } + { _ } ⇒ destruct x; clarify
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ let Heq := fresh "Heq" in destruct x as [] eqn:Heq; clarify
end
end.
Ltac des_if :=
clarify;
repeat
match goal with
| |- context[match ?x with _ ⇒ _ end] ⇒
match (type of x) with
| { _ } + { _ } ⇒ destruct x; clarify
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ 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
| bool ⇒
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ ⇒ let Heq := fresh "Heq" in destruct x as [] eqn:Heq; clarify
end
end.
Ltac des_eqrefl :=
match goal with
| H: context[match ?X with |true ⇒ _ | false ⇒ _ end Logic.eq_refl] |- _ ⇒
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
generalize (Logic.eq_refl X);
try (generalize X at 1 3); try (generalize X at 2 3);
intros id' EQ; destruct id'; intros H
| |- context[match ?X with |true ⇒ _ | false ⇒ _ end Logic.eq_refl] ⇒
let EQ := fresh "EQ" in
let id' := fresh "x" in
generalize (Logic.eq_refl X);
try (generalize X at 1 3); try (generalize X at 2 3);
intros id' EQ; destruct id'
end.
Ltac desf_asm := clarify; des; des_if_asm.
Ltac desf := clarify; des; des_if.
Ltac clarassoc := clarsimp; autorewrite with vlib_trivial vlib vlibA in *; try done.
Ltac vlib__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[match ?p with _ ⇒ _ end] ⇒ solve [destruct p; vlib__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 for simplifying a sum with constant term.
Usage: simpl_sum_const in H.
H: \sum_(2 <= x < 4) 5 > 0 ==becomes==> H: 5 * (4 - 2) > 0 *)
Ltac simpl_sum_const :=
rewrite ?big_const_nat ?big_const_ord ?big_const_seq iter_addn ?muln1 ?mul1n ?mul0n
?muln0 ?addn0 ?add0n.
(* Tactic for splitting all conjunctions in a hypothesis.
Usage: split_conj H.
H: A /\ (B /\ C) ==becomes==> H1: A
H2: B
H3: C *)
Ltac split_conj X :=
hnf in X;
repeat match goal with
| H : ?p ∧ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
end.
(* Tactic for simplifying a sum with constant term.
Usage: simpl_sum_const in H.
H: \sum_(2 <= x < 4) 5 > 0 ==becomes==> H: 5 * (4 - 2) > 0 *)
Ltac simpl_sum_const :=
rewrite ?big_const_nat ?big_const_ord ?big_const_seq iter_addn ?muln1 ?mul1n ?mul0n
?muln0 ?addn0 ?add0n.
(* Tactic for splitting all conjunctions in a hypothesis.
Usage: split_conj H.
H: A /\ (B /\ C) ==becomes==> H1: A
H2: B
H3: C *)
Ltac split_conj X :=
hnf in X;
repeat match goal with
| H : ?p ∧ ?q |- _ ⇒
let x' := H in
let y' := fresh H in
destruct H as [x' y']
end.