Add rew dependent Notations

This way when users `Import EqNotations`, we get pretty-printing for
equality `match` statements too.

4 files changed, 185 insertions, 9 deletions

diff --git a/doc/changelog/03-notations/11240-rew-dependent.rst b/doc/changelog/03-notations/11240-rew-dependent.rst
new file mode 100644
index 0000000000..e9daab0c2c
--- /dev/null
+++ b/doc/changelog/03-notations/11240-rew-dependent.rst
@@ -0,0 +1,5 @@
+- **Added**
+  Added :g:`rew dependent` notations for the dependent version of
+  :g:`rew` in :g:`Coq.Init.Logic.EqNotations` to improve the display
+  and parsing of :g:`match` statements on :g:`Logic.eq` (`#11240
+  <https://github.com/coq/coq/pull/11240>`_, by Jason Gross).
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 94b86fc222..b870fa6f6f 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -137,3 +137,71 @@ end = p
      : forall x : nat, x = x -> Prop
 bar  0
      : nat
+let k := rew [P] p in v in k
+     : P y
+let k := rew [P] p in v in k
+     : P y
+let k := rew <- [P] p in v' in k
+     : P x
+let k := rew [P] p in v in k
+     : P y
+let k := rew [P] p in v in k
+     : P y
+let k := rew <- [P] p in v' in k
+     : P x
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+     : P x
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+     : P x
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+     : P y p
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+     : P y p
+let k := rew dependent <- [fun y0 p => id (P' y0 p)] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+     : P y p
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+     : P y p
+let k := rew dependent <- [fun y0 p0 => id (P' y0 p0)] p in v' in k
+     : P' x (eq_sym p)
+rew dependent [P] p in v
+     : P y p
+rew dependent <- [P'] p in v'
+     : P' x (eq_sym p)
+rew dependent [fun a x => id (P a x)] p in v
+     : id (P y p)
+rew dependent <- [fun a p' => id (P' a p')] p in v'
+     : id (P' x (eq_sym p))
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adab324cf0..7d2f1e9ba8 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -251,11 +251,11 @@ Notation NONE := None.
 Check (fun x => match x with SOME x => x | NONE => 0 end).
 
 Notation NONE2 := (@None _).
-Notation SOME2 := (@Some _).     
+Notation SOME2 := (@Some _).
 Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
 
 Notation NONE3 := @None.
-Notation SOME3 := @Some.     
+Notation SOME3 := @Some.
 Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end).
 
 Notation "a :'" := (cons a) (at level 12).
@@ -300,3 +300,61 @@ Definition bar (a b : nat) := plus a b.
 Notation "" := A (format "", only printing).
 Check (bar A 0).
 End M.
+
+(* Check eq notations *)
+Module EqNotationsCheck.
+  Import EqNotations.
+  Section nd.
+    Context (A : Type) (x : A) (P : A -> Type)
+            (y : A) (p : x = y) (v : P x) (v' : P y).
+
+    Check let k : P y := rew p in v in k.
+    Check let k : P y := rew -> p in v in k.
+    Check let k : P x := rew <- p in v' in k.
+    Check let k : P y := rew [P] p in v in k.
+    Check let k : P y := rew -> [P] p in v in k.
+    Check let k : P x := rew <- [P] p in v' in k.
+    Check let k : P y := rew [fun y => P y] p in v in k.
+    Check let k : P y := rew -> [fun y => P y] p in v in k.
+    Check let k : P x := rew <- [fun y => P y] p in v' in k.
+    Check let k : P y := rew [fun (y : A) => P y] p in v in k.
+    Check let k : P y := rew -> [fun (y : A) => P y] p in v in k.
+    Check let k : P x := rew <- [fun (y : A) => P y] p in v' in k.
+  End nd.
+  Section dep.
+    Context (A : Type) (x : A) (P : forall y, x = y -> Type)
+            (y : A) (p : x = y) (P' : forall x, y = x -> Type)
+            (v : P x eq_refl) (v' : P' y eq_refl).
+
+    Check let k : P y p := rew dependent p in v in k.
+    Check let k : P y p := rew dependent -> p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- p in v' in k.
+    Check let k : P y p := rew dependent [P] p in v in k.
+    Check let k : P y p := rew dependent -> [P] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [P'] p in v' in k.
+    Check let k : P y p := rew dependent [fun y p => P y p] p in v in k.
+    Check let k : P y p := rew dependent -> [fun y p => P y p] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => P' y p] p in v' in k.
+    Check let k : P y p := rew dependent [fun y p => id (P y p)] p in v in k.
+    Check let k : P y p := rew dependent -> [fun y p => id (P y p)] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => id (P' y p)] p in v' in k.
+    Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+    Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => P' x p)] p in v' in k.
+    Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+    Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => id (P' x p))] p in v' in k.
+    Check match p as x in _ = a return P a x with
+          | eq_refl => v
+          end.
+    Check match eq_sym p as p' in _ = a return P' a p' with
+          | eq_refl => v'
+          end.
+    Check match p as x in _ = a return id (P a x) with
+          | eq_refl => v
+          end.
+    Check match eq_sym p as p' in _ = a return id (P' a p') with
+          | eq_refl => v'
+          end.
+  End dep.
+End EqNotationsCheck.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4d84d61f9f..8ba17e38c8 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -460,6 +460,58 @@ Module EqNotations.
   Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
     (at level 10, H' at level 10, only parsing).
 
+  Notation "'rew' 'dependent' H 'in' H'"
+    := (match H with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' -> H 'in' H'"
+    := (match H with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, only parsing).
+  Notation "'rew' 'dependent' <- H 'in' H'"
+    := (match eq_sym H with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  <-  H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' [ 'fun' y p => P ] H 'in' H'"
+    := (match H as p in (_ = y) return P with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, y ident, p ident,
+          format "'[' 'rew'  'dependent'  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' -> [ 'fun' y p => P ] H 'in' H'"
+    := (match H as p in (_ = y) return P with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, y ident, p ident, only parsing).
+  Notation "'rew' 'dependent' <- [ 'fun' y p => P ] H 'in' H'"
+    := (match eq_sym H as p in (_ = y) return P with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, y ident, p ident,
+          format "'[' 'rew'  'dependent'  <-  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' [ P ] H 'in' H'"
+    := (match H as p in (_ = y) return P y p with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  [ P ]  '/    ' H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' -> [ P ] H 'in' H'"
+    := (match H as p in (_ = y) return P y p with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          only parsing).
+  Notation "'rew' 'dependent' <- [ P ] H 'in' H'"
+    := (match eq_sym H as p in (_ = y) return P y p with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  <-  [ P ]  '/    ' H  in  '/' H' ']'").
 End EqNotations.
 
 Import EqNotations.
@@ -793,13 +845,6 @@ Qed.
 Declare Left Step iff_stepl.
 Declare Right Step iff_trans.
 
-Local Notation "'rew' 'dependent' H 'in' H'"
-  := (match H with
-      | eq_refl => H'
-      end)
-       (at level 10, H' at level 10,
-        format "'[' 'rew'  'dependent'  '/    ' H  in  '/' H' ']'").
-
 (** Equality for [ex] *)
 Section ex.
   Local Unset Implicit Arguments.