SumBool
Require Export LProp LBool.
Require Import internalize_tac.
Definition sumbool_enc (X: Prop) (Y:Prop) (x : sumbool X Y) :=
match x with
left A => lam (lam (1 I))
| right B => lam (lam (0 I))
end.
Instance sumbool_term (X : Prop) (Y : Prop) : registered (sumbool X Y).
Proof.
register (@sumbool_enc X Y).
Defined.
Instance term_True_dec: internalized (True_dec).
Proof.
internalizeC (enc (@left True (~True) Logic.I)).
Defined.
Instance term_False_dec: internalized (False_dec).
Proof.
internalizeC (enc (@right False (~False) id)).
Defined.
Instance term_left (X Y:Prop) : internalized (@left X Y).
Proof.
internalizeC (lam (lam (lam (1 2)))).
Defined.
Instance term_right (X Y:Prop) : internalized (@right X Y).
Proof.
internalizeC (lam (lam (lam (0 2)))).
Defined.
(*
Lemma left_spec (X Y Z1 Z2 : Prop) (A : X) (B : Y) : enc (@left X Z1 A ) = enc (@left Y Z2 B).
Proof.
reflexivity.
Qed.
Lemma right_spec (X Y Z1 Z2 : Prop) (A : X) (B : Y) : enc (@right Z1 X A ) >* enc (@right Z2 Y B).
Proof.
reflexivity.
Qed.
*)
Lemma sumbool_enc_correct (X Y : Prop) (b: sumbool X Y) (s t:term): proc s -> proc t -> enc b s t >* if b then s I else t I.
Proof.
destruct b;fcrush.
Qed.
Hint Extern 0 (app (app (@enc (@sumbool _ _) _ _) _) _ >* _) => apply sumbool_enc_correct;value : LCor.
Definition to_sumbool (b:bool) := if b then left Logic.I else right Logic.I.
Definition from_sumbool X Y (b:sumbool X Y) := if b then true else false.
(*Arguments from_sumbool : clear implicits.*)
Instance term_to_sumbool: internalized to_sumbool.
Proof.
internalize. crush. destruct y;crush.
Defined.
(*
Instance term_from_sumbool' X Y: internalized (@from_sumbool X Y).
Proof.
internalize. destruct y; crush.
Defined.
*)
Instance term_from_sumbool: internalized (from_sumbool).
Proof.
internalize. destruct y;crush.
Defined.
(*needed to cast any sumbool to boolean without caring about the sumbool*)
Lemma from_sumbool_elim p q R S (b : @sumbool R S): proc p -> proc q -> int (@from_sumbool) p q (enc b) >* enc (if b then true else false).
Proof.
destruct b; fcrush.
Qed.
Lemma reflect_dec (P:Prop) (dec_P : dec P) b :
Bool.reflect P b -> enc (to_sumbool b) >* enc (dec_P).
Proof.
destruct 1; destruct dec_P;try contradiction;try reflexivity.
Qed.
Definition reflection_2
(X Y : Type) (RX : registered X) (RY : registered Y)
(P : X -> Y -> Prop)
(f : X -> Y -> bool)
{int_f : internalizedClass (!X ~> !Y ~> !bool) f} :
(forall x y, Bool.reflect (P x y) (f x y)) ->
forall (d : forall x y, dec (P x y)), internalized d.
Proof.
intros ref P_dec. pose (s := fun x => fun y => to_sumbool (f x y)).
internalizeWith s.
destruct (ref y y0), (P_dec y y0); try congruence; crush.
Defined.
Definition reflection_1
(X : Type) (_ : registered X)
(P : X -> Prop) f
{int_f : internalizedClass (!X ~> !bool) f} :
(forall x, Bool.reflect (P x) (f x)) ->
forall (d : forall x, dec (P x)), internalized d.
Proof.
intros ref P_dec. pose (s := fun x => to_sumbool (f x)).
internalizeWith s.
destruct (ref y), (P_dec y); try congruence; crush.
Defined.
Instance term_impl_dec: internalized @impl_dec.
Proof.
pose (f (P Q : Prop) (p: dec P) (q: dec Q) := to_sumbool (orb (negb (from_sumbool p)) (from_sumbool q))).
internalizeWith f. destruct y,y0;crush.
Defined.
Instance term_not_dec: internalized (not_dec).
Proof.
internalize.
Qed.
(*
Instance reflection_0
(X Y : Type) (P : Prop) b
(int_b : internalized b) :
registered P ->
(Bool.reflect P b) ->
forall d : dec P, internalized d.
Proof.
intros iii ref P_dec. pose (s := to_sumbool b).
econstructor. instantiate (1 := enc (to_sumbool b)).
value. instantiate (1 := TyB _). simpl.
destruct P_dec, ref; try congruence; simpl; eauto using left_spec, right_spec.
Defined.
*)
(* Once you have a boolean decider reflecting the Coq-decider, you are done *)
(* for nat *)
(*
Local Instance nat_eq_dec_term : internalized nat_eq_dec.
Proof.
apply reflection_2 with (f:= eqb).
exact _.
eapply Nat.eqb_spec.
Defined.
*)
(* for bool *)
(*
Lemma eqb_spec : forall x y : bool, Bool.reflect (x = y) (Bool.eqb x y).
Proof.
intros x y.
destruct (Bool.eqb x y) eqn:E.
- econstructor. now rewrite Bool.eqb_true_iff in E.
- econstructor. now rewrite Bool.eqb_false_iff in E.
Defined.
Local Instance eqb_term : internalized Bool.eqb.
Proof.
internalize. intros ; crush.
Defined.
Local Instance bool_eq_dec_term : internalized bool_eq_dec.
Proof.
eapply reflection_2 with (f := Bool.eqb).
exact _.
eapply eqb_spec.
Defined.
*)
Require Import internalize_tac.
Definition sumbool_enc (X: Prop) (Y:Prop) (x : sumbool X Y) :=
match x with
left A => lam (lam (1 I))
| right B => lam (lam (0 I))
end.
Instance sumbool_term (X : Prop) (Y : Prop) : registered (sumbool X Y).
Proof.
register (@sumbool_enc X Y).
Defined.
Instance term_True_dec: internalized (True_dec).
Proof.
internalizeC (enc (@left True (~True) Logic.I)).
Defined.
Instance term_False_dec: internalized (False_dec).
Proof.
internalizeC (enc (@right False (~False) id)).
Defined.
Instance term_left (X Y:Prop) : internalized (@left X Y).
Proof.
internalizeC (lam (lam (lam (1 2)))).
Defined.
Instance term_right (X Y:Prop) : internalized (@right X Y).
Proof.
internalizeC (lam (lam (lam (0 2)))).
Defined.
(*
Lemma left_spec (X Y Z1 Z2 : Prop) (A : X) (B : Y) : enc (@left X Z1 A ) = enc (@left Y Z2 B).
Proof.
reflexivity.
Qed.
Lemma right_spec (X Y Z1 Z2 : Prop) (A : X) (B : Y) : enc (@right Z1 X A ) >* enc (@right Z2 Y B).
Proof.
reflexivity.
Qed.
*)
Lemma sumbool_enc_correct (X Y : Prop) (b: sumbool X Y) (s t:term): proc s -> proc t -> enc b s t >* if b then s I else t I.
Proof.
destruct b;fcrush.
Qed.
Hint Extern 0 (app (app (@enc (@sumbool _ _) _ _) _) _ >* _) => apply sumbool_enc_correct;value : LCor.
Definition to_sumbool (b:bool) := if b then left Logic.I else right Logic.I.
Definition from_sumbool X Y (b:sumbool X Y) := if b then true else false.
(*Arguments from_sumbool : clear implicits.*)
Instance term_to_sumbool: internalized to_sumbool.
Proof.
internalize. crush. destruct y;crush.
Defined.
(*
Instance term_from_sumbool' X Y: internalized (@from_sumbool X Y).
Proof.
internalize. destruct y; crush.
Defined.
*)
Instance term_from_sumbool: internalized (from_sumbool).
Proof.
internalize. destruct y;crush.
Defined.
(*needed to cast any sumbool to boolean without caring about the sumbool*)
Lemma from_sumbool_elim p q R S (b : @sumbool R S): proc p -> proc q -> int (@from_sumbool) p q (enc b) >* enc (if b then true else false).
Proof.
destruct b; fcrush.
Qed.
Lemma reflect_dec (P:Prop) (dec_P : dec P) b :
Bool.reflect P b -> enc (to_sumbool b) >* enc (dec_P).
Proof.
destruct 1; destruct dec_P;try contradiction;try reflexivity.
Qed.
Definition reflection_2
(X Y : Type) (RX : registered X) (RY : registered Y)
(P : X -> Y -> Prop)
(f : X -> Y -> bool)
{int_f : internalizedClass (!X ~> !Y ~> !bool) f} :
(forall x y, Bool.reflect (P x y) (f x y)) ->
forall (d : forall x y, dec (P x y)), internalized d.
Proof.
intros ref P_dec. pose (s := fun x => fun y => to_sumbool (f x y)).
internalizeWith s.
destruct (ref y y0), (P_dec y y0); try congruence; crush.
Defined.
Definition reflection_1
(X : Type) (_ : registered X)
(P : X -> Prop) f
{int_f : internalizedClass (!X ~> !bool) f} :
(forall x, Bool.reflect (P x) (f x)) ->
forall (d : forall x, dec (P x)), internalized d.
Proof.
intros ref P_dec. pose (s := fun x => to_sumbool (f x)).
internalizeWith s.
destruct (ref y), (P_dec y); try congruence; crush.
Defined.
Instance term_impl_dec: internalized @impl_dec.
Proof.
pose (f (P Q : Prop) (p: dec P) (q: dec Q) := to_sumbool (orb (negb (from_sumbool p)) (from_sumbool q))).
internalizeWith f. destruct y,y0;crush.
Defined.
Instance term_not_dec: internalized (not_dec).
Proof.
internalize.
Qed.
(*
Instance reflection_0
(X Y : Type) (P : Prop) b
(int_b : internalized b) :
registered P ->
(Bool.reflect P b) ->
forall d : dec P, internalized d.
Proof.
intros iii ref P_dec. pose (s := to_sumbool b).
econstructor. instantiate (1 := enc (to_sumbool b)).
value. instantiate (1 := TyB _). simpl.
destruct P_dec, ref; try congruence; simpl; eauto using left_spec, right_spec.
Defined.
*)
(* Once you have a boolean decider reflecting the Coq-decider, you are done *)
(* for nat *)
(*
Local Instance nat_eq_dec_term : internalized nat_eq_dec.
Proof.
apply reflection_2 with (f:= eqb).
exact _.
eapply Nat.eqb_spec.
Defined.
*)
(* for bool *)
(*
Lemma eqb_spec : forall x y : bool, Bool.reflect (x = y) (Bool.eqb x y).
Proof.
intros x y.
destruct (Bool.eqb x y) eqn:E.
- econstructor. now rewrite Bool.eqb_true_iff in E.
- econstructor. now rewrite Bool.eqb_false_iff in E.
Defined.
Local Instance eqb_term : internalized Bool.eqb.
Proof.
internalize. intros ; crush.
Defined.
Local Instance bool_eq_dec_term : internalized bool_eq_dec.
Proof.
eapply reflection_2 with (f := Bool.eqb).
exact _.
eapply eqb_spec.
Defined.
*)