coq - 对目标类型的子项进行逻辑抽象

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经常使用。

问题是

[Is there a | what is the] Right Thing to Do?

Answer 1

有一个bug关于对类型中的关系使用重写，这将允许您只说 rewrite <- y.
同时，

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

可能会做你想要的。