LProd
Require Export Lvw bijection internalize_tac.
Require Import internalize_tac LNat SumBool.
Section Fix_XY.
Variable X:Set.
Variable intX : registered X.
Variable Y:Set.
Variable intY : registered Y.
Definition prod_enc (t:X*Y) :term :=
match t with
| (x,y) => lam (0 (enc x) (enc y))
end.
(*
(* do not use this, but (internalizes some) once registered!*)
Definition product_pair : term := Eval cbn in .\"x", "y", "f"; "f" "x" "y".
Definition option_some : term := .\"t", "s", "n"; "s" "t".
*)
(*instance contains proc-ness and injectivity of encoding*)
Global Instance register_prod : registered (prod X Y).
Proof.
register prod_enc.
Defined.
Global Instance option_enc_inj (HX : inj_reg intX) (HY : inj_reg intY) : inj_reg register_prod.
Proof.
register_inj.
Defined.
(* now we must register the constructors*)
Global Instance term_pair : internalized (@pair X Y).
Proof.
internalizeC (.\"x", "y", "f"; "f" "x" "y").
Defined.
Lemma prod_enc_correct (p:prod X Y) (s:term): proc s -> enc p s >* match p with (x,y) => s (enc x) (enc y) end.
Proof.
enc_correct.
Qed.
Hint Extern 0 (app (@enc (@prod _ _) _ _) _ >* _)=> apply prod_enc_correct;value : LCor.
Global Instance term_fst : internalized (@fst X Y).
Proof.
internalize. destruct y. crush.
Defined.
Global Instance term_snd : internalized (@snd X Y).
Proof.
internalize. destruct y. crush.
Defined.
Global Instance term_prod_eq_dec : internalized (@prod_eq_dec X Y).
Proof.
pose (f (Dx : eq_dec X) (Dy: eq_dec Y) (p1 p2: X*Y) :=
let (x1,y1) := p1 in
let (x2,y2) := p2 in
to_sumbool (andb (from_sumbool (Dx x1 x2)) (from_sumbool (Dy y1 y2)))).
internalizeWith f. destruct y1,y2. crush. unfold decision. destruct y,y0; crush.
Defined.
End Fix_XY.
Hint Extern 0 (app (@enc (@prod _ _) _ _) _ >* _)=> apply prod_enc_correct;value : LCor.
Require Import internalize_tac LNat SumBool.
Section Fix_XY.
Variable X:Set.
Variable intX : registered X.
Variable Y:Set.
Variable intY : registered Y.
Definition prod_enc (t:X*Y) :term :=
match t with
| (x,y) => lam (0 (enc x) (enc y))
end.
(*
(* do not use this, but (internalizes some) once registered!*)
Definition product_pair : term := Eval cbn in .\"x", "y", "f"; "f" "x" "y".
Definition option_some : term := .\"t", "s", "n"; "s" "t".
*)
(*instance contains proc-ness and injectivity of encoding*)
Global Instance register_prod : registered (prod X Y).
Proof.
register prod_enc.
Defined.
Global Instance option_enc_inj (HX : inj_reg intX) (HY : inj_reg intY) : inj_reg register_prod.
Proof.
register_inj.
Defined.
(* now we must register the constructors*)
Global Instance term_pair : internalized (@pair X Y).
Proof.
internalizeC (.\"x", "y", "f"; "f" "x" "y").
Defined.
Lemma prod_enc_correct (p:prod X Y) (s:term): proc s -> enc p s >* match p with (x,y) => s (enc x) (enc y) end.
Proof.
enc_correct.
Qed.
Hint Extern 0 (app (@enc (@prod _ _) _ _) _ >* _)=> apply prod_enc_correct;value : LCor.
Global Instance term_fst : internalized (@fst X Y).
Proof.
internalize. destruct y. crush.
Defined.
Global Instance term_snd : internalized (@snd X Y).
Proof.
internalize. destruct y. crush.
Defined.
Global Instance term_prod_eq_dec : internalized (@prod_eq_dec X Y).
Proof.
pose (f (Dx : eq_dec X) (Dy: eq_dec Y) (p1 p2: X*Y) :=
let (x1,y1) := p1 in
let (x2,y2) := p2 in
to_sumbool (andb (from_sumbool (Dx x1 x2)) (from_sumbool (Dy y1 y2)))).
internalizeWith f. destruct y1,y2. crush. unfold decision. destruct y,y0; crush.
Defined.
End Fix_XY.
Hint Extern 0 (app (@enc (@prod _ _) _ _) _ >* _)=> apply prod_enc_correct;value : LCor.