16

作为一个粗略且未经指导的背景，在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经常被使用。

问题是

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

4

2 回答 2

5

有一个关于对类型中的关系使用重写的错误，这将允许你说rewrite <- y.

同时，

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

可能做你想要的。

于 2012-02-22T03:21:22.617 回答
2

汤姆普林斯在他的回答中提到的功能请求已被批准：

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.

我通过比较Set Typeclasses Debug从setoid_rewrite <- HwhenH : paths x y和 when获得的日志找到了所需的实例H : eq x y。

于 2017-09-29T18:46:00.503 回答