Require Import chan.
Require Import chanlist.
Require Import util_for_tactics.
Require Import applpi.
Require Import cong.
Require Import cong_tactic.
Require Import logic.
Require Import logic_prop.

 (* tactic to prove that ZEROS holds of some state *)

(*Tactic Definition SolveZEROS_direct :=
Match Context With
[ |- (sat ZEROS ?1#zeroP) ] ->
Unfold ZEROS;
Apply CONSISTS_sat;
Exists zeroP;
Exists zeroP;
Split; [ProcCong | Split; [Apply ISZERO_sat; Simpl; Auto | Apply ISZERO_sat; Simpl; Auto]].

Tactic Definition SolveZEROS :=
Match Context With
  [ |- (sat ZEROS ?1#(parP ?2 ?3)) ] ->
Apply sat_ZEROS_parP;
Split; [SolveZEROS | SolveZEROS]
| [ |- (sat ZEROS ?1#zeroP)] ->
SolveZEROS_direct
| _ -> Fail.*)

(** tactic to prove that OUTPUTS holds of some state *)

Lemma sat_OUTPUTS_OUTPUTS_parP :
 forall (A : Set) (b : bool) (c : chan A b) (v : A) 
   (f : form) (L : ChanList) (P Q : proc),
 sat (OUTPUTS c v f) (L # P) \/ sat (OUTPUTS c v f) (L # Q) ->
 sat (OUTPUTS c v f) (L # parP P Q).
intros.
inversion_clear H.
generalize (OUTPUTS_sat_inv H0); intro.
inversion_clear H.
inversion_clear H1.
inversion_clear H.
apply OUTPUTS_sat.
exists (parP x Q).
exists x0.
split; auto.
apply cong_tr with (parP (parP (c << v >> x0) x) Q).
apply cong_par.
auto.
apply cong_refl.
ProcCong.
generalize (OUTPUTS_sat_inv H0); intro.
inversion_clear H.
inversion_clear H1.
apply OUTPUTS_sat.
exists (parP x P).
exists x0.
split; auto.
apply cong_tr with (parP P (parP (c << v >> x0) x)).
apply cong_par.
apply cong_refl.
intuition.
ProcCong.
intuition.
Qed.

(*Tactic Definition SolveISOUTPUT :=
Match Context With
[ |- (sat (ISOUTPUT ?3 ?4 ?5) ?6#(outP ?7 ?8 ?9)) ] ->
Apply ISOUTPUT_sat;
Exists ?9;
Split; [Auto | Idtac].*)

(*Lemma SolveISOUTPUT_test : (A:Set)(b:bool)(c:(chan A b))(v:A)(P:proc)(f:form)
(sat (ISOUTPUT A b c v f) nilC#(outP c v P)).
Intros.
SolveISOUTPUT.
Abort.*)

Ltac test_val v w :=
  let v' := eval compute in v with w' := eval compute in w in
  match constr:(v' = w') with
  | (?X1 = ?X1) => idtac
  | (?X1 = ?X2) => fail
  end.

Ltac SolveOUTPUTS_direct :=
  match goal with
  |  |- (sat (OUTPUTS ?X3 ?X4 ?X5) (?X6 # ?X7 << ?X8 >> ?X9)) =>
      test_chan X3 X7; test_val X4 X8; apply OUTPUTS_sat; exists zeroP;
       exists X9; split; [ ProcCong | idtac ]
  end.

(*Lemma SolveOUTPUTS_direct_test : (A:Set)(b:bool)(c:(chan A b))(v:A)(P:proc)(f:form)
(sat (OUTPUTS c v f) nilC#(outP c v P)).
Intros.
SolveOUTPUTS_direct.
Abort.*)

Ltac SolveOUTPUTS :=
  match goal with
  |  |- (sat (OUTPUTS ?X3 ?X4 ?X5) (?X6 # parP ?X7 ?X8)) =>
      apply sat_OUTPUTS_OUTPUTS_parP; first
       [ right; SolveOUTPUTS | left; SolveOUTPUTS ]
  |  |- (sat (OUTPUTS ?X3 ?X4 ?X5) (?X6 # OutAtom ?X7 ?X8)) =>
      unfold OutAtom in |- *; SolveOUTPUTS_direct
  |  |- (sat (OUTPUTS ?X3 ?X4 ?X5) (?X6 # ?X7 << ?X8 >> ?X9)) =>
      SolveOUTPUTS_direct
  end.

(*Lemma SolveOUTPUTS_test : (A:Set)(b:bool)(c:(chan A b))(v:A)(P:proc)(f:form)
(sat (OUTPUTS c v f) nilC#(parP zeroP (parP (outP c v P) zeroP))).
Intros.
SolveOUTPUTS.
Abort.*)

(** tactic to prove that INPUTS holds of some state *)

Lemma sat_INPUTS_INPUTS_parP :
 forall (A : Set) (b : bool) (c : chan A b) (f : form) 
   (L : ChanList) (P Q : proc),
 sat (INPUTS c f) (L # P) \/ sat (INPUTS c f) (L # Q) ->
 sat (INPUTS c f) (L # parP P Q).
intros.
inversion_clear H.
generalize (INPUTS_sat_inv H0); intro.
inversion_clear H.
inversion_clear H1.
decompose [and] H; clear H.
apply INPUTS_sat.
exists (parP Q x).
exists x0.
split.
apply cong_tr with (parP (parP (c ?? x0) x) Q).
apply cong_par.
auto.
apply cong_refl.
ProcCong.
auto.
generalize (INPUTS_sat_inv H0); intro.
inversion_clear H.
inversion_clear H1.
decompose [and] H; clear H.
apply INPUTS_sat.
exists (parP P x).
exists x0.
split.
apply cong_tr with (parP P (parP (c ?? x0) x)).
apply cong_par.
apply cong_refl.
auto.
ProcCong.
auto.
Qed.

(*Tactic Definition SolveISINPUT :=
Match Context With
[ |- (sat (ISINPUT ?3 ?4) ?6#(inP ?7 ?8)) ] ->
Apply ISINPUT_sat;
Exists ?8;
Split; [Auto | Intro; Idtac].

Tactic Definition SolveISRINPUT :=
Match Context With
[ |- (sat (ISRINPUT ?3 ?4) ?6#(rinP ?7 ?8)) ] ->
Apply ISRINPUT_sat;
Exists ?8;
Split; [Auto | Intro; Idtac].*)

(*Lemma SolveINPUTS_test : (A:Set)(b:bool)(c:(chan A b))(v:A)(P:A->proc)(f:form)
(sat (INPUTS c f) nilC#(inP c P)).
Intros.
Apply INPUTS_sat.
Exists zeroP.
Exists P.
Split; [ProcCong | Idtac].
Abort.*)

Ltac SolveINPUTS_direct :=
  match goal with
  |  |- (sat (INPUTS ?X3 ?X4) (?X6 # ?X7 ?? ?X8)) =>
      test_chan X3 X7; apply INPUTS_sat; exists zeroP; exists X8; split;
       [ ProcCong | idtac ]
  end.

Ltac SolveINPUTS_direct_rinP :=
  match goal with
  |  |- (sat (INPUTS ?X3 ?X4) (?X6 # ?X7 ??* ?X8)) =>
      test_chan X3 X7; apply INPUTS_sat; exists (X7 ??* X8); exists X8; split;
       [ apply cong_tr with (parP (X7 ??* X8) (X7 ?? X8));
          [ apply cong_rep | apply cong_comm ]
       | idtac ]
  end.

(*Lemma SolveINPUTS_test2 : (A:Set)(b:bool)(c:(chan A b))(v:A)(P:A->proc)(f:form)
(sat (INPUTS c f) nilC#(rinP c P)).
Intros.
SolveINPUTS_direct_rinP.*)

Ltac SolveINPUTS :=
  match goal with
  |  |- (sat (INPUTS ?X3 ?X4) (?X6 # parP ?X7 ?X8)) =>
      apply sat_INPUTS_INPUTS_parP; first
       [ right; SolveINPUTS | left; SolveINPUTS ]
  |  |- (sat (INPUTS ?X3 ?X4) (?X6 # InAtom ?X7)) =>
      unfold OutAtom in |- *; SolveINPUTS_direct
  |  |- (sat (INPUTS ?X3 ?X4) (?X6 # ?X7 ?? ?X8)) => SolveINPUTS_direct
  |  |- (sat (INPUTS ?X3 ?X4) (?X6 # ?X7 ??* ?X8)) =>
      SolveINPUTS_direct_rinP
  end.

Ltac SolveOROUTPUTS :=
  match goal with
  |  |- (sat (OR ?X1 ?X2) (?X3 # ?X4)) => first
  [ apply intro_left_OR; SolveOROUTPUTS
  | apply intro_right_OR; SolveOROUTPUTS ]
  |  |- (sat (OUTPUTS ?X3 ?X4 ?X5) (?X6 # ?X7)) => SolveOUTPUTS
  | _ => fail
  end.