Ltac-tycznie abstrahując nad subterm typu bramkowej

Question

Jako szorstkiej i niewyrobionego tle, w HoTT jeden dedukuje cholery z indukcyjnie zdefiniowanego typu

Inductive paths {X : Type } : X -> X -> Type := 
| idpath : forall x: X, paths x x. 

który umożliwia bardzo ogólnobudowlane

Lemma transport {X : Type } (P : X -> Type){ x y : X} (γ : paths x y): 
    P x -> P y. 
Proof. 
induction γ. 
exact (fun a => a). 
Defined. 

Podstawową zasadą HoTT "zastąp" lub "przepisuj"; trick, o ile dobrze rozumiem, byłoby, zakładając cel, który można rozpoznać czy ja abstrakcyjnie jako

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

aby dowiedzieć się, co jest konieczne, rodzaj zależny G, dzięki czemu możemy apply (transport G H). Jak dotąd wszystko, co odkryłem, to to, że nie jest wystarczająco ogólne. Oznacza to, że pierwszy często używa się tego samego.

Pytanie jest

[Czy istnieje | co to jest] Right Thing to Do?

Answer 1

Jest bug temat korzystania przepisać dla stosunków w typie, który pozwoliłby Ci tylko powiedzieć rewrite <- y.

W tym czasie,

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

prawdopodobnie robi to, co chcesz.

Answer 2

Żądanie cechą wymienionych przez Toma Prince'a w his answer została przyznana:

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. 

znalazłem wymaganych wystąpień porównując dzienniki Mam z Set Typeclasses Debug z setoid_rewrite <- H gdy H : paths x y i kiedy H : eq x y.