Skip to content

Commit

Permalink
New version of bigop_tactics.v.
Browse files Browse the repository at this point in the history 
Summary:
- Add tactic support for eq_bigl (for rewriting bigop predicates).
- Add a shortcut: big := bigop _ _ _.
- Rephrase the tactic notations.
  Before:
    underbig (bigop _ _ _) i Hi rewrite lem.
  Now:
    under big i Hi rewrite lem.
- Improve the Ltac tactics so the bigop variable ("i" or so) is kept,
  if specified.

Note: this file correspond to the first commit of repo
erikmd/ssr-under-tac@e2aeee0

Since then it has been significantly improved thanks to Cyril Cohen's
advice, but the latest version of my tactic only work with the
development version of MathComp, which contains a few bugs related to
the ssrpattern tactic. As soon as both issues
math-comp/math-comp#61 and
math-comp/math-comp#62 are resolved, I will
submit a PR for integrating https://github.com/erikmd/ssr-under-tac in
MathComp (and upgrade validsdp accordingly).
  • Loading branch information
@erikmd
erikmd committed Sep 3, 2016
1 parent 2f383a0 commit 7f6919c
Show file tree
Hide file tree
Showing 2 changed files with 147 additions and 48 deletions.
174 changes: 138 additions & 36 deletions cholesky/bigop_tactics.v
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
From mathcomp Require Import div choice fintype tuple finfun bigop.
From mathcomp Require Import prime binomial ssralg.
From mathcomp Require Import prime binomial ssralg finset.

Set Implicit Arguments.
Unset Strict Implicit.
Expand All @@ -14,59 +14,65 @@ Unset Printing Implicit Defensive.

