(** * coq10_demo_under.v *)
(** https://www.irit.fr/~Erik.Martin-Dorel/exposes/coq10_demo_under.v *)

(* Setup:

$ coqtop --version
The Coq Proof Assistant, version 8.10+beta2 (September 2019)
compiled with OCaml 4.05.0

$ opam list | grep coq-mathcomp-algebra
coq-mathcomp-algebra 1.9.0
*)

From mathcomp Require Import all_ssreflect all_algebra.
Import GRing.Theory.

(******************************************************************************)

(** ** § Motivating example *)

Lemma slide10 (n : nat) :
  \sum_(0 <= k < n | odd k && (k != 1)) (k - k) = 0.
Fail rewrite subnn.
Fail rewrite eq_big.
rewrite (eq_big (fun k => odd k && (k != 1)) (fun k => 0));
  [ | done | by move=> ? _; rewrite subnn].
Abort.

Lemma slide11 (n : nat) :
  \sum_(0 <= k < n | odd k && (k != 1)) (k - k) = 0.
Proof.
Set Diffs "on". (* Better: enable this option from your IDE menu *)

(* batch mode *)
under eq_big => [k|k _] do [ | rewrite subnn].

Set Diffs "off".
Abort.

Lemma slide12 (n : nat) :
  \sum_(0 <= k < n | odd k && (k != 1)) (k - k) = 0.
Proof.
(* interactive mode *)
under eq_big =>[i | i /andP[i_odd i_neq1]].
- over.
- rewrite subnn. over.
Abort.

(******************************************************************************)

(** ** § Lemma mxtrace_mulC from math-comp/mathcomp/algebra/matrix.v *)

Section ComMatrix.
Variable R : comRingType.
Local Open Scope ring_scope.

(** Original proof *)
Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B :
   \tr (A *m B) = \tr (B *m A).
Proof.
have expand_trM C D: \tr (C *m D) = \sum_i \sum_j C i j * D j i.
  by apply: eq_bigr => i _; rewrite mxE.
rewrite !{}expand_trM exchange_big /=.
by do 2!apply: eq_bigr => ? _; apply: mulrC.
Qed.

(** Possible proof with Coq 8.10 *)
Lemma mxtrace_mulC' m n (A : 'M[R]_(m, n)) B :
   \tr (A *m B) = \tr (B *m A).
Proof.
do 2!under [\tr _]eq_bigr do rewrite mxE.
under [RHS]eq_bigr => i do under eq_bigr => j do rewrite mulrC.
by rewrite exchange_big.
Qed.

End ComMatrix.

(******************************************************************************)

