Stream: Coq users

Topic: ✔ Destruct on inductive types


view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Oct 12 2022 at 03:49):

Inversion is not helpful as in the nil case it just returns the equality i = i

view this post on Zulip 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.
 ```

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Oct 12 2022 at 08:01):

I see, that's really interesting. I will have to remember that equivalence.

view this post on Zulip Gaëtan Gilbert (Oct 12 2022 at 08:01):

P is exactly the same as @eq A pt just with a different name

view this post on Zulip Patrick Nicodemus (Oct 12 2022 at 08:04):

Yeah I just realized that. It took me a minute.

view this post on Zulip 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

view this post on Zulip 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 '.

view this post on Zulip Patrick Nicodemus (Oct 12 2022 at 10:15):

I see what you're saying.

view this post on Zulip Notification Bot (Oct 12 2022 at 15:42):

Patrick Nicodemus has marked this topic as resolved.


Last updated: Jun 25 2024 at 15:02 UTC