Patrick Nicodemus (Oct 12 2022 at 03:47): Patrick Nicodemus (Oct 12 2022 at 03:47):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
Patrick Nicodemus (Oct 12 2022 at 03:49):Inversion is not helpful as in the nil case it just returns the equality i = i
Patrick Nicodemus (Oct 12 2022 at 07:51):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".
Patrick Nicodemus (Oct 12 2022 at 07:51):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
Gaëtan Gilbert (Oct 12 2022 at 07:53):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)
Patrick Nicodemus (Oct 12 2022 at 07:58):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
Patrick Nicodemus (Oct 12 2022 at 07:59):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
Gaëtan Gilbert (Oct 12 2022 at 07:59):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
Patrick Nicodemus (Oct 12 2022 at 08:01):I see, that's really interesting. I will have to remember that equivalence.
Gaëtan Gilbert (Oct 12 2022 at 08:01):P is exactly the same as @eq A pt just with a different name
Patrick Nicodemus (Oct 12 2022 at 08:04):Yeah I just realized that. It took me a minute.
Patrick Nicodemus (Oct 12 2022 at 08:06):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
Gaëtan Gilbert (Oct 12 2022 at 08:12):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.
Notification Bot (Oct 12 2022 at 15:42):Patrick Nicodemus has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC