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.