Ltac-tically लक्ष्य प्रकार

Question

एक किसी न किसी और अशिक्षित पृष्ठभूमि के रूप में की एक subterm से अधिक सार संक्षेप, HoTT में, एक उपपादन द्वारा परिभाषित प्रकार

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

जो बहुत सामान्य निर्माण

की अनुमति देता है से बाहर बिल्ली deduces

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 होटटी "प्रतिस्थापन" या "पुनः लिखने" रणनीति के केंद्र में होगा; चाल, अब तक मैं यह समझ के रूप में, हो सकता है, एक लक्ष्य है जो आप या मैं संक्षेप में पहचान सकते हैं के रूप में

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

यह पता लगाने की क्या आवश्यक निर्भर प्रकार जी है मान, तो हम कर सकते 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. 

सामान्य नहीं है। यही है, पहले अक्सर उपयोग किया जाता है।

सवाल

[वहाँ है एक | क्या करना है करने के लिए सही बात?

Answer 1

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

शायद आप क्या चाहते हैं करता है प्रकार में संबंधों, जो आपको सिर्फ इतना कहना है rewrite <- y.

इस बीच की अनुमति होगी के लिए फिर से लिखने का उपयोग कर के बारे में bug नहीं है,।

Answer 2

सुविधा his answer में टॉम राजकुमार ने उल्लेख अनुरोध को मान लिया गया है:

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. 

मैं setoid_rewrite <- H जब H : paths x y और जब H : eq x y से लॉग मैं Set Typeclasses Debug साथ मिल की तुलना द्वारा आवश्यक मिले हैं, इसलिए।