Reflection
Require Export Lvw LvwClos_Eval.
Open Scope LvwClos.
Inductive rTerm : Type :=
| rVar (x : nat) : rTerm
| rApp (s : rTerm) (t : rTerm) : rTerm
| rLam (s : rTerm)
| rConst (x : nat) : rTerm.
Coercion rApp : rTerm >-> Funclass.
Definition denoteTerm (phi : nat -> term) :rTerm->term :=
fix denoteTerm s :=
match s with
| rVar n => var n
| rApp s t=> (denoteTerm s) (denoteTerm t)
| rLam s => lam (denoteTerm s)
| rConst n => phi n
end.
Definition Proc phi := forall (n:nat) , proc (phi n).
Definition rClosed phi s:= Proc phi /\ closed (denoteTerm phi s).
Definition rReduce phi s t :=
denoteTerm phi s >* denoteTerm phi t.
Definition rEquiv phi s t :=
denoteTerm phi s == denoteTerm phi t.
Lemma rReduceIntro phi s t : Proc phi -> rClosed phi s -> rClosed phi t -> denoteTerm phi s >* denoteTerm phi t -> rReduce phi s t.
unfold rReduce;tauto.
Qed.
Lemma rEquivIntro phi s t : Proc phi -> rClosed phi s -> rClosed phi t -> denoteTerm phi s == denoteTerm phi t -> rEquiv phi s t.
unfold rReduce;tauto.
Qed.
Instance rEquiv_Equivalence phi: Equivalence (rEquiv phi).
Proof.
unfold rEquiv. constructor;repeat intro;intuition.
-now rewrite H.
Qed.
Instance rEquiv_rApp_proper phi:
Proper (rEquiv phi ==> rEquiv phi==> rEquiv phi ) rApp.
Proof.
intros ? ? R1 ? ? R2. unfold rEquiv in *. simpl. now rewrite R1,R2.
Qed.
Instance rReduce_PreOrder phi: PreOrder (rReduce phi).
Proof.
unfold rReduce. constructor;repeat intro;intuition.
-now rewrite H.
Qed.
Instance rReduce_rApp_proper phi:
Proper (rReduce phi ==> rReduce phi==> rReduce phi ) rApp.
Proof.
intros ? ? R1 ? ? R2. unfold rReduce in *. simpl. now rewrite R1,R2.
Qed.
Instance rReduce_rEquiv_subrelation phi: subrelation (rReduce phi) (rEquiv phi).
Proof.
intros s t R. unfold rReduce,rEquiv in *. now rewrite R.
Qed.
Inductive rComp : Type :=
| rCompVar (x:nat)
| rCompApp (s : rComp) (t : rComp) : rComp
| rCompClos (s : rTerm) (A : list rComp) : rComp.
Coercion rCompApp : rComp >-> Funclass.
Definition denoteComp (phi : nat -> term) :rComp -> Comp:=
fix denoteComp s :=
match s with
| rCompVar x => CompVar x
| rCompApp s t => (denoteComp s) (denoteComp t)
| rCompClos s A => CompClos (denoteTerm phi s) (map denoteComp A)
end.
Fixpoint rSubstList (s:rTerm) (x:nat) (A: list rTerm): rTerm :=
match s with
| rVar n => if decision ( n < x )then rVar n else nth (n-x) A (rVar n)
| rApp s t => (rSubstList s x A) (rSubstList t x A)
| rLam s => rLam (rSubstList s (S x) A)
| s => s
end.
Fixpoint rDeClos (s:rComp) : rTerm :=
match s with
| rCompVar x => rVar x
| rCompApp s t => (rDeClos s) (rDeClos t)
| rCompClos s A => rSubstList s 0 (map rDeClos A)
end.
Definition rComp_ind_deep'
(P : rComp -> Prop)
(Pl : list rComp -> Prop)
(IHVar : forall x : nat, P (rCompVar x))
(IHApp : forall s : rComp, P s -> forall t : rComp, P t -> P (s t))
(IHClos : forall (s : rTerm) (A : list rComp),
Pl A -> P (rCompClos s A))
(IHNil : Pl nil)
(IHCons : forall (a:rComp) (A : list rComp),
P a -> Pl A -> Pl (a::A))
(x:rComp) : P x :=
(fix f c : P c:=
match c with
| rCompVar x => IHVar x
| rCompApp s t => IHApp s (f s) t (f t)
| rCompClos s A => IHClos s A
((fix g A : Pl A :=
match A with
[] => IHNil
| a::A => IHCons a A (f a) (g A)
end) A)
end) x
.
Definition rComp_ind_deep
(P : rComp -> Prop)
(IHVar : forall x : nat, P (rCompVar x))
(IHApp : forall s : rComp, P s -> forall t : rComp, P t -> P (s t))
(IHClos : forall (s : rTerm) (A : list rComp),
(forall a, a el A -> P a) -> P (rCompClos s A)) : forall x, P x.
Proof.
apply rComp_ind_deep' with (Pl:=fun A => (forall a, a el A -> P a));auto.
-simpl. tauto.
-intros. inv H1;auto.
Qed.
Definition rValidComp phi s := Proc phi /\validComp (denoteComp phi s).
(*
Definition rEquivC phi s t := rReduce phi (rDeClos s) (rDeClos t).
Instance rEquivC'_per phi: PER (rEquivC' phi).
Proof.
unfold rEquivC',rValidComp. constructor;repeat intro;intuition.
-now rewrite H5.
Qed.
Instance rEquivC_rApp_proper phi:
Proper (rEquivC phi ==> rEquivC phi==> rEquivC phi ) rApp.
Proof.
unfold rEquivC, rEquivC', rValidComp. repeat intro. simpl in *. intuition.
-inv H4. inv H6. constructor;simpl in *;repeat intuition constructor.
-inv H8. inv H9. constructor;simpl in *;repeat intuition constructor.
-constructor. inv H5. inv H7. simpl. now rewrite H, H5.
Qed.
*)
(*
Lemma rEquivC'_iff s t phi : Proc phi -> rValidComp phi s -> rValidComp phi t -> (denoteTerm s == denoteComp phi t <-> rEquivC' phi s t).
Proof.
firstorder.
Qed.
*)
Lemma rSubstList_correct phi s x A: Proc phi -> denoteTerm phi (rSubstList s x A) =substList (denoteTerm phi s) x (map (denoteTerm phi) A).
Proof.
revert x. induction s; intros;simpl.
- decide (x < x0); decide (x0 > x); try omega ;intuition (try congruence);simpl.
now rewrite <-map_nth with (f:= denoteTerm phi).
-now rewrite IHs1,IHs2.
-now rewrite IHs.
-rewrite substList_closed. auto. apply H.
Qed.
Lemma map_ext' : forall (A B : Type) (f g : A -> B) (l:list A),
(forall a : A, a el l -> f a = g a) -> map f l = map g l.
Proof.
intros. induction l.
-reflexivity.
-simpl. rewrite H;auto. f_equal. apply IHl. intros. apply H. auto.
Qed.
Lemma denoteTerm_correct phi s: Proc phi -> deClos (denoteComp phi s) = denoteTerm phi (rDeClos s).
Proof.
intros pp. unfold denoteComp, rDeClos. pattern s. apply rComp_ind_deep;intros;simpl;try congruence.
-rewrite rSubstList_correct;auto. f_equal.
rewrite !map_map. now apply map_ext'.
Qed.
(*
Lemma starC_deClos s phi: Proc phi -> rEquiv phi (deClos s) (deCLos ()enoteComp phi (rCompClos (rDeClos s) ).
Proof.
intros pp. constructor. simpl. rewrite substList_nil. now rewrite denoteTerm_correct.
Qed.
*)
Definition rCompBeta s t :=
match s,t with
|rCompClos (rLam ls) A,rCompClos (rLam lt) B => Some (rCompClos ls (t::A))
|rCompClos (rLam ls) A,rCompClos (rConst x) B => Some (rCompClos ls (t::A))
|_,_ => None
end.
Fixpoint rCompSeval' n u : rComp*bool:=
match n with
S n =>
match u with
| rCompApp s t =>
match rCompSeval' n s,rCompSeval' n t with
(s',true),(t',true) =>
match rCompBeta s' t' with
Some u => rCompSeval' n u
| None => (s' t',false)
end
| (s',_),(t',_) => (s' t',false)
end
| rCompClos (rApp s t) A =>
rCompSeval' n (rCompApp (rCompClos s A) (rCompClos t A))
| rCompClos (rVar x) A => (nth x A (rCompVar x),true)
| rCompClos (rConst x) A => (u,true)
| rCompVar x => (u,true)
| rCompClos (rLam _) A => (u,true)
end
| 0 => (u,true)
end.
Definition rCompSeval n u : rComp:=
fst (rCompSeval' n u).
Lemma rCompBeta_sound phi (s t u: rComp) : Proc phi -> rCompBeta s t = Some u -> denoteComp phi (s t) >[]> denoteComp phi u.
Proof with simpl in *;try congruence;auto.
intros pp eq. destruct s... destruct s... destruct t... destruct s0; inv eq...
-constructor. apply pp.
Qed.
Lemma rCompSeval_sound n phi s: Proc phi -> denoteComp phi s >[]* denoteComp phi (rCompSeval n s).
Proof.
intros. unfold rCompSeval. revert s. induction n;intros s;simpl.
-reflexivity.
-destruct s;simpl.
+reflexivity.
+destruct (rCompSeval' n s1) eqn:eq1 . destruct (rCompSeval' n s2) eqn:eq2. destruct b;simpl. destruct b0;simpl.
destruct (rCompBeta r r0) eqn:eq3;simpl.
*rewrite <- IHn. eapply (rCompBeta_sound H) in eq3. rewrite <- eq3. simpl. apply rStar'_App_proper;rewrite IHn.
now rewrite eq1. now rewrite eq2.
*apply rStar'_App_proper;rewrite IHn. now rewrite eq1. now rewrite eq2.
*apply rStar'_App_proper;rewrite IHn. now rewrite eq1. now rewrite eq2.
*apply rStar'_App_proper;rewrite IHn. now rewrite eq1. now rewrite eq2.
+destruct s;simpl;try reflexivity.
*rewrite <-map_nth. now rewrite CStepVar.
*rewrite CStepApp. now rewrite <-!IHn.
Qed.
Lemma rCompBeta_rValidComp s t u phi : rValidComp phi s -> rValidComp phi t -> rCompBeta s t = Some u -> rValidComp phi u.
Proof with repeat (eauto || congruence || subst || simpl in * || intuition).
unfold rValidComp in *. intros vs vt eq. assert (pp:Proc phi)by (inv vs;auto). split;auto. unfold rCompBeta in eq. destruct s... destruct s... destruct t... destruct s0...
-inv eq. inv H0; inv H2. constructor... rewrite map_length in *. now inv H7.
-inv eq. inv H0; inv H2. constructor...
+destruct (pp x) as [_ H']. inv H'. now rewrite H0.
+rewrite map_length in *. now inv H7.
Qed.
Lemma rCompSeval_rValidComp n s phi: Proc phi -> rValidComp phi s -> rValidComp phi (rCompSeval n s).
Proof with repeat (simpl in * || eauto).
revert s. unfold rCompSeval. induction n; intros s pp H... assert (H':=H). inv H'. destruct s...
-destruct (rCompSeval' n s1) eqn:eq1. destruct (rCompSeval' n s2) eqn:eq2.
assert(v : rValidComp phi (fst (r,b))).
{ rewrite <-eq1. apply IHn;auto. now constructor;inv H1. }
assert(v0 : rValidComp phi (fst (r0,b0))).
{ rewrite <-eq2. apply IHn;auto. now constructor;inv H1. }
simpl in v,v0.
destruct b. destruct b0. destruct (rCompBeta r r0) eqn:eq.
+apply IHn... eapply rCompBeta_rValidComp with (s:=r) (t:=r0)...
+simpl. constructor;auto. constructor;[apply v|apply v0];auto.
+simpl. constructor;auto. constructor;[apply v|apply v0];auto.
+simpl. constructor;auto. constructor;[apply v|apply v0];auto.
-unfold rValidComp in *. inv H. destruct s;simpl...
+rewrite <- map_nth. split;auto. inv H1. apply H5. apply nth_In. now inv H7.
+apply IHn;auto. simpl in *. split;auto. inv H3. inv H7. repeat constructor...
Qed.
Lemma rClosed_valid s phi : Proc phi -> (rClosed phi s <-> rValidComp phi (rCompClos s [])).
Proof.
intros pp. unfold rClosed. unfold rValidComp. rewrite closed_dcl. split;intros H.
-repeat constructor;simpl;intuition;apply H0.
-inv H. inv H1. now tauto.
Qed.
Lemma expandDenote phi s: Proc phi -> denoteTerm phi s = deClos (denoteComp phi (rCompClos s [])).
intros pp. rewrite (denoteTerm_correct _ pp). simpl. rewrite rSubstList_correct;auto. simpl. now rewrite substList_nil.
Qed.
Lemma rDeClos_reduce phi s: Proc phi -> rValidComp phi s -> deClos (denoteComp phi s) = deClos (denoteComp phi (rCompClos (rDeClos s) [])).
Proof.
intros pp vc. simpl. rewrite <- denoteTerm_correct;auto. now rewrite substList_nil.
Qed.
Lemma rDeClos_rValidComp phi s: Proc phi -> rValidComp phi s -> rValidComp phi (rCompClos (rDeClos s) []).
Proof with repeat (eauto || congruence || subst || simpl in * || intuition).
intros pp [? H]. unfold rValidComp in *. split;try tauto. simpl. apply deClos_valComp in H. apply validComp_closed. now rewrite <- denoteTerm_correct.
Qed.
Lemma rStandardize n phi s : Proc phi -> rClosed phi s -> rReduce phi s (rDeClos (rCompSeval n (rCompClos s []))).
Proof.
intros pp cl. unfold rReduce. rewrite rClosed_valid in *;auto. assert (cl': rValidComp phi (rCompSeval n (rCompClos s []))).
-apply rCompSeval_rValidComp;auto.
- rewrite !expandDenote;auto. rewrite deClos_correct_star;[|auto|apply (rCompSeval_sound n);auto].
+now rewrite rDeClos_reduce.
+now inv cl.
Qed.
Lemma rStandardizeHypo n phi s t : rEquiv phi s t -> rClosed phi s -> rClosed phi t -> rEquiv phi (rDeClos (rCompSeval n (rCompClos s []))) (rDeClos (rCompSeval n (rCompClos t []))).
Proof.
intros eq cs ct. assert (pp:=cs). destruct pp as [PP _]. rewrite <- !rStandardize;auto.
Qed.
Lemma rStandardizeGoal n phi s t :
rEquiv phi (rDeClos (rCompSeval n (rCompClos s []))) (rDeClos (rCompSeval n (rCompClos t []))) -> rClosed phi s-> rClosed phi t ->rEquiv phi s t.
Proof.
intros eq cs ct.
assert (pp:Proc phi) by now inv cs.
rewrite (rStandardize n) with (s:=s);auto. rewrite (rStandardize n) with (s:=t);auto.
Qed.
Lemma rStandardizeGoalLeft' n phi s t :
rReduce phi (rDeClos (rCompSeval n (rCompClos s []))) t -> rClosed phi s ->rReduce phi s t.
Proof.
intros eq cs.
assert (pp:Proc phi) by now inv cs.
rewrite (rStandardize n) with (s:=s); auto.
Qed.
Lemma rStandardizeGoalLeft n phi s t :
(denoteTerm phi (rDeClos (rCompSeval n (rCompClos s [])))) >* t -> rClosed phi s-> (denoteTerm phi s) >* t.
Proof.
intros eq cs.
assert (pp:Proc phi) by now inv cs.
assert (R:=rStandardize n pp cs). unfold rReduce in R. now rewrite R.
Qed.
Lemma rStandardizeUse n phi s:
Proc phi -> rClosed phi s -> denoteTerm phi s>* denoteTerm phi (rDeClos (rCompSeval n (rCompClos s []))).
Proof.
intros pp cs.
refine (_:rReduce _ _ _).
now apply rStandardize.
Qed.
Fixpoint rClosed_decb' n u : bool:=
match u with
| rApp s t => andb (rClosed_decb' n s) (rClosed_decb' n t)
| rVar x => negb (leb n x)
| rConst x => true
| rLam s =>rClosed_decb' (S n) s
end.
Lemma rClosed_decb'_correct s phi n: Proc phi -> rClosed_decb' n s = true -> dclosed n (denoteTerm phi s).
Proof.
intros pp. revert n. induction s;intros n eq;simpl in *.
-rewrite Bool.negb_true_iff in eq. apply leb_complete_conv in eq. now constructor.
-rewrite Bool.andb_true_iff in eq. constructor; intuition.
-constructor. auto.
-apply dclosed_ge with (k:=0);[|omega]. rewrite <- closed_dcl. apply pp.
Qed.
Definition rClosed_decb s:= rClosed_decb' 0 s.
Lemma rClosed_decb_correct phi s : Proc phi -> rClosed_decb s = true -> rClosed phi s.
Proof.
intros. hnf;split;[auto|]. rewrite closed_dcl. apply rClosed_decb'_correct;auto.
Qed.
(* Facts about denote *)
Definition liftPhi Vars n:=nth n Vars I.
Arguments liftPhi Vars n/.
Lemma liftPhi_correct Vars: (forall s, s el Vars -> proc s) -> Proc (liftPhi Vars).
Proof.
intros H n. unfold liftPhi. destruct (nth_in_or_default n Vars I) as [?|eq].
-now apply H.
-rewrite eq. cbv. split. auto. eexists. eauto.
Qed.
Fixpoint benchTerm x : rTerm :=
match x with
0 => (rLam (rVar 0))
| S x => (rLam (benchTerm x)) (rLam (rVar 0))
end.
Close Scope LvwClos.
Open Scope LvwClos.
Inductive rTerm : Type :=
| rVar (x : nat) : rTerm
| rApp (s : rTerm) (t : rTerm) : rTerm
| rLam (s : rTerm)
| rConst (x : nat) : rTerm.
Coercion rApp : rTerm >-> Funclass.
Definition denoteTerm (phi : nat -> term) :rTerm->term :=
fix denoteTerm s :=
match s with
| rVar n => var n
| rApp s t=> (denoteTerm s) (denoteTerm t)
| rLam s => lam (denoteTerm s)
| rConst n => phi n
end.
Definition Proc phi := forall (n:nat) , proc (phi n).
Definition rClosed phi s:= Proc phi /\ closed (denoteTerm phi s).
Definition rReduce phi s t :=
denoteTerm phi s >* denoteTerm phi t.
Definition rEquiv phi s t :=
denoteTerm phi s == denoteTerm phi t.
Lemma rReduceIntro phi s t : Proc phi -> rClosed phi s -> rClosed phi t -> denoteTerm phi s >* denoteTerm phi t -> rReduce phi s t.
unfold rReduce;tauto.
Qed.
Lemma rEquivIntro phi s t : Proc phi -> rClosed phi s -> rClosed phi t -> denoteTerm phi s == denoteTerm phi t -> rEquiv phi s t.
unfold rReduce;tauto.
Qed.
Instance rEquiv_Equivalence phi: Equivalence (rEquiv phi).
Proof.
unfold rEquiv. constructor;repeat intro;intuition.
-now rewrite H.
Qed.
Instance rEquiv_rApp_proper phi:
Proper (rEquiv phi ==> rEquiv phi==> rEquiv phi ) rApp.
Proof.
intros ? ? R1 ? ? R2. unfold rEquiv in *. simpl. now rewrite R1,R2.
Qed.
Instance rReduce_PreOrder phi: PreOrder (rReduce phi).
Proof.
unfold rReduce. constructor;repeat intro;intuition.
-now rewrite H.
Qed.
Instance rReduce_rApp_proper phi:
Proper (rReduce phi ==> rReduce phi==> rReduce phi ) rApp.
Proof.
intros ? ? R1 ? ? R2. unfold rReduce in *. simpl. now rewrite R1,R2.
Qed.
Instance rReduce_rEquiv_subrelation phi: subrelation (rReduce phi) (rEquiv phi).
Proof.
intros s t R. unfold rReduce,rEquiv in *. now rewrite R.
Qed.
Inductive rComp : Type :=
| rCompVar (x:nat)
| rCompApp (s : rComp) (t : rComp) : rComp
| rCompClos (s : rTerm) (A : list rComp) : rComp.
Coercion rCompApp : rComp >-> Funclass.
Definition denoteComp (phi : nat -> term) :rComp -> Comp:=
fix denoteComp s :=
match s with
| rCompVar x => CompVar x
| rCompApp s t => (denoteComp s) (denoteComp t)
| rCompClos s A => CompClos (denoteTerm phi s) (map denoteComp A)
end.
Fixpoint rSubstList (s:rTerm) (x:nat) (A: list rTerm): rTerm :=
match s with
| rVar n => if decision ( n < x )then rVar n else nth (n-x) A (rVar n)
| rApp s t => (rSubstList s x A) (rSubstList t x A)
| rLam s => rLam (rSubstList s (S x) A)
| s => s
end.
Fixpoint rDeClos (s:rComp) : rTerm :=
match s with
| rCompVar x => rVar x
| rCompApp s t => (rDeClos s) (rDeClos t)
| rCompClos s A => rSubstList s 0 (map rDeClos A)
end.
Definition rComp_ind_deep'
(P : rComp -> Prop)
(Pl : list rComp -> Prop)
(IHVar : forall x : nat, P (rCompVar x))
(IHApp : forall s : rComp, P s -> forall t : rComp, P t -> P (s t))
(IHClos : forall (s : rTerm) (A : list rComp),
Pl A -> P (rCompClos s A))
(IHNil : Pl nil)
(IHCons : forall (a:rComp) (A : list rComp),
P a -> Pl A -> Pl (a::A))
(x:rComp) : P x :=
(fix f c : P c:=
match c with
| rCompVar x => IHVar x
| rCompApp s t => IHApp s (f s) t (f t)
| rCompClos s A => IHClos s A
((fix g A : Pl A :=
match A with
[] => IHNil
| a::A => IHCons a A (f a) (g A)
end) A)
end) x
.
Definition rComp_ind_deep
(P : rComp -> Prop)
(IHVar : forall x : nat, P (rCompVar x))
(IHApp : forall s : rComp, P s -> forall t : rComp, P t -> P (s t))
(IHClos : forall (s : rTerm) (A : list rComp),
(forall a, a el A -> P a) -> P (rCompClos s A)) : forall x, P x.
Proof.
apply rComp_ind_deep' with (Pl:=fun A => (forall a, a el A -> P a));auto.
-simpl. tauto.
-intros. inv H1;auto.
Qed.
Definition rValidComp phi s := Proc phi /\validComp (denoteComp phi s).
(*
Definition rEquivC phi s t := rReduce phi (rDeClos s) (rDeClos t).
Instance rEquivC'_per phi: PER (rEquivC' phi).
Proof.
unfold rEquivC',rValidComp. constructor;repeat intro;intuition.
-now rewrite H5.
Qed.
Instance rEquivC_rApp_proper phi:
Proper (rEquivC phi ==> rEquivC phi==> rEquivC phi ) rApp.
Proof.
unfold rEquivC, rEquivC', rValidComp. repeat intro. simpl in *. intuition.
-inv H4. inv H6. constructor;simpl in *;repeat intuition constructor.
-inv H8. inv H9. constructor;simpl in *;repeat intuition constructor.
-constructor. inv H5. inv H7. simpl. now rewrite H, H5.
Qed.
*)
(*
Lemma rEquivC'_iff s t phi : Proc phi -> rValidComp phi s -> rValidComp phi t -> (denoteTerm s == denoteComp phi t <-> rEquivC' phi s t).
Proof.
firstorder.
Qed.
*)
Lemma rSubstList_correct phi s x A: Proc phi -> denoteTerm phi (rSubstList s x A) =substList (denoteTerm phi s) x (map (denoteTerm phi) A).
Proof.
revert x. induction s; intros;simpl.
- decide (x < x0); decide (x0 > x); try omega ;intuition (try congruence);simpl.
now rewrite <-map_nth with (f:= denoteTerm phi).
-now rewrite IHs1,IHs2.
-now rewrite IHs.
-rewrite substList_closed. auto. apply H.
Qed.
Lemma map_ext' : forall (A B : Type) (f g : A -> B) (l:list A),
(forall a : A, a el l -> f a = g a) -> map f l = map g l.
Proof.
intros. induction l.
-reflexivity.
-simpl. rewrite H;auto. f_equal. apply IHl. intros. apply H. auto.
Qed.
Lemma denoteTerm_correct phi s: Proc phi -> deClos (denoteComp phi s) = denoteTerm phi (rDeClos s).
Proof.
intros pp. unfold denoteComp, rDeClos. pattern s. apply rComp_ind_deep;intros;simpl;try congruence.
-rewrite rSubstList_correct;auto. f_equal.
rewrite !map_map. now apply map_ext'.
Qed.
(*
Lemma starC_deClos s phi: Proc phi -> rEquiv phi (deClos s) (deCLos ()enoteComp phi (rCompClos (rDeClos s) ).
Proof.
intros pp. constructor. simpl. rewrite substList_nil. now rewrite denoteTerm_correct.
Qed.
*)
Definition rCompBeta s t :=
match s,t with
|rCompClos (rLam ls) A,rCompClos (rLam lt) B => Some (rCompClos ls (t::A))
|rCompClos (rLam ls) A,rCompClos (rConst x) B => Some (rCompClos ls (t::A))
|_,_ => None
end.
Fixpoint rCompSeval' n u : rComp*bool:=
match n with
S n =>
match u with
| rCompApp s t =>
match rCompSeval' n s,rCompSeval' n t with
(s',true),(t',true) =>
match rCompBeta s' t' with
Some u => rCompSeval' n u
| None => (s' t',false)
end
| (s',_),(t',_) => (s' t',false)
end
| rCompClos (rApp s t) A =>
rCompSeval' n (rCompApp (rCompClos s A) (rCompClos t A))
| rCompClos (rVar x) A => (nth x A (rCompVar x),true)
| rCompClos (rConst x) A => (u,true)
| rCompVar x => (u,true)
| rCompClos (rLam _) A => (u,true)
end
| 0 => (u,true)
end.
Definition rCompSeval n u : rComp:=
fst (rCompSeval' n u).
Lemma rCompBeta_sound phi (s t u: rComp) : Proc phi -> rCompBeta s t = Some u -> denoteComp phi (s t) >[]> denoteComp phi u.
Proof with simpl in *;try congruence;auto.
intros pp eq. destruct s... destruct s... destruct t... destruct s0; inv eq...
-constructor. apply pp.
Qed.
Lemma rCompSeval_sound n phi s: Proc phi -> denoteComp phi s >[]* denoteComp phi (rCompSeval n s).
Proof.
intros. unfold rCompSeval. revert s. induction n;intros s;simpl.
-reflexivity.
-destruct s;simpl.
+reflexivity.
+destruct (rCompSeval' n s1) eqn:eq1 . destruct (rCompSeval' n s2) eqn:eq2. destruct b;simpl. destruct b0;simpl.
destruct (rCompBeta r r0) eqn:eq3;simpl.
*rewrite <- IHn. eapply (rCompBeta_sound H) in eq3. rewrite <- eq3. simpl. apply rStar'_App_proper;rewrite IHn.
now rewrite eq1. now rewrite eq2.
*apply rStar'_App_proper;rewrite IHn. now rewrite eq1. now rewrite eq2.
*apply rStar'_App_proper;rewrite IHn. now rewrite eq1. now rewrite eq2.
*apply rStar'_App_proper;rewrite IHn. now rewrite eq1. now rewrite eq2.
+destruct s;simpl;try reflexivity.
*rewrite <-map_nth. now rewrite CStepVar.
*rewrite CStepApp. now rewrite <-!IHn.
Qed.
Lemma rCompBeta_rValidComp s t u phi : rValidComp phi s -> rValidComp phi t -> rCompBeta s t = Some u -> rValidComp phi u.
Proof with repeat (eauto || congruence || subst || simpl in * || intuition).
unfold rValidComp in *. intros vs vt eq. assert (pp:Proc phi)by (inv vs;auto). split;auto. unfold rCompBeta in eq. destruct s... destruct s... destruct t... destruct s0...
-inv eq. inv H0; inv H2. constructor... rewrite map_length in *. now inv H7.
-inv eq. inv H0; inv H2. constructor...
+destruct (pp x) as [_ H']. inv H'. now rewrite H0.
+rewrite map_length in *. now inv H7.
Qed.
Lemma rCompSeval_rValidComp n s phi: Proc phi -> rValidComp phi s -> rValidComp phi (rCompSeval n s).
Proof with repeat (simpl in * || eauto).
revert s. unfold rCompSeval. induction n; intros s pp H... assert (H':=H). inv H'. destruct s...
-destruct (rCompSeval' n s1) eqn:eq1. destruct (rCompSeval' n s2) eqn:eq2.
assert(v : rValidComp phi (fst (r,b))).
{ rewrite <-eq1. apply IHn;auto. now constructor;inv H1. }
assert(v0 : rValidComp phi (fst (r0,b0))).
{ rewrite <-eq2. apply IHn;auto. now constructor;inv H1. }
simpl in v,v0.
destruct b. destruct b0. destruct (rCompBeta r r0) eqn:eq.
+apply IHn... eapply rCompBeta_rValidComp with (s:=r) (t:=r0)...
+simpl. constructor;auto. constructor;[apply v|apply v0];auto.
+simpl. constructor;auto. constructor;[apply v|apply v0];auto.
+simpl. constructor;auto. constructor;[apply v|apply v0];auto.
-unfold rValidComp in *. inv H. destruct s;simpl...
+rewrite <- map_nth. split;auto. inv H1. apply H5. apply nth_In. now inv H7.
+apply IHn;auto. simpl in *. split;auto. inv H3. inv H7. repeat constructor...
Qed.
Lemma rClosed_valid s phi : Proc phi -> (rClosed phi s <-> rValidComp phi (rCompClos s [])).
Proof.
intros pp. unfold rClosed. unfold rValidComp. rewrite closed_dcl. split;intros H.
-repeat constructor;simpl;intuition;apply H0.
-inv H. inv H1. now tauto.
Qed.
Lemma expandDenote phi s: Proc phi -> denoteTerm phi s = deClos (denoteComp phi (rCompClos s [])).
intros pp. rewrite (denoteTerm_correct _ pp). simpl. rewrite rSubstList_correct;auto. simpl. now rewrite substList_nil.
Qed.
Lemma rDeClos_reduce phi s: Proc phi -> rValidComp phi s -> deClos (denoteComp phi s) = deClos (denoteComp phi (rCompClos (rDeClos s) [])).
Proof.
intros pp vc. simpl. rewrite <- denoteTerm_correct;auto. now rewrite substList_nil.
Qed.
Lemma rDeClos_rValidComp phi s: Proc phi -> rValidComp phi s -> rValidComp phi (rCompClos (rDeClos s) []).
Proof with repeat (eauto || congruence || subst || simpl in * || intuition).
intros pp [? H]. unfold rValidComp in *. split;try tauto. simpl. apply deClos_valComp in H. apply validComp_closed. now rewrite <- denoteTerm_correct.
Qed.
Lemma rStandardize n phi s : Proc phi -> rClosed phi s -> rReduce phi s (rDeClos (rCompSeval n (rCompClos s []))).
Proof.
intros pp cl. unfold rReduce. rewrite rClosed_valid in *;auto. assert (cl': rValidComp phi (rCompSeval n (rCompClos s []))).
-apply rCompSeval_rValidComp;auto.
- rewrite !expandDenote;auto. rewrite deClos_correct_star;[|auto|apply (rCompSeval_sound n);auto].
+now rewrite rDeClos_reduce.
+now inv cl.
Qed.
Lemma rStandardizeHypo n phi s t : rEquiv phi s t -> rClosed phi s -> rClosed phi t -> rEquiv phi (rDeClos (rCompSeval n (rCompClos s []))) (rDeClos (rCompSeval n (rCompClos t []))).
Proof.
intros eq cs ct. assert (pp:=cs). destruct pp as [PP _]. rewrite <- !rStandardize;auto.
Qed.
Lemma rStandardizeGoal n phi s t :
rEquiv phi (rDeClos (rCompSeval n (rCompClos s []))) (rDeClos (rCompSeval n (rCompClos t []))) -> rClosed phi s-> rClosed phi t ->rEquiv phi s t.
Proof.
intros eq cs ct.
assert (pp:Proc phi) by now inv cs.
rewrite (rStandardize n) with (s:=s);auto. rewrite (rStandardize n) with (s:=t);auto.
Qed.
Lemma rStandardizeGoalLeft' n phi s t :
rReduce phi (rDeClos (rCompSeval n (rCompClos s []))) t -> rClosed phi s ->rReduce phi s t.
Proof.
intros eq cs.
assert (pp:Proc phi) by now inv cs.
rewrite (rStandardize n) with (s:=s); auto.
Qed.
Lemma rStandardizeGoalLeft n phi s t :
(denoteTerm phi (rDeClos (rCompSeval n (rCompClos s [])))) >* t -> rClosed phi s-> (denoteTerm phi s) >* t.
Proof.
intros eq cs.
assert (pp:Proc phi) by now inv cs.
assert (R:=rStandardize n pp cs). unfold rReduce in R. now rewrite R.
Qed.
Lemma rStandardizeUse n phi s:
Proc phi -> rClosed phi s -> denoteTerm phi s>* denoteTerm phi (rDeClos (rCompSeval n (rCompClos s []))).
Proof.
intros pp cs.
refine (_:rReduce _ _ _).
now apply rStandardize.
Qed.
Fixpoint rClosed_decb' n u : bool:=
match u with
| rApp s t => andb (rClosed_decb' n s) (rClosed_decb' n t)
| rVar x => negb (leb n x)
| rConst x => true
| rLam s =>rClosed_decb' (S n) s
end.
Lemma rClosed_decb'_correct s phi n: Proc phi -> rClosed_decb' n s = true -> dclosed n (denoteTerm phi s).
Proof.
intros pp. revert n. induction s;intros n eq;simpl in *.
-rewrite Bool.negb_true_iff in eq. apply leb_complete_conv in eq. now constructor.
-rewrite Bool.andb_true_iff in eq. constructor; intuition.
-constructor. auto.
-apply dclosed_ge with (k:=0);[|omega]. rewrite <- closed_dcl. apply pp.
Qed.
Definition rClosed_decb s:= rClosed_decb' 0 s.
Lemma rClosed_decb_correct phi s : Proc phi -> rClosed_decb s = true -> rClosed phi s.
Proof.
intros. hnf;split;[auto|]. rewrite closed_dcl. apply rClosed_decb'_correct;auto.
Qed.
(* Facts about denote *)
Definition liftPhi Vars n:=nth n Vars I.
Arguments liftPhi Vars n/.
Lemma liftPhi_correct Vars: (forall s, s el Vars -> proc s) -> Proc (liftPhi Vars).
Proof.
intros H n. unfold liftPhi. destruct (nth_in_or_default n Vars I) as [?|eq].
-now apply H.
-rewrite eq. cbv. split. auto. eexists. eauto.
Qed.
Fixpoint benchTerm x : rTerm :=
match x with
0 => (rLam (rVar 0))
| S x => (rLam (benchTerm x)) (rLam (rVar 0))
end.
Close Scope LvwClos.