tapl-3-5-13.v

Inductive term :=
  Tru
| Fls
| IfThenElse : term -> term -> term -> term.

Notation "'If' c1 'Then' c2 'Else' c3" := (IfThenElse c1 c2 c3)
(at level 200, right associativity, format
"'[v   ' 'If'  c1 '/' '[' 'Then'  c2  ']' '/' '[' 'Else'  c3 ']' ']'").

Reserved Notation "x --> y" (at level 60).

Inductive step : term -> term -> Prop :=
  EIfTrue : forall t2 t3, (If Tru Then t2 Else t3) --> t2
| EIfFalse : forall t2 t3, (If Fls Then t2 Else t3) --> t3
| EIf : forall t1 t1' t2 t3, t1 --> t1' -> (If t1 Then t2 Else t3) --> (If t1' Then t2 Else t3)
where "x --> y" := (step x y).

Ltac auto_inversion step :=
   repeat match goal with
      H : step Tru _ |- _ => inversion H
    | H : step Fls _ |- _ => inversion H
    | H : step (IfThenElse _ _ _) _ |- _ => inversion H; clear H; subst; try f_equal; auto
    end.

Theorem step_deterministic : forall t t', t --> t' -> forall t'', t --> t'' -> t' = t''.
Proof.
  intros t t' H.
  induction H; intros; auto_inversion step.
  (* ^ - ^ *)
Qed.

Reserved Notation "x -->' y" (at level 60).

Inductive step' : term -> term -> Prop :=
  EIfTrue' : forall t2 t3, (If Tru Then t2 Else t3) -->' t2
| EIfFalse' : forall t2 t3, (If Fls Then t2 Else t3) -->' t3
| EIf' : forall t1 t1' t2 t3, t1 -->' t1' -> (If t1 Then t2 Else t3) -->' (If t1' Then t2 Else t3)
| EFunny2 : forall t1 t2 t2' t3, t2 -->' t2' -> (If t1 Then t2 Else t3) -->' (If t1 Then t2' Else t3)
where "x -->' y" := (step' x y).

Ltac fo := eexists; firstorder (try constructor; eauto).

Lemma step'_loc_conf : forall t s s',
    t -->' s -> t -->' s' ->
    exists u, (s = u /\ s' = u) \/ (s = u /\ s' -->' u) \/ (s -->' u /\ s' = u) \/ (s -->' u /\ s' -->' u).
Proof.
  intros t s s' H.
  revert s'.
  induction H; intros; auto_inversion step'; try solve [fo].
  - destruct (IHstep' _ H5).
    destruct H0 as [|[|[]]]; destruct H0; subst; fo.
  - destruct (IHstep' _ H5).
    destruct H0 as [|[|[]]]; destruct H0; subst; fo.
    (* ^ o ^ *)
Qed.