The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

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.