internalize_def
Require Export Lvw.
Require Import bijection String.
(* Typeclass for registering types *)
Class registered (X : Type) := mk_registered
{
enc_f : X -> term ; (* the encoding function for X *)
proc_enc : forall x, proc (enc_f x) (* encodings need to be a procedure *)
}.
Class inj_reg (X:Type) (H:registered X) := mk_inj_reg
{
inj_enc : injective enc_f
}.
Arguments enc_f X {registered} _.
Definition enc (X : Type) (H:registered X) := enc_f X.
Global Arguments enc {X} {H} x : simpl never.
(*Notation "'enc' s" := (encode s) (at level 10).*)
(* Definition of the valid types for internalization *)
Inductive TT : Type -> Type :=
TyB t (H : registered t) : TT t
| TyElim (t:Type) : TT t
| TyAll t (ttt : TT t) (f : t -> Type) (ftt : forall x, TT (f x))
: TT (forall (x:t), f x).
Arguments TyB _ {_}.
Arguments TyAll {_} _ {_} _.
Notation "! X" := (TyB X) (at level 69).
(*Notation "X ~> Y" := (TyAll X (fun _ => Y)) (right associativity, at level 70).*)
Notation "X ~> Y" := (TyAll X (fun _ => Y)) (right associativity, at level 70).
(*
Ltac test x:= exact (x + 10).
Notation "!! X" := ( ltac:(test X ) ) (at level 100).
Compute (!! 10).
*)
(*Notation "\X ~> Y" := (TyAll X Y) (right associativity, at level 70).*)
(*
Axiom reg : registered nat.
Compute ( !nat ~> ! nat ~> ! nat).
*)
Definition internalizesF (p : Lvw.term) t (ty : TT t) (f : t) : Prop.
revert p. induction ty as [ t H p | t H p | t ty internalizesHyp R ftt internalizesF']; simpl in *;intros.
- exact (p >* enc f).
- exact (p >* I).
- exact (forall (y : t) u, proc u -> internalizesHyp y u -> internalizesF' y (f y) (app p u)).
Defined.
(*
destruct ty.
+exact (forall (y : t), X y (f y) (app p (enc y))).
+exact (forall (y : t), X y (f y) (app p I)).
+exact (forall (y : (forall x : t, f1 x)) u, proc u -> IHty y u -> X y (f y) (app p u)).*)
(*
Definition intFPretty (p : Lvw.term) t (ty : TT t) (f : t) : Prop.
revert p. induction ty; simpl in *;intros.
- exact (p>* enc f).
- exact (p>* I).
- destruct ty.
+exact (forall (y : t), X y (f y) (app p (enc y))).
+exact (forall (y : t), X y (f y) (app p I)).
+exact (forall (y : (forall x : t, f1 x)) u, proc u -> IHty y u -> X y (f y) (app p u)).
Defined.
Lemma Pretty_step ty (tt:TT ty) (fty : ty -> Type) (ftt : forall x, TT (fty x)) f p :
(forall (y : ty) u, proc u ->
intFPretty u tt y ->
intFPretty (app p u) (ftt y) (f y)) <->
intFPretty p (TyAll tt ftt) f.
Proof.
induction tt;split; intros H'.
-intros ?. apply H'. apply proc_enc. now simpl.
-intros. specialize (H' y). cbn in H' . apply H'. cbn in *. intro ?. admit.
-intros ?. apply H'. split. cbv. reflexivity. eexists. reflexivity. now simpl.
-admit.
-intros y u pu Hu. apply H';try auto.
-admit.
Qed.
Lemma intFPretty_complete (p : Lvw.term) t (ty : TT t) (f : t) : internalizesF p ty f <-> intFPretty p ty f.
Proof.
revert p f. induction ty;tauto..|. split.
-intros. apply Pretty_step. intros. apply H. simpl in H0. apply H0;auto. now apply IHty.
-intros. destruct ty. cbn. intros. rewrite <- H. simpl. apply H0. cbn.
intros ?. destruct ty; hnf in H0.
-cbn in *. cbv in H0. intros ?. cbn. admit. admit.
cbn.
*)
(*
Inductive wellBehavedFun : forall X, term -> TT X -> Prop:=
wbBase s b (R:registered b) : wellBehavedFun s (TyB b)
| wbAll s t (ttt : TT t) (f : t -> Type) (ftt : forall x, TT (f x))
: (forall t, wellBehavedFun s (ftt t)) ->
wellBehavedFun (lam s) (TyAll ttt ftt).
*)
(*
Axiom rn : registered nat.
Axiom rbool : registered bool.
Axiom rdec : forall x, registered (dec x).
Axiom rsb : forall P Q, registered (sumbool P Q).
Definition eqDecType := TyAll (TyB nat) (fun x => TyAll (TyB nat) (fun y => TyB (dec (x=y)))).
Print dec.
Definition negDecType (P:Prop):= TyAll (TyB (dec P)) (fun _ => TyB (dec (~P))).
Definition nwt := TyAll (TyAll (TyB nat) (fun _ => TyB nat)) (fun f => TyB (dec (f 0 = 1))).
Check eqDecType.
Check negDecType.
Definition notWorking : forall f, dec (f 0 = 1).
intros. auto.
Defined.
Eval lazy dec in eq_dec nat.
Eval cbv dec in ltac:(let t' := type of nat_eq_dec in exact t').
Eval cbv dec in ltac:(let t' := type of not_dec in exact t').
Eval cbv dec in ltac:(let t' := type of notWorking in exact t').
Eval cbn in (internalizesF 1000 eqDecType nat_eq_dec).
Eval cbn in (internalizesF 1000 (negDecType True) (@not_dec True)).
Eval cbn in (internalizesF 1000 nwt notWorking).
*)
(*
Goal nat.
pose (H :=forall x, x \/ True).
assert ({F:Prop -> Prop | (H) = (forall x, F x)}).
eexists. reflexivity.
firstorder.
pattern x in H.
evar (x : False).
constructor.
Qed.
now repeat constructor; firstorder.
Qed.
*)
(*
Check (eq_dec nat).
Check (not_dec).
Goal True.
let x := constr:ltac:(toTT (eq_dec nat)) in pose x.
cbv in t.
constructor.
*)
(* Typeclass for internalization of terms *)
Class internalizedClass (X : Type) (ty : TT X) (x : X):=
{ internalizer : term ;
proc_t : proc internalizer ;
correct_t : internalizesF internalizer ty x (*;
wellBehaved : wellBehavedFun internalizer ty*)
}.
Definition int (X : Type) (ty : TT X) (x : X) (H : internalizedClass ty x) := internalizer.
Global Arguments int {X} {ty} x {H} : simpl never.
(*Notation "'int' t" := (internalize t) (at level 10).*)
Definition correct (X : Type) (ty : TT X) (x : X) (H : internalizedClass ty x) := correct_t.
Global Arguments correct {X} {ty} x {H} : simpl never.
Require Import bijection String.
(* Typeclass for registering types *)
Class registered (X : Type) := mk_registered
{
enc_f : X -> term ; (* the encoding function for X *)
proc_enc : forall x, proc (enc_f x) (* encodings need to be a procedure *)
}.
Class inj_reg (X:Type) (H:registered X) := mk_inj_reg
{
inj_enc : injective enc_f
}.
Arguments enc_f X {registered} _.
Definition enc (X : Type) (H:registered X) := enc_f X.
Global Arguments enc {X} {H} x : simpl never.
(*Notation "'enc' s" := (encode s) (at level 10).*)
(* Definition of the valid types for internalization *)
Inductive TT : Type -> Type :=
TyB t (H : registered t) : TT t
| TyElim (t:Type) : TT t
| TyAll t (ttt : TT t) (f : t -> Type) (ftt : forall x, TT (f x))
: TT (forall (x:t), f x).
Arguments TyB _ {_}.
Arguments TyAll {_} _ {_} _.
Notation "! X" := (TyB X) (at level 69).
(*Notation "X ~> Y" := (TyAll X (fun _ => Y)) (right associativity, at level 70).*)
Notation "X ~> Y" := (TyAll X (fun _ => Y)) (right associativity, at level 70).
(*
Ltac test x:= exact (x + 10).
Notation "!! X" := ( ltac:(test X ) ) (at level 100).
Compute (!! 10).
*)
(*Notation "\X ~> Y" := (TyAll X Y) (right associativity, at level 70).*)
(*
Axiom reg : registered nat.
Compute ( !nat ~> ! nat ~> ! nat).
*)
Definition internalizesF (p : Lvw.term) t (ty : TT t) (f : t) : Prop.
revert p. induction ty as [ t H p | t H p | t ty internalizesHyp R ftt internalizesF']; simpl in *;intros.
- exact (p >* enc f).
- exact (p >* I).
- exact (forall (y : t) u, proc u -> internalizesHyp y u -> internalizesF' y (f y) (app p u)).
Defined.
(*
destruct ty.
+exact (forall (y : t), X y (f y) (app p (enc y))).
+exact (forall (y : t), X y (f y) (app p I)).
+exact (forall (y : (forall x : t, f1 x)) u, proc u -> IHty y u -> X y (f y) (app p u)).*)
(*
Definition intFPretty (p : Lvw.term) t (ty : TT t) (f : t) : Prop.
revert p. induction ty; simpl in *;intros.
- exact (p>* enc f).
- exact (p>* I).
- destruct ty.
+exact (forall (y : t), X y (f y) (app p (enc y))).
+exact (forall (y : t), X y (f y) (app p I)).
+exact (forall (y : (forall x : t, f1 x)) u, proc u -> IHty y u -> X y (f y) (app p u)).
Defined.
Lemma Pretty_step ty (tt:TT ty) (fty : ty -> Type) (ftt : forall x, TT (fty x)) f p :
(forall (y : ty) u, proc u ->
intFPretty u tt y ->
intFPretty (app p u) (ftt y) (f y)) <->
intFPretty p (TyAll tt ftt) f.
Proof.
induction tt;split; intros H'.
-intros ?. apply H'. apply proc_enc. now simpl.
-intros. specialize (H' y). cbn in H' . apply H'. cbn in *. intro ?. admit.
-intros ?. apply H'. split. cbv. reflexivity. eexists. reflexivity. now simpl.
-admit.
-intros y u pu Hu. apply H';try auto.
-admit.
Qed.
Lemma intFPretty_complete (p : Lvw.term) t (ty : TT t) (f : t) : internalizesF p ty f <-> intFPretty p ty f.
Proof.
revert p f. induction ty;tauto..|. split.
-intros. apply Pretty_step. intros. apply H. simpl in H0. apply H0;auto. now apply IHty.
-intros. destruct ty. cbn. intros. rewrite <- H. simpl. apply H0. cbn.
intros ?. destruct ty; hnf in H0.
-cbn in *. cbv in H0. intros ?. cbn. admit. admit.
cbn.
*)
(*
Inductive wellBehavedFun : forall X, term -> TT X -> Prop:=
wbBase s b (R:registered b) : wellBehavedFun s (TyB b)
| wbAll s t (ttt : TT t) (f : t -> Type) (ftt : forall x, TT (f x))
: (forall t, wellBehavedFun s (ftt t)) ->
wellBehavedFun (lam s) (TyAll ttt ftt).
*)
(*
Axiom rn : registered nat.
Axiom rbool : registered bool.
Axiom rdec : forall x, registered (dec x).
Axiom rsb : forall P Q, registered (sumbool P Q).
Definition eqDecType := TyAll (TyB nat) (fun x => TyAll (TyB nat) (fun y => TyB (dec (x=y)))).
Print dec.
Definition negDecType (P:Prop):= TyAll (TyB (dec P)) (fun _ => TyB (dec (~P))).
Definition nwt := TyAll (TyAll (TyB nat) (fun _ => TyB nat)) (fun f => TyB (dec (f 0 = 1))).
Check eqDecType.
Check negDecType.
Definition notWorking : forall f, dec (f 0 = 1).
intros. auto.
Defined.
Eval lazy dec in eq_dec nat.
Eval cbv dec in ltac:(let t' := type of nat_eq_dec in exact t').
Eval cbv dec in ltac:(let t' := type of not_dec in exact t').
Eval cbv dec in ltac:(let t' := type of notWorking in exact t').
Eval cbn in (internalizesF 1000 eqDecType nat_eq_dec).
Eval cbn in (internalizesF 1000 (negDecType True) (@not_dec True)).
Eval cbn in (internalizesF 1000 nwt notWorking).
*)
(*
Goal nat.
pose (H :=forall x, x \/ True).
assert ({F:Prop -> Prop | (H) = (forall x, F x)}).
eexists. reflexivity.
firstorder.
pattern x in H.
evar (x : False).
constructor.
Qed.
now repeat constructor; firstorder.
Qed.
*)
(*
Check (eq_dec nat).
Check (not_dec).
Goal True.
let x := constr:ltac:(toTT (eq_dec nat)) in pose x.
cbv in t.
constructor.
*)
(* Typeclass for internalization of terms *)
Class internalizedClass (X : Type) (ty : TT X) (x : X):=
{ internalizer : term ;
proc_t : proc internalizer ;
correct_t : internalizesF internalizer ty x (*;
wellBehaved : wellBehavedFun internalizer ty*)
}.
Definition int (X : Type) (ty : TT X) (x : X) (H : internalizedClass ty x) := internalizer.
Global Arguments int {X} {ty} x {H} : simpl never.
(*Notation "'int' t" := (internalize t) (at level 10).*)
Definition correct (X : Type) (ty : TT X) (x : X) (H : internalizedClass ty x) := correct_t.
Global Arguments correct {X} {ty} x {H} : simpl never.