Comme un fond rugueux et untutored, dans HoTT, on en déduit le diable du type inductif définiLtac-tiquement abstraire sur une sous-terme du type d'objectif
Inductive paths {X : Type } : X -> X -> Type :=
| idpath : forall x: X, paths x x.
qui permet la construction très générale
Lemma transport {X : Type } (P : X -> Type){ x y : X} (γ : paths x y):
P x -> P y.
Proof.
induction γ.
exact (fun a => a).
Defined.
Le Lemma transport
serait le être au cœur des tactiques «remplacer» ou «réécrire» de HoTT; l'affaire, pour autant que je le comprends, serait, en supposant un objectif que vous ou je peux abstraitement reconnaître comme
...
H : paths x y
[ Q : (G x) ]
_____________
(G y)
pour savoir quel est le type dépendant nécessaire G, afin que nous puissions apply (transport G H)
. Jusqu'à présent, tout ce que j'ai compris est que
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.
n'est pas assez générale. Autrement dit, la première s'utilise assez souvent.
La question est
[Y at-il un | quel est le] Right Thing to Do?