gistfile1.txt

Lemma star_red_lookup: forall s f e e', star_red_exp s e e' ->
                                        star_red_exp s (Elookup e f) (Elookup e' f).
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_lookup_simpl.
    apply H. apply IHstar.
Qed.

Lemma star_red_plus_left: forall s e1 e2 e1', star_red_exp s e1 e1' ->
                                              star_red_exp s (Eplus e1 e2) (Eplus e1' e2).
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_plus_left.
    apply H. apply IHstar.
Qed.

Lemma star_red_plus_right: forall s e1 e2 e2', star_red_exp s e2 e2' ->
                                               star_red_exp s (Eplus e1 e2) (Eplus e1 e2').
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_plus_right.
    apply H. apply IHstar.
Qed.

Lemma star_red_minus_left: forall s e1 e2 e1', star_red_exp s e1 e1' ->
                                               star_red_exp s (Eminus e1 e2) (Eminus e1' e2).
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_minus_left.
    apply H. apply IHstar.
Qed.

Lemma star_red_minus_right: forall s e1 e2 e2', star_red_exp s e2 e2' ->
                                                star_red_exp s (Eminus e1 e2) (Eminus e1 e2').
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_minus_right.
    apply H. apply IHstar.
Qed.

Lemma star_red_subst_left: forall s e1 e2 f e1', star_red_exp s e1 e1' ->
                                                 star_red_exp s (Esubst e1 f e2) (Esubst e1' f e2).
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_subst_left.
    apply H. apply IHstar.
Qed.

Lemma star_red_subst_right: forall s e1 e2 f e2', star_red_exp s e2 e2' ->
                                                  star_red_exp s (Esubst e1 f e2) (Esubst e1 f e2').
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_subst_right.
    apply H. apply IHstar.
Qed.

Theorem eval_expr_to_red : forall s e v, eval_expr s e = Some v -> star_red_exp s e (Econst v).
Proof.
  intros s e.
  induction e.
  - intros. simpl eval_expr in H. injection H. intro.
    rewrite H0. apply star_refl.
  - intros. 
    eapply star_step. apply red_empty_rec.
    simpl eval_expr in H. injection H. intro.
    rewrite H0. apply star_refl.
  - intros. simpl eval_expr in H.
    eapply star_step.
    apply red_var. apply H. apply star_refl.
  - intros. simpl eval_expr in H.
    case_eq (eval_expr s e1).
    + case_eq (eval_expr s e2).
      * intros.
        case_eq v0. intros. rewrite H2 in H0.
        case_eq v1. intros. rewrite H3 in H1.
        rewrite H0 in H. rewrite H1 in H.
        injection H. intro.
        eapply star_trans.
        eapply star_trans.
        eapply star_red_plus_left.
        apply IHe1. apply H1.
        eapply star_red_plus_right.
        apply IHe2. apply H0.
        rewrite <- H4.
        eapply star_step.
        apply red_plus_simpl.
        apply star_refl.
        (* Autres cas, absurdes. *)
        intros. rewrite H3 in H1. rewrite H1 in H. discriminate.
        intros. rewrite H2 in H0. rewrite H0 in H. 
        case_eq v1; intros; rewrite H3 in H1; rewrite H1 in H; discriminate.
      * intros. case_eq v0; intros;
        rewrite H0 in H; try (rewrite H2 in H1); rewrite H1 in H; discriminate.
        + intros. rewrite H0 in H. discriminate.
  - intros. simpl eval_expr in H.
    case_eq (eval_expr s e1).
    + case_eq (eval_expr s e2).
      * intros.
        case_eq v0. intros. rewrite H2 in H0.
        case_eq v1. intros. rewrite H3 in H1.
        rewrite H0 in H. rewrite H1 in H.
        injection H. intro.
        eapply star_trans.
        eapply star_trans.
        eapply star_red_minus_left.
        apply IHe1. apply H1.
        eapply star_red_minus_right.
        apply IHe2. apply H0.
        rewrite <- H4.
        eapply star_step.
        apply red_minus_simpl.
        apply star_refl.
        (* Autres cas, absurdes. *)
        intros. rewrite H3 in H1. rewrite H1 in H. discriminate.
        intros. rewrite H2 in H0. rewrite H0 in H. 
        case_eq v1; intros; rewrite H3 in H1; rewrite H1 in H; discriminate.
      * intros. case_eq v0; intros;
        rewrite H0 in H; try (rewrite H2 in H1); rewrite H1 in H; discriminate.
    + intros. rewrite H0 in H. discriminate.
  - intros.
    simpl eval_expr in H.
    case_eq (eval_expr s e). intros.
    case_eq v0.
    + intros. rewrite H1 in H0. rewrite H0 in H. discriminate.
    + intros. rewrite H1 in H0. rewrite H0 in H.
      assert (star_red_exp s (Elookup e r) (Elookup (Econst v0) r)).
      apply star_red_lookup. apply IHe.
      rewrite H1. assumption.
      eapply star_trans. apply H2.
      rewrite H1. eapply star_step.
      apply red_lookup. apply H.
      apply star_refl.
    + intros. rewrite H0 in H. simpl eval_expr in H. discriminate.
  - intros. simpl eval_expr in H.
    case_eq (eval_expr s e1). {
      case_eq (eval_expr s e2). {
        intros.
        case_eq v1.
        + intros. rewrite H2 in H1. rewrite H1 in H. discriminate.
        + intros. rewrite H2 in H1. rewrite H1 in H. rewrite H0 in H.
          eapply star_trans.
          eapply star_trans.
          apply star_red_subst_left.
          apply IHe1. apply H1.
          apply star_red_subst_right.
          apply IHe2. apply H0.
          injection H. intro.
          rewrite <- H3.
          eapply star_step.
          apply red_subst_simpl.
          apply star_refl. 
      }
      {
        intros. rewrite H1 in H. rewrite H0 in H.
        case_eq v0; intros; rewrite H2 in H; discriminate.
      }
    }
    {
      intros. rewrite H0 in H. discriminate.
    }
Qed.