Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(* 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
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.