The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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
> 
Hi,

I think that your intuition was right. All of "B nat", "B2 nat" and
"nat = nat" are equivalent.

What seems wrong below is that the image of [bar] 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] includes
a coercion from [X] to [nat]).

Hugo