The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

Thanks to all who replied. You were very helpful.
-Ian
----- Original Message -----
From: "Daniel Schepler" 
<dschepler AT gmail.com>
To: "J. Ian Johnson" 
<ianj AT ccs.neu.edu>
Cc: "coq-club" 
<coq-club AT inria.fr>
Sent: Thursday, January 23, 2014 8:24:06 PM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] Stack overflow trying an encode/decode proof.


How about something like this for the original problem of showing Fin.t 2 is 
bijective with bool: 



Require Import Vector. 


Definition Fin0_inv (P : Fin.t 0 -> Type) 
(x : Fin.t 0) : P x := 
match x in (Fin.t z) return 
(match z return (Fin.t z -> Type) with 
| 0 => P 
| S _ => fun _ => unit 
end x) with 
| Fin.F1 _ => tt 
| Fin.FS _ _ => tt 
end. 


Definition FinS_inv {n : nat} (P : Fin.t (S n) -> Type) 
(P1 : P Fin.F1) (PS : forall i : Fin.t n, P (Fin.FS i)) 
(x : Fin.t (S n)) : P x := 
match x in (Fin.t Sn) return 
(match Sn return (Fin.t Sn -> Type) with 
| 0 => fun _ => unit 
| S n => fun x => forall P : Fin.t (S n) -> Type, 
P Fin.F1 -> (forall i : Fin.t n, P (Fin.FS i)) -> P x 
end x) with 
| Fin.F1 _ => fun P P1 PS => P1 
| Fin.FS n i => fun P P1 PS => PS i 
end P P1 PS. 


Definition Fin2_inv (P : Fin.t 2 -> Type) 
(P1 : P Fin.F1) (P2 : P (Fin.FS Fin.F1)) : forall i : Fin.t 2, P i := 
FinS_inv P P1 
(FinS_inv (fun i:Fin.t 1 => P (Fin.FS i)) P2 (Fin0_inv _)). 


Definition bool_to_Fin2 (b:bool) : Fin.t 2 := 
if b then Fin.F1 else Fin.FS Fin.F1. 


Definition Fin2_to_bool : Fin.t 2 -> bool := 
Fin2_inv (fun _ => bool) true false. 


Lemma bool_to_Fin2_to_bool : forall b:bool, Fin2_to_bool (bool_to_Fin2 b) = 
b. 
Proof. 
destruct b; reflexivity. 
Qed. 


Lemma Fin2_to_bool_to_Fin2 : forall i:Fin.t 2, bool_to_Fin2 (Fin2_to_bool i) 
= i. 
Proof. 
inversion i using Fin2_inv; reflexivity. 
Qed. 
-- 
Daniel Schepler 



On Thu, Jan 23, 2014 at 1:21 PM, J. Ian Johnson < 
ianj AT ccs.neu.edu
 > wrote: 


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