As a rough and untutored background, in HoTT, one deduces the heck out of the inductively defined type
Inductive paths {X : Type } : X -> X -> Type :=
| idpath : forall x: X, paths x x.
which allows the very general construction
Lemma transport {X : Type } (P : X -> Type ){ x y : X} (γ : paths x y):
P x -> P y.
Proof.
induction γ.
exact (fun a => a).
Defined.
The Lemma transport
would be at the heart of HoTT "replace" or "rewrite" tactics; the trick, so far as I understand it, would be, supposing a goal which you or I can abstractly recognize as
...
H : paths x y
[ Q : (G x) ]
_____________
(G y)
to figure out what is the necessary dependent type G, so that we can apply (transport G H)
. So far, all I've figured out is that
Ltac transport_along γ :=
match (type of γ) with
| ?a ~~> ?b =>
match goal with
|- ?F b => apply (transport F γ)
| _ => idtac "apparently couldn't abstract" b "from the goal." end
| _ => idtac "Are you sure" γ "is a path?" end.
isn't general enough. That is, the first idtac
gets used rather often.
The question is
[Is there a | what is the] Right Thing to Do?
There is a bug about using rewrite for relations in type, which would allow you to just say rewrite <- y.
In the mean time,
Ltac transport_along γ :=
match (type of γ) with
| ?a ~~> ?b => pattern b; apply (transport _ y)
| _ => idtac "Are you sure" γ "is a path?"
end.
probably does what you want.
The feature request mentioned by Tom Prince in his answer has been granted:
Require Import Coq.Setoids.Setoid Coq.Classes.CMorphisms.
Inductive paths {X : Type } : X -> X -> Type :=
| idpath : forall x: X, paths x x.
Lemma transport {X : Type } (P : X -> Type ){ x y : X} (γ : paths x y):
P x -> P y.
Proof.
induction γ.
exact (fun a => a).
Defined.
Global Instance paths_Reflexive {A} : Reflexive (@paths A) := idpath.
Global Instance paths_Symmetric {A} : Symmetric (@paths A).
Proof. intros ?? []; constructor. Defined.
Global Instance proper_paths {A} (x : A) : Proper paths x := idpath x.
Global Instance paths_subrelation
(A : Type) (R : crelation A)
{RR : Reflexive R}
: subrelation paths R.
Proof.
intros ?? p.
apply (transport _ p), RR.
Defined.
Global Instance reflexive_paths_dom_reflexive
{B} {R' : crelation B} {RR' : Reflexive R'}
{A : Type}
: Reflexive (@paths A ==> R')%signature.
Proof. intros ??? []; apply RR'. Defined.
Goal forall (x y : nat) G, paths x y -> G x -> G y.
intros x y G H Q.
rewrite <- H.
exact Q.
Qed.
I found the required instances by comparing the logs I got with Set Typeclasses Debug
from setoid_rewrite <- H
when H : paths x y
and when H : eq x y
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With