transit.v

Require Import List.

Open Scope list_scope.

Import ListNotations.

Variable String : Type.

Axiom string_eq_dec : forall s1 s2 : String, {s1 = s2} + {s1 <> s2}.

Inductive User := user : String -> User.

Inductive LoginState :=
    Logout : LoginState
  | Login  : String -> LoginState.

Inductive State := state : User -> LoginState -> list String ->State.

Inductive Screen :=
  | Menu : State -> Screen
  | LoginV : State -> Screen
  | Setting : State -> Screen.

Definition pick_state sc : State :=
  match sc with
  | Menu s => s
  | LoginV s => s
  | Setting s => s
  end.

Definition pick_user s : User :=
  match s with
  | state u _ _ => u
  end.

Definition pick_user_from_scr sc : User :=
  pick_user (pick_state sc).

Inductive OneStepTransit : Screen -> Screen -> Type :=
  | MenuToLogin : forall s, OneStepTransit (Menu s) (LoginV s)
  | LoginToMenu : forall s, OneStepTransit (LoginV s) (Menu s)
  | LoginToMenuLogin : forall p l, In p l ->
      OneStepTransit (LoginV (state (user p) Logout l)) (Menu (state (user p) (Login p) l))
  | LoginToSetting : forall s, OneStepTransit (LoginV s) (Setting s)
  | ChangeUser : forall u u' ls l sc sc',
      pick_state sc = state u ls l -> pick_state sc' = state u' ls l ->
      OneStepTransit sc sc.

Inductive Transit sc1 sc2 : Type :=
  | OneStep : OneStepTransit sc1 sc2 -> Transit sc1 sc2
  | Trans : forall sc, OneStepTransit sc1 sc -> Transit sc sc2 ->
      Transit sc1 sc2.

Fixpoint pass_screens {sc1 sc2} sc1' sc2' (t : Transit sc1 sc2) : Prop :=
  match t with
  | OneStep o => sc1 = sc1' /\ sc2 = sc2'
  | Trans sc o t0 => (sc1 = sc1' /\ sc = sc2') \/ pass_screens sc1' sc2' t0
  end.

Lemma not_change_list_os : forall u u' ls ls' l l' sc sc',
  pick_state sc = state u ls l -> pick_state sc' = state u' ls' l' ->
  OneStepTransit sc sc' -> l = l'.
Proof with simpl in *; auto.
intros.
inversion X; subst; simpl in *; subst; inversion H; subst...
inversion H0. congruence.
congruence.
Qed.

Lemma not_change_list : forall u u' ls ls' l l' sc sc',
  pick_state sc = state u ls l -> pick_state sc' = state u' ls' l' -> Transit sc sc' ->
  l = l'.
Proof with simpl in *; auto.
intros.
revert H H0. revert ls ls' u u'.
induction X; intros.
  apply (not_change_list_os u u' ls ls' l l' sc1 sc2)...
inversion o; subst; simpl in *; subst; try(eapply IHX; try apply eq_refl; apply H0).
inversion H... subst... eapply IHX; eauto.
rewrite H1 in H. inversion H; subst... eapply IHX; eauto.
Qed.

Lemma not_change_pwd_os : forall u u' p p' l sc sc',
  pick_state sc = state u (Login p) l -> pick_state sc' = state u' (Login p') l ->
  OneStepTransit sc sc' -> p = p'.
Proof with simpl in *; auto.
intros.
inversion X; subst; simpl in *; subst; inversion H...
congruence.
Qed.

Lemma not_change_pwd : forall u u' p p' l sc sc',
  pick_state sc = state u (Login p) l -> pick_state sc' = state u' (Login p') l -> 
  Transit sc sc' -> p = p'.
Proof with simpl in *; auto.
intros.
revert H H0. revert p p'.
induction X; intros...
  inversion o; subst; simpl in *; subst; inversion H... rewrite H0 in H4. inversion H4...
inversion o; subst; simpl in *; subst...
discriminate.
Qed.

Lemma pass_logout_to_login1 : forall u p l sc1 sc2,
  pick_state sc1 = state u Logout l -> pick_state sc2 = state u (Login p) l ->
  OneStepTransit sc1 sc2 -> sc1 = LoginV (state u Logout l).
Proof with simpl in *; auto.
intros.
inversion X; subst; simpl in *; subst; try discriminate...
  inversion H0...
congruence.
Qed.

Lemma pass_logout_to_login2 : forall u p l sc1 sc2,
  pick_state sc1 = state u Logout l -> pick_state sc2 = state u (Login p) l ->
  OneStepTransit sc1 sc2 -> sc2 = Menu (state u (Login p) l).
Proof with simpl in *; eauto.
intros.
inversion X; subst; simpl in *; subst; try discriminate. inversion H0...
congruence.
Qed.

Theorem pass_login : forall u p l sc1 sc2 (t : Transit sc1 sc2),
  pick_state sc1 = state u Logout l -> pick_state sc2 = state u (Login p) l
  -> pass_screens (LoginV (state u Logout l)) (Menu (state u (Login p) l)) t.
Proof with simpl in *; auto.
intros.
revert H H0.
induction t; intros...
  constructor. eapply pass_logout_to_login1; eauto. eapply pass_logout_to_login2; eauto.
inversion o; subst...
left.
constructor; inversion H...
replace p with p0... eapply not_change_pwd; subst; eauto...
Qed.

Lemma pass_login_then_have_pwd : forall u p l sc1 sc2 (t : Transit sc1 sc2),
  pass_screens (LoginV (state u Logout l)) (Menu (state u (Login p) l)) t -> In p l.
Proof with simpl in *; auto.
intros.
induction t...
  destruct H. subst. inversion o...
destruct H...
  destruct H. subst. inversion o...
Qed.

Lemma pass_login_then_user : forall u p l sc1 sc2 (t : Transit sc1 sc2),
  pass_screens (LoginV (state u Logout l)) (Menu (state u (Login p) l)) t -> u = user p.
Proof with simpl in *; auto.
intros.
induction t...
  destruct H. subst. inversion o...
destruct H...
destruct H. subst. inversion o...
Qed.

Theorem cannnot_login_without_pwd : forall u p,
  Transit (Menu (state u Logout nil)) (Menu (state u (Login p) nil)) -> False.
Proof with simpl in*; auto.
intros.
assert (In p nil).
  eapply pass_login_then_have_pwd... apply (pass_login u p nil _ _ X)...
auto.
Qed.

Fixpoint transit_without_user_change {sc1 sc2} (t : Transit sc1 sc2) : Prop :=
  match t with
  | OneStep o => pick_user_from_scr sc1 = pick_user_from_scr sc2
  | Trans sc o t0 => pick_user_from_scr sc1 = pick_user_from_scr sc /\
      transit_without_user_change t0
  end.

Theorem can_login_then_user : forall p p' l
  (t : Transit (Menu (state (user p) Logout l)) (Menu (state (user p) (Login p') l))),
  transit_without_user_change t -> p = p'.
Proof with simpl in *; auto.
intros.
assert (pass_screens (LoginV (state (user p) Logout l)) (Menu (state (user p) (Login p') l)) t).
  apply pass_login...
apply pass_login_then_user in H0.
congruence.
Qed.