coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "J. Ian Johnson" <ianj AT ccs.neu.edu>
- To: Daniel Schepler <dschepler AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>, "J. Ian Johnson" <ianj AT ccs.neu.edu>
- Subject: Re: [Coq-Club] Stack overflow trying an encode/decode proof.
- Date: Thu, 23 Jan 2014 23:21:01 -0500 (EST)
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
*)
- [Coq-Club] Stack overflow trying an encode/decode proof., J. Ian Johnson, 01/23/2014
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., Daniel Schepler, 01/24/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., J. Ian Johnson, 01/23/2014
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., J. Ian Johnson, 01/23/2014
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., Matthieu Sozeau, 01/24/2014
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., Jason Gross, 01/24/2014
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., Matthieu Sozeau, 01/24/2014
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., J. Ian Johnson, 01/23/2014
- Re: [Coq-Club] Stack overflow trying an encode/decode proof., J. Ian Johnson, 01/24/2014
Archive powered by MHonArc 2.6.18.