password.v

Require Import Arith.
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 := Owner | Other.

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

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

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

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 Logout l)) (Menu (state (Login p) l))
  | LoginToSetting : forall s, OneStepTransit (LoginV s) (Setting s).

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

Lemma loginst_eq_dec : forall l1 l2 : LoginState, {l1 = l2} + {l1 <> l2}.
Proof with simpl in *; auto.
intros.
destruct l1; destruct l2...
right. discriminate.
right. discriminate.
destruct (string_eq_dec s s0).
left. subst...
right. intro. apply n. inversion H...
Qed.

Lemma state_eq_dec : forall s1 s2 : State, {s1 = s2} + {s1 <> s2}.
Proof with simpl in *; auto.
intros.
destruct s1; destruct s2...
destruct l; destruct l1; (right; discriminate)||auto;
  destruct (list_eq_dec string_eq_dec l0 l2); subst...
right. intro. inversion H...
destruct (string_eq_dec s s0)...
left. subst. auto.
right. intro. inversion H...
right. intro. inversion H...
Qed.

Lemma screen_eq_dec : forall sc1 sc2 : Screen, {sc1 = sc2} + {sc1 <> sc2}.
Proof with simpl in *; auto.
intros.
destruct sc1; destruct sc2; (right; discriminate)||auto;
  destruct (state_eq_dec s s0); subst...
right. intro. inversion H...
right. intro. inversion H...
right. intro. inversion H...
Qed.

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 pass_notmlogin_to_nlogin : forall p l sc (t : Transit sc (Menu (state (Login p) l))),
  sc <> Menu (state (Login p) l) ->
  exists sc', sc' <> (Menu (state (Login p) l)) /\
    pass_screens sc' (Menu (state (Login p) l)) t.
Proof with simpl in *; auto.
intros.
remember (Menu (state (Login p) l)) as scn.
induction t...
  exists sc1...
subst...
destruct (screen_eq_dec sc (Menu (state (Login p) l))).
  subst. exists sc1...
destruct (IHt eq_refl n).
exists x.
intuition.
Qed.

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

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

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

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

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

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

Lemma not_change_pwd : forall p p' l sc sc',
  pick_state sc = state (Login p) l -> pick_state sc' = state (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...
inversion o; subst; simpl in *; subst...
discriminate.
Qed.

Theorem pass_login : forall p l sc1 sc2
    (t : Transit sc1 sc2), pick_state sc1 = state Logout l -> pick_state sc2 = state (Login p) l
  -> pass_screens (LoginV (state Logout l)) (Menu (state (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; eauto. simpl; congruence.
Qed.

Lemma pass_login_then_have_pwd : forall p l sc1 sc2 (t : Transit sc1 sc2),
  pass_screens (LoginV (state Logout l)) (Menu (state (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.

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