The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

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
> *)