LOptions
Require Import internalize_tac.
Section Fix_X.
Variable X:Type.
Variable intX : registered X.
Definition option_enc (t:option X) :term :=
match t with
| Some t => .\"s", "n"; "s" !!(enc t)
| None => .\"s", "n"; "n"
end.
(* do not use this, but (internalizes some) once registered!*)
Definition option_none : term := .\"s", "n"; "n".
Definition option_some : term := .\"t", "s", "n"; "s" "t".
Global Instance register_option : registered (option X).
Proof.
register option_enc.
Defined.
Global Instance option_enc_inj (H : inj_reg intX) : inj_reg register_option.
Proof.
register_inj.
Defined.
(* now we must register the constructors*)
Global Instance term_None : internalized (@None X).
Proof.
internalizeC option_none.
Defined.
Global Instance term_Some : internalized (@Some X).
Proof.
internalizeC option_some.
Defined.
Lemma option_enc_correct (o:option X) (s t:term): proc s -> proc t -> enc o s t >* match o with Some x => s (enc x ) | None => t end.
Proof.
enc_correct.
Qed.
Hint Extern 0 (app (app (@enc (@option X) _ _) _) _ >* _)=> apply option_enc_correct;value : LCor.
Lemma oenc_correct_some s (v : term) : lambda v -> enc s == option_some v -> exists s', s = Some s' /\ v = enc s'.
Proof.
intros lam_v H. lazy [option_some] in H. simpl in H;crushHypo. redStep in H.
apply unique_normal_forms in H;[|value..]. destruct s;simpl in H.
-injection H;eauto.
-discriminate H.
Qed.
Section Fix_X.
Variable X:Type.
Variable intX : registered X.
Definition option_enc (t:option X) :term :=
match t with
| Some t => .\"s", "n"; "s" !!(enc t)
| None => .\"s", "n"; "n"
end.
(* do not use this, but (internalizes some) once registered!*)
Definition option_none : term := .\"s", "n"; "n".
Definition option_some : term := .\"t", "s", "n"; "s" "t".
Global Instance register_option : registered (option X).
Proof.
register option_enc.
Defined.
Global Instance option_enc_inj (H : inj_reg intX) : inj_reg register_option.
Proof.
register_inj.
Defined.
(* now we must register the constructors*)
Global Instance term_None : internalized (@None X).
Proof.
internalizeC option_none.
Defined.
Global Instance term_Some : internalized (@Some X).
Proof.
internalizeC option_some.
Defined.
Lemma option_enc_correct (o:option X) (s t:term): proc s -> proc t -> enc o s t >* match o with Some x => s (enc x ) | None => t end.
Proof.
enc_correct.
Qed.
Hint Extern 0 (app (app (@enc (@option X) _ _) _) _ >* _)=> apply option_enc_correct;value : LCor.
Lemma oenc_correct_some s (v : term) : lambda v -> enc s == option_some v -> exists s', s = Some s' /\ v = enc s'.
Proof.
intros lam_v H. lazy [option_some] in H. simpl in H;crushHypo. redStep in H.
apply unique_normal_forms in H;[|value..]. destruct s;simpl in H.
-injection H;eauto.
-discriminate H.
Qed.
(*
Lemma none_equiv_some v : proc v -> ~ none == some v.
Proof.
intros eq. rewrite some_correct. Lrewrite. apply unique_normal_forms in eq;discriminate|value...
intros H. assert (converges (some v)) by (eexists; split;rewrite <- H; cbv; now unfold none| auto). destruct (app_converges H0) as _ ?. destruct H1 as u [H1 lu]. rewrite H1 in H.
symmetry in H. eapply eqTrans with (s := (lam (lam (1 u)))) in H. eapply eq_lam in H. inv H. symmetry. unfold some. clear H. old_crush. Qed. *)
End Fix_X.
Hint Extern 0 (app (app (@enc (@option _) _ _) _) _ >* _)=> apply option_enc_correct;value : LCor.
(* this is more or lest just an test for internalization automation... *)
Instance term_option_map X Y (Hy:registered Y) (Hx : registered X) : internalized (@option_map X Y).
Proof.
internalize' 0. cbn. intros y u pu H1. intros y' u' pu' H1'. crush. destruct y';crush.
Qed.
(*
Require Import Encoding.
Instance term_unenc : internalized ltac:(Coq_name unenc) unenc.
Proof.
internalizeR. apply size_induction with (x:=y) (f:=size). clear y. intros y IH.
recStep P;crush. destruct y;crush. destruct y;crush. destruct y;crush. destruct n;crush.
*)