(* Exercice 2 *)

Require Import ZArith.

Open Scope Z_scope.

Inductive expr := Econst (n: Z) | Esub (e1 e2: expr).
Definition prog := expr.
Definition val := Z.

(* L'evaluateur en style direct *)

Fixpoint eval_0 (e: expr) : val :=
  match e with
  | Econst n => n
  | Esub e1 e2 => eval_0 e1 - eval_0 e2
  end.

Definition interp_0 (p: prog) : val := eval_0 p.

(* Small-step *)

Definition contracte (e: expr) : option expr :=
  match e with
  | Esub (Econst n1) (Econst n2) => Some (Econst (n1 - n2))
  | _ => None
  end.

Lemma contracte_sound:
  forall e e', contracte e = Some e' -> eval_0 e' = eval_0 e.
Proof with (try discriminate).
  unfold contracte; intros e e' EQ; destruct e...
  destruct e1... destruct e2... inversion EQ. auto.
Qed.

Inductive is_redex: expr -> Prop :=
  | is_redex_1: forall n1 n2, is_redex (Esub (Econst n1) (Econst n2)).

(* Contextes et zippers *)

Inductive context : Type :=
  | Chole 
  | Csubl (c: context) (e: expr)
  | Csubr (n: val) (c: context).

Fixpoint remplir (c: context) (e: expr) :=
  match c with
  | Chole => e
  | Csubl c1 e2 => Esub (remplir c1 e) e2
  | Csubr n1 c2 => Esub (Econst n1) (remplir c2 e)
  end.

Inductive zipper : Type :=
  | Ztop
  | Zsubl (z: zipper) (e: expr)
  | Zsubr (n: val) (z: zipper).

Fixpoint recompose (z: zipper) (e: expr) : expr :=
  match z with
  | Ztop => e
  | Zsubl z1 e2 => recompose z1 (Esub e e2)
  | Zsubr n1 z2 => recompose z2 (Esub (Econst n1) e)
  end.

(* Decomposition avec contextes *)

Fixpoint decomp_context (e: expr) : val + context * expr :=
  match e with
  | Econst n => inl n
  | Esub e1 e2 =>
      match decomp_context e1 with
      | inr (c, e') => inr (Csubl c e2, e')
      | inl n1 =>
          match decomp_context e2 with
          | inr (c, e') => inr (Csubr n1 c, e')
          | inl n2 => inr (Chole, e)
          end
      end
  end.

Lemma decomp_context_correct:
  forall e,
  match decomp_context e with
  | inl n => e = Econst n
  | inr (c, e') => e = remplir c e' /\ is_redex e'
  end.
Proof.
  induction e; simpl.
- auto.
- destruct (decomp_context e1) as [n1 | [c e']].
  destruct (decomp_context e2) as [n2 | [c e']].
  split. auto. subst; constructor.
  destruct IHe2; split; auto. simpl; congruence.
  destruct IHe1; split; auto. simpl; congruence.
Qed.

Definition reduit_1 (e: expr): option expr :=
  match decomp_context e with
  | inl v => None
  | inr (c, e') =>
      match contracte e' with
      | Some e'' => Some(remplir c e'')
      | None => None
      end
  end.

Remark remplir_eval:
  forall e1 e2, eval_0 e1 = eval_0 e2 ->
  forall c, eval_0 (remplir c e1) = eval_0 (remplir c e2).
Proof.
  induction c; simpl; congruence.
Qed.

Lemma reduit_1_sound:
  forall e e', reduit_1 e = Some e' -> eval_0 e' = eval_0 e.
Proof with (try discriminate).
  unfold reduit_1; intros e e' EQ.
  destruct (decomp_context e) as [v1 | [c e1]] eqn:DC...
  destruct (contracte e1) as [e2 | ] eqn:CC...
  inversion EQ. generalize (decomp_context_correct e); rewrite DC. intros [EQ1 ISRED].
  rewrite EQ1. apply remplir_eval. apply contracte_sound; auto.
Qed.

(* Decomposition avec zippers *)

Fixpoint decomp_zip (e: expr) (z: zipper) : val + zipper * expr :=
  match e with
  | Econst n => inl n
  | Esub e1 e2 =>
      match decomp_zip e1 (Zsubl z e2) with
      | inr (z, e') => inr (z, e')
      | inl n1 =>
          match decomp_zip e2 (Zsubr n1 z) with
          | inr (z, e') => inr (z, e')
          | inl n2 => inr (z, e)
          end
      end
  end.

Definition decomp_zipper (e: expr) : val + zipper * expr := decomp_zip e Ztop.

Lemma decomp_zip_correct:
  forall e z,
  match decomp_zip e z with
  | inl n => e = Econst n
  | inr (z', e') => recompose z' e' = recompose z e /\ is_redex e'
  end.
Proof.
  induction e; intros; simpl.
- auto.
- specialize (IHe1 (Zsubl z e2)). destruct (decomp_zip e1 (Zsubl z e2)) as [n1 | [z' e']].
  specialize (IHe2 (Zsubr n1 z)). destruct (decomp_zip e2 (Zsubr n1 z)) as [n2 | [z' e']].
  split. auto. subst; constructor.
  simpl in *; congruence.
  simpl in *; congruence.
Qed.

Corollary decomp_zipper_correct:
  forall e,
  match decomp_zipper e with
  | inl n => e = Econst n
  | inr (z', e') => recompose z' e' = e /\ is_redex e'
  end.
Proof.
  intros. apply (decomp_zip_correct e Ztop). 
Qed.

Definition reduit_2 (e: expr): option expr :=
  match decomp_zipper e with
  | inl v => None
  | inr (z, e') =>
      match contracte e' with
      | Some e'' => Some(recompose z e'')
      | None => None
      end
  end.

Remark recompose_eval:
  forall z e1 e2,
  eval_0 e1 = eval_0 e2 ->
  eval_0 (recompose z e1) = eval_0 (recompose z e2).
Proof.
  induction z; simpl; intros.
  auto.
  apply IHz. simpl; congruence.
  apply IHz. simpl; congruence.
Qed.

Lemma reduit_2_sound:
  forall e e', reduit_2 e = Some e' -> eval_0 e' = eval_0 e.
Proof with (try discriminate).
  unfold reduit_2; intros e e' EQ.
  destruct (decomp_zipper e) as [v1 | [z e1]] eqn:DC...
  destruct (contracte e1) as [e2 | ] eqn:CC...
  inversion EQ. generalize (decomp_zipper_correct e); rewrite DC. intros [EQ1 IR].
  rewrite <- EQ1. apply recompose_eval. apply contracte_sound; auto.
Qed.

(* Unicite de la decomposition *)

Fixpoint zconcat (z1 z2: zipper) : zipper :=
  match z1 with
  | Ztop => z2
  | Zsubl z e2 => Zsubl (zconcat z z2) e2
  | Zsubr n1 z => Zsubr n1 (zconcat z z2)
  end.

Lemma recompose_concat:
  forall z1 z2 e,
  recompose (zconcat z1 z2) e = recompose z2 (recompose z1 e).
Proof.
  induction z1; simpl; auto.
Qed.

Lemma zconcat_assoc:
  forall z1 z2 z3, zconcat (zconcat z1 z2) z3 = zconcat z1 (zconcat z2 z3).
Proof.
  induction z1; simpl; intros. 
  auto.
  rewrite IHz1; auto.
  rewrite IHz1; auto.
Qed.

Fixpoint zreverse (z: zipper) : zipper :=
  match z with
  | Ztop => Ztop
  | Zsubl z e2 => zconcat (zreverse z) (Zsubl Ztop e2)
  | Zsubr n1 z => zconcat (zreverse z) (Zsubr n1 Ztop)
  end.

Lemma zreverse_concat:
  forall z1 z2, zreverse (zconcat z1 z2) = zconcat (zreverse z2) (zreverse z1).
Proof.
  induction z1; simpl; intros.
  induction (zreverse z2); simpl. auto. congruence. congruence.
  rewrite IHz1. rewrite zconcat_assoc. auto.
  rewrite IHz1. rewrite zconcat_assoc. auto.
Qed.

Lemma zreverse_inv:
  forall z, zreverse (zreverse z) = z.
Proof.
  induction z; simpl.
  auto.
  rewrite zreverse_concat. rewrite IHz. auto.
  rewrite zreverse_concat. rewrite IHz. auto.
Qed.

Lemma zipper_rev_ind:
  forall (P: zipper -> Prop),
  P Ztop ->
  (forall z e2, P z -> P (zconcat z (Zsubl Ztop e2))) ->
  (forall z n1, P z -> P (zconcat z (Zsubr n1 Ztop))) ->
  forall z, P z.
Proof.
  intros. 
  assert (forall z', P (zreverse z')).
  { induction z'; simpl; auto. }
  rewrite <- zreverse_inv. apply H2. 
Qed.

Remark recompose_val:
  forall z e n, recompose z e = Econst n -> z = Ztop /\ e = Econst n.
Proof.
  induction z; simpl; intros. 
  auto.
  destruct (IHz _ _ H). congruence.
  destruct (IHz _ _ H). congruence.
Qed.

Lemma unique_decomp:
  forall e1 e2, is_redex e1 -> is_redex e2 ->
  forall z1 z2, recompose z1 e1 = recompose z2 e2 -> z1 = z2 /\ e1 = e2.
Proof.
  intros e1 e2 R1 R2.
  induction z1 using zipper_rev_ind; induction z2 using zipper_rev_ind;
  rewrite ? recompose_concat; simpl; intros EQ.
- auto.
- subst e1. inversion R1; subst. 
  destruct (recompose_val z2 e2 n1) as [A B]; auto. subst. inversion R2.
- subst e1. inversion R1; subst.
  destruct (recompose_val z2 e2 n2) as [A B]; auto. subst. inversion R2.
- subst e2. inversion R2; subst.
  destruct (recompose_val z1 e1 n1) as [A B]; auto. subst. inversion R1.
- inversion EQ; subst. destruct (IHz1 _ H0). split; congruence.
- inversion EQ; subst. 
  destruct (recompose_val z1 e1 n1) as [A B]; auto. subst. inversion R1.
- subst e2. inversion R2; subst. 
  destruct (recompose_val z1 e1 n2) as [A B]; auto. subst. inversion R1.
- inversion EQ; subst.
  destruct (recompose_val z2 e2 n1) as [A B]; auto. subst. inversion R2.
- inversion EQ; subst. destruct (IHz1 _ H1). split; congruence.
Qed.

(* Refocusing *)

Fixpoint size_expr (e: expr): nat :=
  match e with
  | Econst n => 1%nat
  | Esub e1 e2 => (size_expr e1 + size_expr e2 + 1)%nat
  end.

Fixpoint size_zip (z: zipper): nat :=
  match z with
  | Ztop => 0%nat
  | Zsubl z e2 => (size_expr e2 + size_zip z)%nat
  | Zsubr n1 z => (size_zip z)%nat
  end.

Definition decomp_ok (e: expr) (z: zipper) (res: val + zipper * expr) : Prop :=
  match res with
  | inl n => recompose z e = Econst n
  | inr (z', e') => recompose z e = recompose z' e' /\ is_redex e'
  end.

Require Coq.Program.Wf.

Program Fixpoint refocus (e: expr) (z: zipper)
                         {measure (size_expr e + size_zip z)%nat}
                       : {res | decomp_ok e z res} :=
  match e with
  | Esub e1 e2 =>
      refocus e1 (Zsubl z e2)
  | Econst n =>
      match z with
      | Ztop => inl n
      | Zsubl z2 e2 => refocus e2 (Zsubr n z2)
      | Zsubr n1 z2 => inr (z2, Esub (Econst n1) (Econst n))
      end
  end.
Next Obligation.
  simpl; omega.
Defined.
Next Obligation.
  split; auto. constructor.
Qed.

Theorem refocus_correct:
  forall e z, proj1_sig (refocus e z) = decomp_zipper (recompose z e).
Proof.
  intros. destruct (refocus e z) as [res OK]. simpl. red in OK.
  destruct res as [n | [z1 e1]].
  rewrite OK. auto.
  destruct OK as [A B].
  generalize (decomp_zipper_correct (recompose z e)). 
  destruct (decomp_zipper (recompose z e)) as [n | [z2 e2]].
  intros. rewrite H in A. destruct (recompose_val z1 e1 n); auto. subst.
  inversion B.
  intros [C D]. 
  assert (z1 = z2 /\ e1 = e2).
  { apply unique_decomp; auto. congruence. }
  intuition congruence.
Qed.

(* Focused transitions *)

Definition ftrans (st: expr * zipper) : val + expr * zipper :=
  match st with
  | (Econst n, Ztop) => inl n
  | (Econst n, Zsubl z e2) => inr (e2, Zsubr n z)
  | (Econst n, Zsubr n1 z) => inr (Econst (n1 - n), z)
  | (Esub e1 e2, z) => inr (e1, Zsubl z e2)
  end.

Lemma ftrans_reduit:
  forall e z e' z',
  ftrans (e, z) = inr (e', z') ->
  recompose z e = recompose z' e' \/
  reduit_2 (recompose z e) = Some (recompose z' e').
Proof.
  unfold ftrans; intros; destruct e.
- destruct z; inversion H; subst; simpl.
  auto.
  right. unfold reduit_2. 
  replace (decomp_zipper (recompose z' (Esub (Econst n0) (Econst n))))
  with (@inr val _ (z', Esub (Econst n0) (Econst n))).
  simpl. auto.
  generalize (decomp_zipper_correct (recompose z' (Esub (Econst n0) (Econst n)))).
  destruct (decomp_zipper (recompose z' (Esub (Econst n0) (Econst n)))) as [n1 | [z1 e1]].
  intros. generalize (recompose_val _ _ _ H0). intros [A B]. inversion B.
  intros [A B].
  assert (z1 = z' /\ e1 = Esub (Econst n0) (Econst n)).
  { apply unique_decomp. auto. constructor. auto. }
  destruct H0; subst. auto.
- inversion H; subst. simpl. auto.
Qed.

Lemma ftrans_correct:
  forall e z,
  match ftrans (e, z) with
  | inl n        => eval_0 (recompose z e) = n
  | inr (e', z') => eval_0 (recompose z e) = eval_0 (recompose z' e')
  end.
Proof.
  unfold ftrans; intros; destruct e.
- destruct z; simpl; auto. apply recompose_eval. auto.
- simpl. auto.
Qed.