The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

To add another bit, I think [eq_refl nat = eq_refl nat] should be isomorphic to the type [(fun x : nat => x) = (fun x => x)], at least if we assume univalence.  (Can this be proven without univalence?). Furthermore, this identity type should be trivial, by the funext equivalence, because nat is discrete.

On Sat, Feb 22, 2020, 15:43 Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

Actually the type [bar = bar] is isomorphic to the type [eq_refl nat =
eq_refl nat].

On Sat, Feb 22, 2020 at 4:25 PM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:
>
> Hi,
>
> That's an interesting question!
>
> I think that Jason's initial intuition was actually right. All of
> [B nat], [B2 nat] and [nat = nat] are easily shown equivalent in
> CIC. And, by relying on a univalent model, they cannot be proved
> equivalent to Talia's type [C tt] which is on the contrary equivalent
> to [unit] (thanks to eta for unit as well as, indeed, that all proofs
> of eta for unit are equal -- this is required since Coq has no
> definitional eta for unit yet).
>
> My own interpretation of what happens is that the image of [bar]
> through the isomorphism between [B nat] and [B2 nat] is not just
> [bar2 nat eq_refl] but [bar2 nat eq_refl] composed with a proof of
> [nat=nat] (since the elimination from [B X] to [B2 X] tacitly includes
> a coercion from [X] to [nat] for the [bar] case).
>
> Best,
>
> Hugo
>
> On Fri, Feb 21, 2020 at 09:00:59PM -0600, Jason Gross wrote:
> > > What is the intuition behind this?
> >
> > The intuition is that all indexed types are isomorphic to corresponding
> > parametric types that use proofs of equality in the constructors.  So
> > Inductive B : Type -> Type :=
> > | bar : B nat.
> > is equivalent to
> > Inductive B2 (T : Type) : Type :=
> > | bar2 : T = nat -> B2 T.
> > This equivalence should be quite straightforward, unless I'm imagining things
> > incorrectly. But then the image of [bar] under this isomorphism is [@bar2 nat
> > refl]. So now we need to ask what the equality type here is.  Well, this
> > should be the same as asking about the loop space based at (nat; refl) in the
> > sigma type { T : Type | T = nat }, because this is the data the constructor
> > carries.  I don't quite have all the details of this part of the proof worked
> > out in my head, so it's about to get more hand-wavy.  My intuition here is that
> > certainly from any loop based at (nat; refl), we can project out a loop nat=
> > nat.  The question that now remains is whether we can go back the other way:
> > can we turn a loop based at nat into a loop based at (nat; refl).  I have
> > conflicting intuitions about this.  My initial intuition was that we could.
> > But now I'm thinking that maybe we can't, because { T : Type | T = nat } is
> > contractible, so we shouldn't be about to find any higher structure here.
> >
> > So it looks like I was actually wrong, initially, and perhaps this gives you
> > the sort of structure/proof you were wanting?
> >
> >
> >
> > On Fri, Feb 21, 2020, 13:20 Talia Ringer <tringer AT cs.washington.edu> wrote:
> >
> >     Interesting feedback. Does anyone have any examples that don't use
> >     SSReflect? I am really not used to SSReflect, and I find it hard to
> >     understand what is happening in proofs written in that style.
> >
> >     Is there a useful induction principle for { l : list T & length l = n }
> >     that people use in general? For example if you'd like to write your list
> >     functions and proofs separately from the invariants about their lengths and
> >     proofs about those invariants. Is there an easy way to glue them together
> >     in general? Could I define this as a single induction principle, something
> >     that takes separately a proof about lists and a proof about its lengths?
> >
> >
> >         It should be pretty easy to show that the equality type [bar = bar] is
> >         isomorphic to the equality type [nat = nat], which is nontrivial if you
> >         assume univalence.  Does this help?
> >
> >
> >     Interesting, so the type of your index really matters, not just the
> >     structure? What is the intuition behind this? It's just weird to me because
> >     I could define another type:
> >
> >
> >         Inductive C : unit -> Type :=
> >         | baz : C tt.
> >
> >
> >     and then you could define indexer functions between B and C that let you
> >     prove an equivalence between B and C at those indices. It should be very
> >     easy to work over equalities between C (because all proofs of unit are
> >     equal to each other). What happens when you transport those equalities to
> >     proofs about equalities between B?
> >
> >     Talia
> >
> >     On Fri, Feb 21, 2020 at 9:04 AM Valentin Robert <
> >     valentin.robert.42 AT gmail.com> wrote:
> >
> >         Very nice, indeed fixing `n`, unlike in the more general `Vector.caseS
> >         `, makes the problems I had go away!
> >
> >         - Valentin
> >
> >         On Fri, 21 Feb 2020 at 17:34, Daniel Schepler <dschepler AT gmail.com>
> >         wrote:
> >
> >             On Fri, Feb 21, 2020 at 2:42 AM Valentin Robert
> >             <valentin.robert.42 AT gmail.com> wrote:
> >             > Or I have to painfully roll my own inversion:
> >             >
> >             > Goal forall T (P : Vector.t T 2 -> Type) v, P v.
> >             >   move => T P v.
> >             >   pose goal :=
> >             >     (
> >             >       fun n v =>
> >             >         match n as n' return Vector.t T n' -> Type with
> >             >         | 2 => P
> >             >         | _ => fun _ => True
> >             >         end v
> >             >     ).
> >
> >             What if instead, you rolled the basic vectorS_inv and vector0_inv
> >             once, and then used those as building blocks?  e.g.
> >
> >             Definition vectorS_inv {X:Type} {n:nat} :
> >               forall P : Vector.t X (S n) -> Type,
> >               (forall (h : X) (t : Vector.t X n), P (Vector.cons _ h _ t)) ->
> >               forall v : Vector.t X (S n), P v.
> >             Admitted.
> >             Definition vector0_inv {X:Type} :
> >               forall P : Vector.t X O -> Type,
> >               P (Vector.nil _) -> forall v : Vector.t X O, P v.
> >             Admitted.
> >
> >             Goal forall {X:Type} (P : Vector.t X 2 -> Type),
> >               (forall a b : X, P (Vector.cons _ a _ (Vector.cons _ b _
> >             (Vector.nil _)))) ->
> >               forall v : Vector.t X 2, P v.
> >             intros X P f v. destruct v as [a0 v'] using @vectorS_inv.
> >             destruct v' as [b0 v''] using @vectorS_inv.
> >             inversion v'' using @vector0_inv. apply f.
> >             Defined.
> >             --
> >             Daniel Schepler
> >



--
Arthur Azevedo de Amorim