(** ** § examples.v from https://github.com/erikmd/ssr-under-tac *)

Local Open Scope ring_scope.

(* A test with a ssr pattern arg *)
Let test_ssrpat (n : nat) (R : ringType) (f1 f2 g : nat -> R) :
  (\big[+%R/0%R]_(i < n) ((f1 i + f2 i) * g i) +
  \big[+%R/0%R]_(i < n) ((f1 i + f2 i) * g i) =
  \big[+%R/0%R]_(i < n) ((f1 i + f2 i) * g i) +
  \big[+%R/0%R]_(i < n) (f1 i * g i) + \big[+%R/0%R]_(i < n) (f2 i * g i))%R.
Proof.
under eq_bigr => x do rewrite mulrDl.
(* 3 occurrences are rewritten; the bigop variable becomes "x" *)

Undo 1.

under [X in _ + X = _]eq_bigr => x do rewrite mulrDl.

rewrite big_split /=.
by rewrite addrA.
Qed.

(* A test with a side-condition. *)
Let test_sc (n : nat) (R : fieldType) (f : nat -> R) :
  (forall k : 'I_n, 0%R != f k) ->
  (\big[+%R/0%R]_(k < n) (f k / f k) = n%:R)%R.
Proof.
Check divff.
move=> Hneq0; under eq_bigr do [rewrite divff; last by rewrite eq_sym].

under eq_bigr do rewrite -[1]/(1%:R); rewrite -natr_sum.
by rewrite sum1_card cardT size_enum_ord.
Qed.

(* A test lemma for [under eq_bigr in] *)
Let test_rin (n : nat) (R : fieldType) (f : nat -> R) :
  (forall k : 'I_n, f k != 0%R) ->
  (\big[+%R/0%R]_(k < n) (f k / f k) = n%:R)%R -> True.
Proof.
move=> Hneq0 H.
do [under eq_bigr => ? H do rewrite divff //] in H.
done.
Qed.

Local Open Scope nat_scope.

(* A test lemma for [under eq_bigr do under eq_bigl ...] *)
Let test_rl (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 eq_bigr => k Hk do
  under eq_bigl => J do rewrite setIT. (* the bigop variables are kept *)
done.
Qed.

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

(* A test lemma for matrices *)
Let test_addmxC (T : zmodType) (m n : nat) (A B : 'M[T]_(m, n)) :
  (A + B = B + A)%R.
Proof. by under [LHS]eq_mx do rewrite addrC. Qed.

(* A test lemma for sets *)
Let test_setIC (T : finType) (A B : {set T}) : A :&: B = B :&: A.
Proof. by under [LHS]eq_finset do rewrite andbC. Qed.

(* A test with several side-conditions *)
Let test_sc2 (n : nat) :
  \big[addn/O]_(i < n.+1) (n - i)%N = \big[addn/O]_(j < n.+1) j.
Proof.
rewrite (reindex (fun i : 'I_n.+1 => inord (n - i))); last first.
  apply/onW_bij/inv_bij=> -[i Hi]; rewrite inordK ?ltnS ?leq_subr // subKn //.
  by rewrite inord_val.
by under eq_bigr => i _ do
  [rewrite inordK ?ltnS ?leq_subr // subKn; last by case: i].
Qed.

(******************************************************************************)

(** ** § coq/test-suite/ssr/under.v *)

Lemma test_big_nested_1 (F G : nat -> nat) (m n : nat) :
  \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) =
  \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
Proof.
(* in interactive mode *)
under eq_bigr => i Hi.
  under eq_big => [j|j Hj].
  { rewrite muln1. over. }
  { rewrite addnC. over. }
  simpl. (* or: cbv beta. *)
  over.
by [].
Qed.

Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) :
  \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) =
  \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
Proof.
(* in one-liner mode *)
under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite addnC ].
done.
Qed.

Lemma test_big_2cond_0intro (F : nat -> nat) (m : nat) :
  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
Proof.
(* in interactive mode *)
under eq_big.
{ move=> n; rewrite (addnC n 1); over. }
{ move=> i Hi; rewrite (addnC i 2); over. }
done.
Qed.

Lemma test_big_2cond_1intro (F : nat -> nat) (m : nat) :
  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
Proof.
(* in interactive mode *)
Fail under eq_big => i.
(* as it amounts to [under eq_big => [i]] *)
Abort.

Lemma test_big_2cond_all (F : nat -> nat) (m : nat) :
  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
Proof.
(* in interactive mode *)
Fail under eq_big => *.
(* as it amounts to [under eq_big => [*]] *)
Abort.

Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) :
  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
Proof.
(* in one-liner mode *)
under eq_big do [rewrite addnC
                |rewrite addnC].
(* amounts to [under eq_big => [*|*] do [...|...]] *)
done.
Qed.

Lemma test_big_patt1 (F G : nat -> nat) (n : nat) :
  \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0.
Proof.
under [in RHS]eq_bigr => i Hi.
  by rewrite addnC over.
by rewrite addn0.
Qed.

Lemma test_big_patt2 (F G : nat -> nat) (n : nat) :
  \sum_(0 <= i < n) (F i + F i) =
  \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2).
Proof.
under [X in _ = _ + X]eq_bigr => i Hi do rewrite mulnS muln1.
by rewrite big_const_nat iter_addn_0.
Qed.

Lemma test_big_occs (F G : nat -> nat) (n : nat) :
  \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0).
Proof.
under {2}[in RHS]eq_bigr => i Hi do rewrite muln0.
by rewrite big_const_nat iter_addn_0 mul0n addn0.
Qed.

(* Solely used, one such renaming is useless in practice, but it works anyway *)
Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) :
  \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) =
  \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
Proof.
under [RHS]eq_bigr => a _ do under eq_bigr => b _ do []. (* renaming bound vars *)
Abort.

Lemma test_big_andb (F : nat -> nat) (m n : nat) :
  \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1.
Proof.
under eq_bigl => i do [rewrite andb_idl; last by move/eqP->].
under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *)
Abort.

Lemma test_foo (f1 f2 : nat -> nat) (f_eq : forall n, f1 n = f2 n)
      (G : (nat -> nat) -> nat)
      (Lem : forall f1 f2 : nat -> nat,
          True ->
          (forall n, f1 n = f2 n) ->
          False = False ->
          G f1 = G f2) :
  G f1 = G f2.
Proof.
(*
under x: Lem.
- done.
- rewrite f_eq; over.
- done.
 *)
under Lem => [|x|] do [done|rewrite f_eq|done].
done.
Qed.


(** ** Inspired From Coquelicot.Lub. *)
(* http://coquelicot.saclay.inria.fr/html/Coquelicot.Lub.html#Lub_Rbar_eqset *)

Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar).
Parameter Rbar_le : Rbar -> Rbar -> Prop.
Parameter Lub_Rbar : (R -> Prop) -> Rbar.
Parameter Lub_Rbar_eqset :
  forall E1 E2 : R -> Prop,
    (forall x : R, E1 x <-> E2 x) ->
    Lub_Rbar E1 = Lub_Rbar E2.

Lemma test_Lub_Rbar (E : R -> Prop)  :
  Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)).
Proof.
under Lub_Rbar_eqset => r.
by rewrite over.
Abort.


Lemma ex_iff R (P1 P2 : R -> Prop) :
  (forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)).
Proof.
by move=> H; split; move=> [x Hx]; exists x; apply H.
Qed.

Arguments ex_iff [R P1] P2 iffP12.

Require Import Setoid.
Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True.
under ex_iff => n.
by rewrite over.
Abort.