(** [under_big] allows one to apply a given tactic under the bigop
that correspond to the specified arguments. *)
Ltac under_big b x Hx tac :=
Ltac under_big b i Hi tac :=
let b' := eval hnf in b in
match b' with
| @BigOp.bigop ?R ?I ?idx ?r ?f =>
match f with
| fun i => @BigBody ?R ?I i ?op (@?P i) (@?F1 i) =>
| fun x => @BigBody ?R ?I x ?op (@?P x) (@?F1 x) =>
(* erewrite (@eq_bigr R idx op I r P F1 _); (*not robust enough*) *)
pattern b;
match goal with
| [|- ?G b] =>
refine (@eq_rect_r _ _ G _ b (@eq_bigr R idx op I r P F1 _ _));
[|move=> x Hx; tac;
refine (@eq_rect_r _ _ G _ b
(@eq_bigr R idx op I r P F1 _ _ : _ = @BigOp.bigop _ _ _ _ (fun i => _)));
[|move=> i Hi; tac;
try reflexivity (* instead of "; first reflexivity" *) ];
cbv beta
end
end
end.

(* BEGIN 3rdparty *)
(** The following tactic can be used to add support for patterns to
tactic notation:
It will search for the first subterm of the goal matching [pat], and
then call [tac] with that subterm.
Posted by Ralf Jung on 2016-02-25 to the ssreflect mailing list.
Inpired by Ralf Jung's post on 2016-02-25 to the ssreflect mailing list.
*)
Ltac find_pat pat tac :=
match goal with |- context [?x] =>
unify pat x with typeclass_instances;
tryif tac x then idtac else fail 2
end.
(* END 3rdparty *)
tryif tac x then idtac else fail
end.

(** [underbig] allows one to apply a given tactic under some bigop:
(** [under] allows one to apply a given tactic under some bigop:
if [pat] is a local variable (let-in) that appears in the goal,
only the occurrences of [pat] will be rewritten;
otherwise the occurrences of the first bigop that matches [pat]
will be rewritten. *)
Tactic Notation "underbig" open_constr(pat) simple_intropattern(x) simple_intropattern(Hx) tactic(tac) :=
Tactic Notation "under" open_constr(pat) simple_intropattern(i) simple_intropattern(Hi) tactic(tac) :=
tryif match goal with [|- context [pat]] => is_var pat end
then under_big pat x Hx tac
else find_pat pat ltac:(fun b => under_big b x Hx tac).
then under_big pat i Hi tac
else find_pat pat ltac:(fun b => under_big b i Hi tac).

(** A shortcut when we want to rewrite the first occurrence of [bigop _ _ _] *)
Notation big := (bigop _ _ _) (only parsing).

(** [swap under big ? _ tac] : shortcut for [(under big ? _ tac); last first] *)
Tactic Notation "swap" tactic(tac) :=
tac; last first.

(** ** When the bigop appears in some hypothesis *)

(** [under_big_in] allows one to apply a given tactic under the bigop
that correspond to the specified arguments, in some hypothesis *)
Ltac under_big_in H b x Hx tac :=
Ltac under_big_in H b i Hi tac :=
let b' := eval hnf in b in
match b' with
| @BigOp.bigop ?R ?I ?idx ?r ?f =>
match f with
| fun i => @BigBody ?R ?I i ?op (@?P i) (@?F1 i) =>
| fun x => @BigBody ?R ?I x ?op (@?P x) (@?F1 x) =>
(* erewrite (@eq_bigr R idx op I r P F1 _); (*not robust enough*) *)
pattern b in H;
match type of H with
Expand All @@ -77,8 +83,9 @@ Ltac under_big_in H b x Hx tac :=
shelve_unifiable;
suff new : e;
[ try clear H ; try rename new into H
| refine (@eq_rect _ _ G H _ (@eq_bigr R idx op I r P F1 _ _));
move=> x Hx; tac;
| refine (@eq_rect _ _ G H _
(@eq_bigr R idx op I r P F1 _ _ : _ = @BigOp.bigop _ _ _ _ (fun i => _)));
move=> i Hi; tac;
try reflexivity (* instead of "; first reflexivity" *)
]; try unfold e in * |- *; try clear e ; cbv beta
end
Expand All @@ -88,20 +95,95 @@ Ltac under_big_in H b x Hx tac :=
Ltac find_pat_in H pat tac :=
match type of H with context [?x] =>
unify pat x with typeclass_instances;
tryif tac x then idtac else fail 2
tryif tac x then idtac else fail
end.

(** [under...in] allows one to apply a given tactic under some bigop:
if [pat] is a local variable (let-in) that appears in H,
only the occurrences of [pat] will be rewritten;
otherwise the occurrences of the first bigop that matches [pat]
will be rewritten. *)
Tactic Notation "under" open_constr(pat) "in" hyp(H) simple_intropattern(i) simple_intropattern(Hi) tactic(tac) :=
tryif match type of H with context [pat] => is_var pat end
then under_big_in H pat i Hi tac
else find_pat_in H pat ltac:(fun b => under_big_in H b i Hi tac).

(** * Similar material, for the bigop predicates *)

(** ** When the bigop appears in the goal *)

(** [underp_big] allows one to apply a given tactic for rewriting the
predicate of the bigop corresponding to the specified arguments. *)
Ltac underp_big b i tac :=
let b' := eval hnf in b in
match b' with
| @BigOp.bigop ?R ?I ?idx ?r ?f =>
match f with
| fun x => @BigBody ?R ?I x ?op (@?P1 x) (@?F x) =>
pattern b;
match goal with
| [|- ?G b] =>
refine (@eq_rect_r _ _ G _ b
(@eq_bigl R idx op I r P1 _ F _ : _ = @BigOp.bigop _ _ _ _ (fun i => _)));
[|move=> i; tac;
try reflexivity (* instead of "; first reflexivity" *) ];
cbv beta
end
end
end.

(** [underp] allows one to apply a given tactic for rewriting
some bigop predicate:
if [pat] is a local variable (let-in) that appears in the goal,
only the occurrences of [pat] will be rewritten;
otherwise the occurrences of the first bigop that matches [pat]
will be rewritten. *)
Tactic Notation "underp" open_constr(pat) simple_intropattern(i) tactic(tac) :=
tryif match goal with [|- context [pat]] => is_var pat end
then underp_big pat i tac
else find_pat pat ltac:(fun b => underp_big b i tac).

(** ** When the bigop appears in some hypothesis *)

(** [underp_big_in] allows one to apply a given tactic for rewriting the
predicate of the bigop corresponding to the specified arguments,
in some hypothesis *)
Ltac underp_big_in H b i tac :=
let b' := eval hnf in b in
match b' with
| @BigOp.bigop ?R ?I ?idx ?r ?f =>
match f with
| fun x => @BigBody ?R ?I x ?op (@?P1 x) (@?F x) =>
pattern b in H;
match type of H with
| ?G b =>
let e := fresh in
let new := fresh in
refine (let e := G _ in _);
shelve_unifiable;
suff new : e;
[ try clear H ; try rename new into H
| refine (@eq_rect _ _ G H _
(@eq_bigl R idx op I r P1 _ F _ : _ = @BigOp.bigop _ _ _ _ (fun i => _)));
move=> i; tac;
try reflexivity (* instead of "; first reflexivity" *)
]; try unfold e in * |- *; try clear e ; cbv beta
end
end
end.

(** [underbig…in] allows one to apply a given tactic under some bigop:
(** [underp...in] allows one to apply a given tactic for rewriting
some bigop predicate:
if [pat] is a local variable (let-in) that appears in H,
only the occurrences of [pat] will be rewritten;
otherwise the occurrences of the first bigop that matches [pat]
will be rewritten. *)
Tactic Notation "underbig" "in" hyp(H) open_constr(pat) simple_intropattern(x) simple_intropattern(Hx) tactic(tac) :=
Tactic Notation "underp" open_constr(pat) "in" hyp(H) simple_intropattern(i) tactic(tac) :=
tryif match type of H with context [pat] => is_var pat end
then under_big_in H pat x Hx tac
else find_pat_in H pat ltac:(fun b => under_big_in H b x Hx tac).
then underp_big_in H pat i tac
else find_pat_in H pat ltac:(fun b => underp_big_in H b i tac).

(** ** Tests *)
(** * Tests and examples *)

Section Tests.

Expand All @@ -113,12 +195,12 @@ Let test1 (n : nat) (R : ringType) (f1 f2 g : nat -> R) :
\big[+%R/0%R]_(i < n) (f1 i * g i) + \big[+%R/0%R]_(i < n) (f2 i * g i))%R.
Proof.
set b1 := {2}(bigop _ _ _).
Fail underbig b1 ? _ rewrite GRing.mulrDr.
Fail under b1 x _ rewrite GRing.mulrDr.

underbig b1 ? _ rewrite GRing.mulrDl. (* only b1 is rewritten *)
under b1 x _ rewrite GRing.mulrDl. (* only b1 is rewritten *)

Undo 1. rewrite /b1.
underbig b1 ? _ rewrite GRing.mulrDl. (* 3 occurrences are rewritten *)
under b1 x _ rewrite GRing.mulrDl. (* 3 occurrences are rewritten *)

rewrite big_split /=.
by rewrite GRing.addrA.
Expand All @@ -127,11 +209,11 @@ Qed.
(* A test with a side-condition. *)
Let test2 (n : nat) (R : fieldType) (f : nat -> R) :
(forall k : 'I_n, f k != 0%R) ->
(\big[+%R/0%R]_(i < n) (f i / f i) = n%:R)%R.
(\big[+%R/0%R]_(k < n) (f k / f k) = n%:R)%R.
Proof.
move=> Hneq0.
underbig (bigop _ _ _) ? _ rewrite GRing.divff.
2: done.
swap under big ? _ rewrite GRing.divff. (* the bigop variable becomes "i" *)
done.

rewrite big_const cardT /= size_enum_ord /GRing.natmul.
case: {Hneq0} n =>// n.
Expand All @@ -141,20 +223,40 @@ Qed.
(* Another test lemma when the bigop appears in some hypothesis *)
Let test3 (n : nat) (R : fieldType) (f : nat -> R) :
(forall k : 'I_n, f k != 0%R) ->
(\big[+%R/0%R]_(i < n) (f i / f i) +
\big[+%R/0%R]_(i < n) (f i / f i) = n%:R + n%:R)%R -> True.
(\big[+%R/0%R]_(k < n) (f k / f k) +
\big[+%R/0%R]_(k < n) (f k / f k) = n%:R + n%:R)%R -> True.
Proof.
move=> Hneq0 H.
set b1 := {2}(bigop _ _ _) in H.
underbig in H b1 ? _ rewrite GRing.divff. (* only b1 is rewritten *)
set b1 := {2}big in H.
under b1 in H ? _ rewrite GRing.divff. (* only b1 is rewritten *)
done.

Undo 2.
move: H.
underbig b1 ? _ rewrite GRing.divff.
under b1 ? _ rewrite GRing.divff.
done.

move=> *; exact: Hneq0.
done.
Qed.

(* A test lemma for [underp] *)
Let testp1 (A : finType) (n : nat) (F : A -> nat) :
\big[addn/O]_(0 <= k < n)
\big[addn/O]_(J in {set A} | #|J :&: [set: A]| == k)
\big[addn/O]_(j in J) F j >= 0.
Proof.
under big k _ underp big J rewrite setIT. (* the bigop variables are kept *)
done.
Qed.

(* A test lemma for [underp...in] *)
Let testp2 (A : finType) (n : nat) (F : A -> nat) :
\big[addn/O]_(J in {set A} | #|J :&: [set: A]| == 1)
\big[addn/O]_(j in J) F j = \big[addn/O]_(j in A) F j -> True.
Proof.
move=> H.
underp big in H J rewrite setIT. (* the bigop variable "J" is kept *)
done.
Qed.

End Tests.
21 changes: 9 additions & 12 deletions cholesky/validsdp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -507,9 +507,6 @@ Qed.

Require Import bigop_tactics.

Tactic Notation "underbigs" simple_intropattern(x) simple_intropattern(Hx)
tactic(tac) := underbig (bigop _ _ _) x Hx tac.

Lemma soscheck_correct p z Q : soscheck_ssr p z Q ->
forall x, 0 <= (map_mpoly T2R p).@[x].
Proof.
Expand Down Expand Up @@ -553,21 +550,21 @@ have : exists E : 'M_s.+1,
rewrite -{1}(Rmult_1_r (T2R r)); apply Rmult_le_compat_l=>//. }
apply/mpolyP => m; rewrite mcoeff_map_mpoly /= mxE.
set M := (Q'r + _)%R.
underbigs ? _ rewrite mxE big_distrl /=; underbigs ? _ rewrite mxE.
under big ? _ rewrite mxE big_distrl /=; under big ? _ rewrite mxE.
rewrite pair_bigA /= (big_morph _ (GRing.raddfD _) (mcoeff0 _ _)) /=.
have -> : M = map_mpolyC_R (matrix.map_mx (T2R \o F2T) Q + E)%R.
{ apply/matrixP=> i j; rewrite /map_mpolyC_R /mpolyC_R.
by rewrite !mxE mpolyCD (map_mpolyC (GRing.raddf0 _)). }
move {M}; set M := map_mpolyC_R _.
underbigs ? _ rewrite (GRing.mulrC (zpr _ _)) -GRing.mulrA mxE mcoeffCM.
underbigs ? _ rewrite GRing.mulrC 2!mxE -mpolyXD mcoeffX.
under big ? _ rewrite (GRing.mulrC (zpr _ _)) -GRing.mulrA mxE mcoeffCM.
under big ? _ rewrite GRing.mulrC 2!mxE -mpolyXD mcoeffX.
rewrite (bigID (fun ij => zij ij.2 ij.1 == m)) /= GRing.addrC.
rewrite big1 ?GRing.add0r; last first.
{ by move=> ij; move/negbTE=> ->; rewrite GRing.mul0r. }
underbigs ? Hi rewrite Hi GRing.mul1r 2!mxE.
under big ? Hi rewrite Hi GRing.mul1r 2!mxE.
rewrite big_split /= GRing.addrC.
pose nbm := size [seq ij <- index_enum I_sp1_2 | zij ij.2 ij.1 == m].
underbigs ? Hi
under big ? Hi
(move/eqP in Hi; rewrite mxE /nbij Hi -/nbm mcoeffB GRing.raddfB /=).
rewrite misc.big_sum_pred_const -/nbm -[_ / _]/(_ * / _)%R.
rewrite GRing.mulrDl GRing.mulrDr -GRing.addrA.
Expand All @@ -580,12 +577,12 @@ have : exists E : 'M_s.+1,
by apply/ltP/card_gt0P; exists (j, i); rewrite /in_mem /=. }
by rewrite mcoeff_msupp; move/eqP->; rewrite GRing.raddf0 GRing.mul0r. }
rewrite /p' mxE.
underbigs ? _ (rewrite mxE big_distrl /=; underbigs ? _ rewrite mxE).
under big ? _ (rewrite mxE big_distrl /=; under big ? _ rewrite mxE).
rewrite pair_bigA /= (big_morph _ (GRing.raddfD _) (mcoeff0 _ _)) /=.
underbigs ? _ rewrite (GRing.mulrC (zp _ _)) -GRing.mulrA mxE mcoeffCM.
underbigs ? _ rewrite GRing.mulrC 2!mxE -mpolyXD mcoeffX.
under big ? _ rewrite (GRing.mulrC (zp _ _)) -GRing.mulrA mxE mcoeffCM.
under big ? _ rewrite GRing.mulrC 2!mxE -mpolyXD mcoeffX.
rewrite GRing.raddf_sum /= (bigID (fun ij => zij ij.2 ij.1 == m)) /=.
underbigs ? Hi rewrite Hi GRing.mul1r.
under big ? Hi rewrite Hi GRing.mul1r.
set b := bigop _ _ _; rewrite big1; last first; [|rewrite {}/b GRing.addr0].
{ by move=> ij; move/negbTE => ->; rewrite GRing.mul0r GRing.raddf0. }
rewrite -big_filter /nbm /I_sp1_2; case [seq i <- _ | _].
Expand Down

0 comments on commit 7f6919c

Please sign in to comment.