Require Export Imp.
Require Import Relations.

Inductive tm : Type :=
  | tm_const : nat -> tm
  | tm_plus : tm -> tm -> tm.

Tactic Notation "tm_cases" tactic(first) tactic(c) :=
  first;
  [ c "tm_const" | c "tm_plus" ].

(*******************************************************************)

Module SimpleArith1.

Reserved Notation " t '==>' n " (at level 40).

Inductive eval : tm -> nat -> Prop :=
  | E_Const : forall n,
      tm_const n ==> n
  | E_Plus : forall t1 t2 n1 n2, 
      t1 ==> n1 -> 
      t2 ==> n2 ->
      tm_plus t1 t2 ==> plus n1 n2

  where " t '==>' n " := (eval t n).

End SimpleArith1.

(*******************************************************************)

Module SimpleArith2.

Reserved Notation " t '-->' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
      tm_plus (tm_const n1) (tm_const n2) --> tm_const (plus n1 n2)
  | ST_Plus1 : forall t1 t1' t2,
      t1 --> t1' ->
      tm_plus t1 t2 --> tm_plus t1' t2
  | ST_Plus2 : forall n1 t2 t2',
      t2 --> t2' -> 
      tm_plus (tm_const n1) t2 --> tm_plus (tm_const n1) t2'

  where " t '-->' t' " := (step t t').

Tactic Notation "step_cases" tactic(first) tactic(c) :=
  first;
  [ c "ST_PlusConstConst" | c "ST_Plus1" | c "ST_Plus2" ].

Example test_step_1 : 
      tm_plus 
        (tm_plus (tm_const 0) (tm_const 3))
        (tm_plus (tm_const 2) (tm_const 4))
      -->
      tm_plus 
        (tm_const (plus 0 3))
        (tm_plus (tm_const 2) (tm_const 4)).
Proof.
  Admitted.

Theorem step_deterministic:
  partial_function step.
Proof.
  Admitted.

(*******************************************************************)

Definition relation (X: Type) := X->X->Prop.

Inductive clos_refl_trans {A: Type} (R: relation A) : relation A :=
    | rt_step : forall x y, R x y -> clos_refl_trans R x y
    | rt_refl : forall x, clos_refl_trans R x x
    | rt_trans : forall x y z,
          clos_refl_trans R x y -> clos_refl_trans R y z -> clos_refl_trans R x z.

Tactic Notation "rt_cases" tactic(first) tactic(c) :=
  first;
  [ c "rt_step" | c "rt_refl" | c "rt_trans" ].

Theorem next_nat_closure_is_le : forall n m,
  (n <= m) <-> ((clos_refl_trans next_nat) n m).
Proof.
  Admitted.

(*******************************************************************)

(** The above definition of reflexive, transitive closure is
    natural -- it says, explicitly, that the reflexive and transitive
    closure of [R] is the least relation that includes [R] and that is
    closed under rules of reflexivity and transitivity.  But it turns
    out that this definition is not very convenient for doing
    proofs -- the "nondeterminism" of the rt_trans rule can sometimes
    lead to tricky inductions.
 
    Here is a more useful definition... *)

Inductive refl_step_closure {X:Type} (R: relation X) 
                            : X -> X -> Prop :=
  | rsc_refl  : forall (x : X),
                 refl_step_closure R x x
  | rsc_step : forall (x y z : X),
                    R x y ->
                    refl_step_closure R y z ->
                    refl_step_closure R x z.

Tactic Notation "rsc_cases" tactic(first) tactic(c) :=
  first;
  [ c "rsc_refl" | c "rsc_step" ].

(*******************************************************************)

Definition stepmany := refl_step_closure step.

Notation " t '-->*' t' " := (stepmany t t') (at level 40).

Lemma test_stepmany_1:
      tm_plus
        (tm_plus (tm_const 0) (tm_const 3))
        (tm_plus (tm_const 2) (tm_const 4))
   -->* 
      tm_const (plus (plus 0 3) (plus 2 4)).
Proof.
  unfold stepmany.
  Admitted.

(* eapply *)

End SimpleArith2.

(*******************************************************************)

Inductive value : tm -> Prop :=
  v_const : forall n, value (tm_const n).

Reserved Notation " t '-->' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
          tm_plus (tm_const n1) (tm_const n2)
      --> tm_const (plus n1 n2)
  | ST_Plus1 : forall t1 t1' t2,
        t1 --> t1' ->
        tm_plus t1 t2 --> tm_plus t1' t2
  | ST_Plus2 : forall v1 t2 t2',
        value v1 ->                     (* <----- n.b. *) 
        t2 --> t2' ->
        tm_plus v1 t2 --> tm_plus v1 t2'

  where " t '-->' t' " := (step t t').

Tactic Notation "step_cases" tactic(first) tactic(c) :=
  first;
  [ c "ST_PlusConstConst" | c "ST_Plus1" | c "ST_Plus2" ].

Definition stepmany := refl_step_closure step.

Notation " t '-->*' t' " := (stepmany t t') (at level 40).

Theorem progress : forall t,
  value t \/ (exists t', t --> t').
Proof.  
  Admitted.

Definition normal_form {X:Type} (R:relation X) (t:X) : Prop :=
  ~ exists t', R t t'.

Definition step_normal_form := normal_form step.

Lemma value_is_nf : forall t,
  value t -> step_normal_form t.
Proof.
  intros t H. unfold step_normal_form. unfold normal_form.
  intros contra. inversion H.
  rewrite <- H0 in contra. destruct contra as [t' P]. inversion P.   Qed.

Lemma nf_is_value : forall t,
  step_normal_form t -> value t.
Proof.
  (* This is a corollary of [progress]. *)
  intros t H.
  unfold normal_form in H.
  assert (value t \/ exists t', t --> t') as G.
    SCase "Proof of assertion". apply progress.
  inversion G.
    SCase "l". apply H0.
    SCase "r". apply ex_falso_quodlibet. apply H. assumption.  Qed.

Definition normal_form_of (t t' : tm) :=
  (t -->* t' /\ step_normal_form t').

Definition normalizing {X:Type} (R:relation X) :=
  forall t, exists t',
    (refl_step_closure R) t t' /\ normal_form R t'.

Theorem step_normalizing :
  normalizing step.
Proof.
  (* see Smallstep.v *)
  Admitted.

(* See Smallstep.v, Small-Step Imp *)