gistfile1.txt

Theorem nat_to_red: forall s e v, nat_expr s e (Econst v) -> star_red_exp s e (Econst v).
Proof.
  intros s e.
  induction e; intros v' H; inversion H; subst.
  - constructor.
  - eapply star_step. constructor. apply star_refl.
  - eapply star_step. constructor. apply H3. apply star_refl.
  - apply IHe1 in H4. apply IHe2 in H5.
    inversion H4; subst.
    + (* e1 = (Econst (Vint i1)) *)
      inversion  H5; subst.
      * (* e2 = (Econst (Vint i2)) *)
        eapply star_step. apply red_plus_simpl. constructor.
      * (* e2 ->+ (Econst (Vint i2)) *)
        eapply star_step. apply red_plus_right. apply H0.
        eapply star_trans. apply star_red_plus_right. apply H1.
        eapply star_step. apply red_plus_simpl. apply star_refl.
    + (* e1 ->+ (Econst (Vint i1)) *)
      inversion H5; subst.
      * (* e2 = (Econst (Vint i2)) *)
        eapply star_step. apply red_plus_left. apply H0.
        eapply star_trans. apply star_red_plus_left. apply H1.
        eapply star_step. apply red_plus_simpl. apply star_refl.
      * eapply star_trans. apply star_red_plus_left. apply H4.
        eapply star_trans. apply star_red_plus_right. apply H5.
        eapply star_step. apply red_plus_simpl. apply star_refl.
  - apply IHe1 in H4. apply IHe2 in H5.
    inversion H4; subst.
    + (* e1 = (Econst (Vint i1)) *)
      inversion  H5; subst.
      * (* e2 = (Econst (Vint i2)) *)
        eapply star_step. apply red_minus_simpl. constructor.
      * (* e2 ->+ (Econst (Vint i2)) *)
        eapply star_step. apply red_minus_right. apply H0.
        eapply star_trans. apply star_red_minus_right. apply H1.
        eapply star_step. apply red_minus_simpl. apply star_refl.
    + (* e1 ->+ (Econst (Vint i1)) *)
      inversion H5; subst.
      * (* e2 = (Econst (Vint i2)) *)
        eapply star_step. apply red_minus_left. apply H0.
        eapply star_trans. apply star_red_minus_left. apply H1.
        eapply star_step. apply red_minus_simpl. apply star_refl.
      * eapply star_trans. apply star_red_minus_left. apply H4.
        eapply star_trans. apply star_red_minus_right. apply H5.
        eapply star_step. apply red_minus_simpl. apply star_refl.
  - apply IHe in H4.
    eapply star_trans. apply star_red_lookup. apply H4.
    eapply star_step. apply red_lookup. apply H5. apply star_refl.
  - apply IHe1 in H3. apply IHe2 in H6.
    eapply star_trans. apply star_red_subst_left. apply H3.
    eapply star_trans. apply star_red_subst_right. apply H6.
    eapply star_step. apply red_subst_simpl. apply star_refl.
Qed.