## Stream: Coq users

### Topic: ✔ Destruct on inductive types

#### 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.
```
``````

#### Gaëtan Gilbert (Oct 12 2022 at 07:51):

``````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.
``````

#### Gaëtan Gilbert (Oct 12 2022 at 08:00):

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 '.
``````

#### Patrick Nicodemus (Oct 12 2022 at 10:15):

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