在目标类型的子项上进行抽象抽象

Question

作为一个粗略和未经训练的背景,在HoTT中,可以推断出归纳定义的类型

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.

这Lemma transport 将是HoTT"替换"或"改写"战术的核心; 据我所知,诀窍就是假设你或我可以抽象地认出的目标

...
H : paths x y
[ Q : (G x) ]
_____________
(G y)

找出什么是必要的依赖类型G,以便我们可以apply (transport G H).到目前为止,我所知道的就是那个

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.

不够通用.也就是说,第一个idtac经常被使用.

问题是

[有没有| 什么是正确的事情？

Answer 1

关于在类型中使用重写关系有一个错误,这可以让你说rewrite <- y.

同时,

Ltac transport_along ? :=
  match (type of ?) with 
    | ?a ~~> ?b => pattern b; apply (transport _ y)
    | _ => idtac "Are you sure" ? "is a path?"
  end.

可能做你想要的.