dependent_rewrite.v

(* check the behaviour of Coq's rewrite tactics *)

Parameter T : Type.

Lemma mmm1 : forall (x y:T) (p : x = y),
    existT (fun (y':T) => x = y') y p = existT (fun (y':T) => x = y') x (eq_refl x).
Proof.
  intros.
  rewrite p.
  reflexivity.
Qed.

Print mmm1.

(* Coq v8.3
Coq < Print mmm1.
mmm1 = 
fun (x y : T) (p : x = y) =>
eq_rew_r_dep T x y
  (fun (x0 : T) (p0 : x0 = y) =>
   existT (fun y' : T => x0 = y') y p0 =
   existT (fun y' : T => x0 = y') x0 (eq_refl x0))
  (eq_refl (existT (fun y' : T => y = y') y (eq_refl y))) p
     : forall (x y : T) (p : x = y),
       existT (fun y' : T => x = y') y p =
       existT (fun y' : T => x = y') x (eq_refl x)

Coq < Print eq_rew_r_dep.
eq_rew_r_dep = 
fun (A : Type) (x y : A) (P : forall y0 : A, y0 = y -> Type)
  (HC : P y (eq_refl y)) (H : x = y) =>
match eq_sym_involutive A x y H in (_ = H0) return (P x H0) with
| eq_refl =>
    match
      eq_sym A x y H as H0 in (_ = y0) return (P y0 (eq_sym A y y0 H0))
    with
    | eq_refl => HC
    end
end
     : forall (A : Type) (x y : A) (P : forall y0 : A, y0 = y -> Type),
       P y (eq_refl y) -> forall H : x = y, P x H

Argument scopes are [type_scope _ _ _ _ _]

Coq < Print eq_sym_involutive.
eq_sym_involutive = 
fun (A : Type) (x y : A) (H : x = y) =>
match H as H0 in (_ = y0) return (eq_sym A y0 x (eq_sym A x y0 H0) = H0) with
| eq_refl => eq_refl (eq_refl x)
end
     : forall (A : Type) (x y : A) (H : x = y),
       eq_sym A y x (eq_sym A x y H) = H

Argument scopes are [type_scope _ _ _]

Coq < Print eq_sym.
eq_sym = 
fun (A : Type) (x y : A) (H : x = y) =>
match H in (_ = y0) return (y0 = x) with
| eq_refl => eq_refl x
end
     : forall (A : Type) (x y : A), x = y -> y = x

Argument scopes are [type_scope _ _ _]
*)

(* Coq v8.6.1
mmm1 = 
let Top_internal_eq_sym_internal :=
  (fun (A : Type) (x y : A) (H : x = y) =>
   match H in (_ = y0) return (y0 = x) with
   | eq_refl => eq_refl
   end)
  :
  forall (A : Type) (x y : A), x = y -> y = x in
let Top_internal_eq_sym_involutive :=
  (fun (A : Type) (x y : A) (H : x = y) =>
   match
     H as H0 in (_ = y0)
     return
       (Top_internal_eq_sym_internal A y0 x (Top_internal_eq_sym_internal A x y0 H0) = H0)
   with
   | eq_refl => eq_refl
   end)
  :
  forall (A : Type) (x y : A) (H : x = y),
  Top_internal_eq_sym_internal A y x (Top_internal_eq_sym_internal A x y H) = H in
let Top_internal_eq_rew_r_dep :=
  fun (A : Type) (x y : A) (P : forall y0 : A, y0 = y -> Type) (HC : P y eq_refl) (H : x = y)
  =>
  match Top_internal_eq_sym_involutive A x y H in (_ = H0) return (P x H0) with
  | eq_refl =>
      match
        Top_internal_eq_sym_internal A x y H as H0 in (_ = y0)
        return (P y0 (Top_internal_eq_sym_internal A y y0 H0))
      with
      | eq_refl => HC
      end
  end in
fun (x y : T) (p : x = y) =>
Top_internal_eq_rew_r_dep T x y
  (fun (x0 : T) (p0 : x0 = y) =>
   existT (fun y' : T => x0 = y') y p0 = existT (fun y' : T => x0 = y') x0 eq_refl) eq_refl p
     : forall (x y : T) (p : x = y),
       existT (fun y' : T => x = y') y p = existT (fun y' : T => x = y') x eq_refl
*)


(* the original one at https://twitter.com/keigoi/status/928573689913688064 *)
Notation "<< x , y , p >>" :=
  (existT (fun x' => _) x
          (existT (fun y' => _) y p)).

Lemma mmm2 : forall (x y:T) (p : x = y), << x, y, p >> = << x, x, eq_refl x >>.
Proof.
  intros.
  (* refine (match p with eq_refl => _ end). *)
  (* destruct p. *)
  rewrite p.
  reflexivity.
Qed.

Check (fun (x y :T) (p : x = y) =>
        (existT (fun (_:T) => {y' : T & x = y'}) x
                (existT (fun (y':T) => x = y') y p)))
: forall (x y : T),
       x = y -> {x' : T & {y' : T & x = y'}}.

Check (fun (x :T) =>
        (existT (fun (_:T) => {y' : T & x = y'}) x
                (existT (fun (y':T) => x = y') x (eq_refl x))))
: forall (x : T), {x' : T & {y' : T & x = y'}}.


(* plain old rewriting *)
Lemma m : forall (x y:T), x = y -> y = x.
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

Print m.
(*
m = 
fun (x y : T) (H : x = y) => eq_ind_r (fun x0 : T => y = x0) eq_refl H
     : forall x y : T, x = y -> y = x
 *)