The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I've added a smaller version of this example (reported on irc) to https://coq.inria.fr/bugs/show_bug.cgi?id=3010.

-Jason

On Thu, Jan 23, 2014 at 3:19 PM, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:

Hi,

  that’s a bug in return clause inference it seems:

Definition fin_decode1 (b : t 2) : True :=

 match b as b' in (t n) return ((match n as n' return n = n' -> _ with

                                       0 => (fun H : n = 0 => False)
                                     | S n' =>
                                       (fun H : n = S n' =>

                                          True)

                                  end) (eq_refl n))
  with
     F1 _ => I
   | FS _ _ => I
 end.

works.

On 23 janv. 2014, at 13:59, J. Ian Johnson <ianj AT ccs.neu.edu> wrote:

> Whoops, change the Prop in the motive to True.
> ystael on #coq got this to go through with 8.4pl1, but my 8.4pl2 has a stack overflow. Must be a bug.
> -Ian
> ----- Original Message -----
> From: "J. Ian Johnson" <ianj AT ccs.neu.edu>
> To: "J. Ian Johnson" <ianj AT ccs.neu.edu>
> Cc: "coq-club" <coq-club AT inria.fr>
> Sent: Thursday, January 23, 2014 4:33:12 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [Coq-Club] Stack overflow trying an encode/decode proof.
>
> Narrowed down the stack overflow to the following function, which I think should be pretty innocuous.
>
> Require Import Vectors.Fin.
> Definition fin_decode1 (b : t 2) : True :=
>  match b as b' in (t n) return ((match n with
>                                        0 => (fun H : n = 0 => False)
>                                      | S n' =>
>                                        (fun H : n = S n' =>
>                                           Prop)
>                                   end) (eq_refl n))
>   with
>      F1 _ => I
>    | FS _ _ => I
>  end.
>
> -Ian
> ----- Original Message -----
> From: "J. Ian Johnson" <ianj AT ccs.neu.edu>
> To: "coq-club" <coq-club AT inria.fr>
> Sent: Thursday, January 23, 2014 4:21:44 PM GMT -05:00 US/Canada Eastern
> Subject: [Coq-Club] Stack overflow trying an encode/decode proof.
>
> I'm trying to formalize the notion of a finite type as one that is equivalent to (fin n) for some n.
> I'm using "t" from Vectors.Fin as "fin" in my code. The rest of this email is coq code with comments describing what I tried and where things go wrong.
> The gist is I tried a fancy motive to get around an ill-typed term after destructing something, and since I apparently don't know quite well enough what I'm doing, explosion.
>
> (* Here's where I started: *)
> Definition Finite (A : Type) : Prop :=
>  exists (n : nat) (f : A -> fin n), Bi_inv f. (* HoTT's Bi_inv with Prop equality *)
>
> Remark bool_fin : Finite bool.
> Proof.
> exists 2, (fun a : bool => if a then F1 else FS F1).
> apply Quasi_bi_inv.
> exists (fun f : fin 2 => match f with F1 _ => true | FS _ _ => false end).
> (* destructing b leads to ill-typed term. *)
> Abort.
>
> (*So I try the encode/decode method with two codes for the two fins I need to deal with:*)
>
> Definition fin_code1 (b : fin 2) : Prop :=
>  match b with
>      F1 _=> b = F1
>    | FS _ _ => False
>  end.
> Definition fin_code2 (b : fin 2) : Prop :=
>  match b with
>      F1 _=> False
>    | FS _ _ => b = FS F1
>  end.
> Definition fin_encode1 (b : fin 2) (p : b = F1) : fin_code1 b.
> unfold fin_code1; rewrite p; reflexivity.
> Defined.
> Definition fin_encode2 (b : fin 2) (p : b = FS F1) : fin_code2 b.
> unfold fin_code1; rewrite p; reflexivity.
> Defined.
>
> (*All is well, so now I need decode functions.*)
>
> (* How about this? Uncomment for the error. Basically, I can't have two different types for H without a fancy motive.
>
> Definition fin_decode1 (b : fin 2) (c : fin_code1 b) : F1 = b :=
>  (match b with
>      F1 _ => (fun (H : F1 = b) (H0 : fin_code1 F1) =>
>                 H)
>    | FS _ _ => (fun (H : b = FS F1) (H0 : fin_code1 (FS F1)) =>
>                   match H0 with end)
>  end (eq_refl b) c)
>
> *)
>
> (* Let's try a fancy motive! I'm pretty sure this should work...
>
> Definition fin_decode1 (b : fin 2) (c : fin_code1 b) : F1 = b :=
>  (match b as b' in (fin n) return (match b' with
>                                        F1 _ => F1 = b -> fin_code1 F1 -> F1 = b
>                                      | FS _ _ => b = FS F1 -> fin_code1 (FS F1) -> F1 = b
>                                    end)
>   with
>      F1 _ => (fun (H : F1 = b) (H0 : fin_code1 F1) =>
>                 H)
>    | FS _ _ => (fun (H : b = FS F1) (H0 : fin_code1 (FS F1)) =>
>                   match H0 with end)
>  end (eq_refl b) c).
>
> Nope, the return type is a match, and I thus can't apply it to (eq_refl b). What now?
> Well, I wasn't sure whether to have b or b' in the return type, but it yelled at me when I put b',
> since I didn't have the fin type's index figured out. Let's try to do something better about that.
> *)
>
> Definition fin_decode1 (b : fin 2) (c : fin_code1 b) : F1 = b :=
>  (match b as b' in (fin n) return ((match n with
>                                        0 => (fun H : n = 0 => False)
>                                      | S n' =>
>                                        (fun H : n = S n' =>
>                                           (match b' with
>                                                F1 _ => (@F1 n') = b' -> fin_code1 F1 -> F1 = b'
>                                              | FS _ _ => b' = FS (@F1 1) -> fin_code1 (FS F1) -> F1 = b'
>                                            end))
>                                          end) (eq_refl n))
>   with
>      F1 _ => (fun (H : F1 = b) (H0 : fin_code1 F1) =>
>                 H)
>    | FS _ _ => (fun (H : b = FS F1) (H0 : fin_code1 (FS F1)) =>
>                   match H0 with end)
>  end (eq_refl b) c).
>
> (* STACK OVERFLOW! Well, I'm out of ideas. Better go to coq-club. Any assistance is appreciated.
>
> -Ian
> *)