I have a definition of a path in a quiver. Here A
and B
are supposed to be thought of as the type of nodes and edges respectively
Inductive tlist (A : Type) ( B : A -> A -> Type) (k : A) : A -> Type :=
| tnil : tlist k
| tcons i j : tlist j -> B i j -> tlist i.
i am trying to prove a goal of the form
i : A
f : tlist i i
H : match f with tnil => True | tcons _ _ => False end
----------
tnil i = f
and I am stuck. I cannot destruct f because it complains about it being ill-typed as it tries to abstract the annotation in tlist
, so then f
becomes of type tlist i j
for some new variable j
and tnil i
is of type tlist i i
so the equation is not well typed. I have been trying to use 'remember' and similar tactics to decouple i
and j
with the idea that i could transport across the equality but this has not been helpful, the dilemma seems to be that at some point I have to destruct the equality too. If I destruct f first then I am left with a branch of the form tnil = transport p tnil
where p : i = i
, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy, but I am looking for a way to do it without this
Inversion is not helpful as in the nil case it just returns the equality i = i
I guess it boils down to
Context (A : Type).
Context (pt : A).
Inductive P : A -> Type :=
| c : P pt.
Goal forall (H : P pt), H = c.
```
Inductive tlist (A : Type) ( B : A -> A -> Type) (k : A) : A -> Type :=
| tnil : tlist k
| tcons i j : tlist j -> B i j -> tlist i.
says The term "k" has type "A" while it is expected to have type "Type".
Gaëtan Gilbert said:
Inductive tlist (A : Type) ( B : A -> A -> Type) (k : A) : A -> Type := | tnil : tlist k | tcons i j : tlist j -> B i j -> tlist i.
says
The term "k" has type "A" while it is expected to have type "Type".
Ok, sorry, I must have screwed up copying it. I will edit the message
I am left with a branch of the form tnil = transport p tnil where p : i = i, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy
note that in this case p is an equality between nats, and uip for nat it true (Eqdep_dec.UIP_refl_nat)
Context (A : Type) (B : A -> A -> Type).
Inductive tlist' (k : A) : A -> Type :=
| tnil : tlist' k
| tcons : ∀ i j : A, B i j -> tlist' j -> tlist' i.
Definition tlist_is_nil (i : A) (f : tlist' i i) :=
match f return Type with tnil _ => True | tcons _ _ _ _ _ => False end.
Proposition tlist_quiver_nilcase (i : A) (f : tlist' i i) (H : tlist_is_nil i f) : tnil i = f.
I think this is a self contained version of what I am trying to prove
Gaëtan Gilbert said:
I am left with a branch of the form tnil = transport p tnil where p : i = i, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy
note that in this case p is an equality between nats, and uip for nat it true (Eqdep_dec.UIP_refl_nat)
I see, ok. Are you suggest I convert the lists to their lengths or something? I don't understand what you mean by nats
I guess it boils down to
that is one way to state UIP
Section S.
Context (A : Type).
Context (pt : A).
Inductive P : A -> Type :=
| c : P pt.
Axiom thing : forall (H : P pt), H = c.
Definition to_eq {y} (e:P y) : pt = y := match e with c => eq_refl end.
Definition from_eq {y} (e:pt = y) : P y := match e with eq_refl => c end.
Lemma to_from_eq {y} e : to_eq (@from_eq y e) = e.
Proof.
destruct e;reflexivity.
Qed.
Theorem uip (e:pt=pt) : e = eq_refl.
Proof.
rewrite <-(to_from_eq e).
change eq_refl with (to_eq c).
f_equal.
apply thing.
Qed.
End S.
Patrick Nicodemus said:
Gaëtan Gilbert said:
I am left with a branch of the form tnil = transport p tnil where p : i = i, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy
note that in this case p is an equality between nats, and uip for nat it true (Eqdep_dec.UIP_refl_nat)
I see, ok. Are you suggest I convert the lists to their lengths or something? I don't understand what you mean by nats
sorry, I misread and thought i:nat
I see, that's really interesting. I will have to remember that equivalence.
P is exactly the same as @eq A pt
just with a different name
Yeah I just realized that. It took me a minute.
I guess the way I have defined my inductive type of paths in the graph, an empty list of edges starting at node i
is essentially equivalent to a proof of i = i
and so I won't be able to prove that there's a unique empty list tnil
without assuming A
satisfies axiom K
you can turn your inductive into an equivalent one (up to isomorphism) by turning indices into (non uniform) parameters and adding equalities:
Inductive tlist' (k : A) (k' : A) : Type :=
| tnil : k = k' -> tlist' k k'
| tcons : ∀ i j : A, B i j -> tlist' k j -> i = k' -> tlist' k k '.
optionally you can then simplify if you have the pattern forall i, ... -> i = k' -> ...
to remove i and just use k' in that constructor (because {i & i = k'}
is contractible) getting
Inductive tlist' (k : A) (k' : A) : Type :=
| tnil : k = k' -> tlist' k k'
| tcons : ∀ j : A, B i j -> tlist' k j -> tlist' k k '.
I see what you're saying.
Patrick Nicodemus has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC