Inductive term :=
  | zero : term
  | succ : term -> term
  | false : term
  | true : term
  | iszero : term -> term
  | if_then_else : term -> term -> term -> term.

Inductive step : term -> term -> Prop :=
  | E_Succ : forall t1 : term, forall t1' : term,
    step t1 t1' ->
    step (succ t1) (succ t1')
  | E_IsZeroZero :
    step (iszero zero) true
  | E_IsZeroSucc : forall t : term,
    step (iszero (succ t)) false
  | E_IfTrue : forall t2 : term, forall t3 : term,
    step (if_then_else true t2 t3) t2
  | E_IfFalse : forall t2 : term, forall t3 : term,
    step (if_then_else false t2 t3) t3
  | E_If : forall t1 : term, forall t1' : term, forall t2 : term, forall t3 : term,
    step t1 t1' ->
    step (if_then_else t1 t2 t3) (if_then_else t1' t2 t3).


Section Exercise1.

  Definition exercise1 :
    step (succ (succ (iszero (succ zero)))) (succ (succ false)) :=
      E_Succ (succ (iszero (succ zero))) (succ false) (
      E_Succ (iszero (succ zero)) false (
      E_IsZeroSucc zero)).

End Exercise1.


Section Exercise2.

  Inductive multistep : term -> term -> Prop :=
    | M_Single : forall t : term, forall t' : term,
      step t t' ->
      multistep t t'
    | M_Reflexive : forall t : term,
      multistep t t
    | M_Transitive : forall t : term, forall t' : term, forall t'' : term,
      multistep t t' -> multistep t' t'' ->
      multistep t t''.

  Definition derivation1 :
    step (if_then_else (iszero zero) zero zero) (if_then_else true zero zero) :=
      E_If (iszero zero) true zero zero
      E_IsZeroZero.

  Definition derivation2 :
    step (if_then_else true zero zero) zero :=
      E_IfTrue zero zero.

  Definition exercise2 :
    multistep (if_then_else (iszero zero) zero zero) zero :=
      M_Transitive (if_then_else (iszero zero) zero zero) (if_then_else true zero zero) zero
        (M_Single (if_then_else (iszero zero) zero zero) (if_then_else true zero zero) derivation1)
        (M_Single (if_then_else true zero zero) zero derivation2).
 
End Exercise2.

Section Exercise3.

  Require Import Arith.
  
  Fixpoint size (t : term) :=
    match t with
      | zero => 1
      | succ t => 1 + size t
      | false => 1
      | true => 1
      | iszero t => 1 + size t
      | if_then_else t1 t2 t3 => 1 + (size t1 + (size t2 + size t3))
    end.

  Lemma lt_n_SSnm : forall n : nat, forall m : nat, n < S (S (n + m)).
    intros n m.
    induction m.

      rewrite plus_0_r.
      apply lt_trans with (S n).
      apply lt_n_Sn.
      apply lt_n_Sn.

      rewrite <- plus_n_Sm.
      apply lt_trans with (S (S (n + m))).
      assumption.
      apply lt_n_Sn.

    Qed.

  Lemma decreasing : forall t : term, forall t' : term, step t t' -> size t' < size t.
    intros t t' d.
    induction d.

      simpl.
      apply lt_n_S.
      assumption.

      simpl.
      auto.

      simpl.
      apply lt_n_S.
      apply lt_O_Sn.

      simpl.
      apply lt_n_SSnm.

      simpl.
      rewrite plus_comm.
      apply lt_n_SSnm.
        
      simpl.
      apply lt_n_S.
      apply plus_lt_compat_r.
      assumption.

    Qed.

End Exercise3.