(* Syntax. *)

Inductive t
  := t_true
   | t_false
   | if_then_else : t -> t -> t -> t.

Inductive v := v_true | v_false.

(* Semantics. *)

Inductive step : t -> t -> Prop
  := step_true : forall t2 t3, step (if_then_else t_true t2 t3) t2
   | step_false : forall t2 t3, step (if_then_else t_false t2 t3) t3
   | step_if : forall t1 t1' t2 t3, step t1 t1' -> step (if_then_else t1 t2 t3) (if_then_else t1' t2 t3).

Definition val t := match t with t_true | t_false => True | _ => False end.

Lemma val_stuck : forall t t', val t -> ~ step t t'.
  intros t t' Ht; induction 1; contradiction Ht.
Qed.

Lemma determinacy : forall t t' t'', step t t' -> step t t'' -> t' = t''.
  intros t t' t'' Ht.
  generalize dependent t''.
  induction Ht.
  (* We proceed by induction on a derivation of [step t t'] *)
  - (* Suppose the last rule applied was [step_true].
       We have [if true then t2 else t3 -> t''] and wish to show that [t2 = t'']. *)
    (* The only way we could've gotten the assumption [if true then t2 else t3 -> t'']
       is if t2 = t'': *)
    inversion 1.
    + (* Suppose the last rule applied in the proof of [if true then t2 else t3 -> t'']
         was step_true. Then t2 = t'' as desired. *) reflexivity.
      (* The last rule couldn't have been step_false, because our assumption is
         [if true then t2 else t3 -> t''] and step_false would only be able to give us
         [if false then t2 else t3 -> t'']. *)
    + (* Now suppose the last rule applied was step_if. That is, the proof tree looks like

                               true -> t1'
          --------------------------------------------------- step_if
           if true then t2 else t3 -> if t1' then t2 else t3

         for some t1', where t'' = if t1' then t2 else t3.

         This is clearly impossible: true -> t1' is never derivable, because constants
         don't step to anything (by lemma val_stuck). *)
      apply val_stuck in H4; [contradiction|exact I].
    (* This completes the first case of the induction. *)
  - (* The second case (where we suppose the last rule applied was [step_false] is largely
       analogous to the first one. *)
    inversion 1; auto; apply val_stuck in H4; [contradiction|exact I].
  - (* Finally, suppose the last rule applied was [step_if]. *)
    intros t''.
    (* We have [if t1 then t2 else t3 -> t''] and [t1 -> t1'] and our induction hypothesis
       says that, for any t4, [t1 -> t4 implies t1' = t4].
       We wish to show that [if t1' then t2 else t3 -> t'']. *)
    (* Because we know that [t1 -> t1'], [t1] can't be a value (by val_stuck again).
       Thus, the last rule applied in the proof of [if t1 then t2 else t3 -> t'']
       must have been step_if: *)
    inversion 1; subst.
    + (* The last rule couldn't have been step_true. *)
      apply val_stuck in Ht; [contradiction|exact I].
    + (* The last rule couldn't have been step_false. *)
      apply val_stuck in Ht; [contradiction|exact I].
    + (* The last rule was step_if; i.e. the proof of our assumption
         [if t1 then t2 else t3 -> t''] must've looked like

                           t1 -> t4
         ----------------------------------------------
         if t1 then t2 else t3 -> if t4 then t2 else t3

         for some t4, where t'' = if t4 then t2 else t3.

      We wish to show that [if t1' then t2 else t3 = if t4 then t2 else t3].
      It's sufficient to show that t1' = t4.
      This follows from our induction hypothesis:
        Our induction hypothesis says that, for any t5, [t1 -> t5 implies t1' = t5].
        Since we know t1 -> t4, we instantiate t5 := t4 to get t1' = t4 as desired. *)
      rewrite (IHHt _ H4).
      reflexivity.
Qed.