The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Wow, thanks, this is fascinating!

On Sat, Feb 22, 2020, 2:22 PM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Ah, I apparently misread Talia's initial question and reformulated it
according to Jason's initial intuition. Sorry for the digression and
thanks for this nice proof (and thanks to Jason for his conclusion).

Hugo

On Sat, Feb 22, 2020 at 04:43:09PM -0500, Arthur Azevedo de Amorim 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

> From mathcomp Require Import all_ssreflect.
>
> Inductive B : Type -> Type := bar : B nat.
>
> Definition eq_of_B T (b : B T) : nat = T :> Type :=
>   match b with bar => erefl end.
>
> Definition B_of_eq T (e : nat = T :> Type) : B T :=
>   match e with erefl => bar end.
>
> Definition B_of_eqK T : cancel (@B_of_eq T) (@eq_of_B T) :=
>   fun e => match e return eq_of_B _ (B_of_eq _ e) = e with erefl => erefl end.
>
> Definition eq_of_BK T : cancel (@eq_of_B T) (@B_of_eq T) :=
>   fun e => match e return B_of_eq _ (eq_of_B _ e) = e with bar => erefl end.
>
> Definition B_of_eq2 (e : @erefl Type nat = erefl) : bar = bar :=
>   congr1 (B_of_eq nat) e.
>
> Definition eq_of_B2 (e : bar = bar) : @erefl Type nat = erefl :=
>   congr1 (eq_of_B nat) e.
>
> Lemma congr1_ext T S (f g : T -> S) (efg : f =1 g) (x y : T) (exy : x = y) :
>   congr1 f exy = etrans (efg x) (etrans (congr1 g exy) (esym (efg y))).
> Proof. by case: y / exy=> /=; case: (g x) / (efg x). Qed.
>
> Definition congr1D (T S R : Type) (g : S -> R) (f : T -> S) (x y : T) (e : x = y) :
>   congr1 g (congr1 f e) = congr1 (g \o f) e :=
>   match e with erefl => erefl end.
>
> Definition congr11 T (x y : T) (e : x = y) : congr1 id e = e :=
>   match e with erefl => erefl end.
>
> Definition etrans1e T (x y : T) (e : x = y) : etrans erefl e = e :=
>   match e with erefl => erefl end.
>
> Lemma B_of_eq2K : cancel B_of_eq2 eq_of_B2.
> Proof.
> move=> e.
> rewrite /eq_of_B2 /B_of_eq2.
> rewrite (congr1D _ _ _ (eq_of_B nat) (B_of_eq nat) _ _ e).
> by rewrite (congr1_ext _ _ _ id (B_of_eqK nat)) /= congr11 etrans1e.
> Qed.
>
> Lemma eq_of_B2K : cancel eq_of_B2 B_of_eq2.
> Proof.
> move=> e.
> rewrite /eq_of_B2 /B_of_eq2.
> rewrite (congr1D _ _ _ (B_of_eq nat) (eq_of_B nat) _ _ e).
> by rewrite (congr1_ext _ _ _ id (eq_of_BK nat)) /= congr11 etrans1e.
> Qed.