search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.26k stars 193 forks source link

Tactic decomposing_intros loop infinitely on goals containing the list type #1414

Open necrosovereign opened 3 years ago

necrosovereign commented 3 years ago

Tactic decomposing_intros (and, therefore, make_equiv) cannot be used when the goal contains the list type, because it goes into a infinite loop.

Example.

Require Import HoTT.Basics.

Goal forall A, { l : list A, l = l } -> Unit.
    decomposing intros. (* never finishes *)

My guess is that it has something to do with list being a recursive type

Alizter commented 3 years ago

Are you doing this with regular coq? I can't get it to work in the library.

necrosovereign commented 3 years ago

Sorry, I've just noticed that I've made a typo in the example: it should be decomposing_intros instead of decomposing intros. The corrected example:

Require Import HoTT.Basics.

Goal forall A, { l : list A, l = l } -> Unit.
    decomposing_intros. (* never finishes *)

I tested it in hoqtop version 8.12+alpha, but the definition of decomposing_intros on my installation is identical to the one in the repository, so I've assumed that it's still an issue.

If it has been fixed in the latest version, that I'm okay with this.

Alizter commented 3 years ago

Yes, this seems to be a problem. @JasonGross is the author of this tactic.

JasonGross commented 3 years ago

You probably want to add a fail 1 case for any recursive types you want it to handle to https://github.com/HoTT/HoTT/blob/46f10ef3c7218b912c6686ecec650e728c69085e/theories/Basics/Equivalences.v#L565-L569

Alternatively, we could try writing a tactic to determine whether or not some type is recursive or something. What should the spec of the tactic be?