Require Export SMwell_formed_V_def.
Require Export SMtactics.

Lemma same_iff_true :
  forall {A} (a : A), (a = a) <-> True.
Proof.
  introv; split; auto.
Qed.
Hint Rewrite @same_iff_true : prop.

Lemma true_equal_false_as_false :
  (true = false) <-> False.
Proof.
  introv; split; tcsp.
Qed.
Hint Rewrite @true_equal_false_as_false : prop.

Lemma false_equal_true_as_false :
  (false = true) <-> False.
Proof.
  introv; split; tcsp.
Qed.
Hint Rewrite @false_equal_true_as_false : prop.

Lemma false_iff_as_not :
  forall P, (False <-> P) <-> ~P.
Proof.
  introv; split; intro h; tcsp.
  - intro q; apply h; auto.
  - split; intro q; tcsp.
Qed.
Hint Rewrite @false_iff_as_not : prop.

Ltac simple_unfold :=
  match goal with
  | [ |- ?x ] => unfold x
  | [ |- ?x = _ ] => unfold x
  | [ |- ?x _ = _ ] => unfold x
  | [ |- ?x _ _ = _ ] => unfold x
  | [ |- ?x _ _ _ = _ ] => unfold x
  | [ |- ?x _ _ _ _ = _ ] => unfold x
  | [ |- ?x _ _ _ _ _ = _ ] => unfold x
  | [ |- ?x _ _ _ _ _ _ = _ ] => unfold x
  | [ |- ?x _ _ _ _ _ _ _ = _ ] => unfold x
  end.

Ltac unf_smash_sm :=
  intros; repeat simple_unfold; simpl; smash_sm.

Ltac sm_destruct_one :=
  match goal with
  | [ H : sm_bare_signed_msg_sing            |- _ ] => destruct H
  | [ H : sm_bare_signed_msg_cons            |- _ ] => destruct H
  | [ H : sm_bare_msg_signed                 |- _ ] => destruct H
  | [ H : sm_bare_msg_result                 |- _ ] => destruct H

  | [ H : sm_msg_init                        |- _ ] => destruct H
  | [ H : sm_msg_signed                      |- _ ] => destruct H
  | [ H : sm_msg_result                      |- _ ] => destruct H

  | [ H : well_formed_V                      |- _ ] => inversion H as [h1 h2]

  end.

Ltac sm_destruct_all :=
  repeat sm_destruct_one; simpl in *; auto.

Ltac sm_brute_force_step :=
  first
    [complete tcsp
    |progress GC
    |progress autorewrite with sm list prop in *
    |progress sm_destruct_all
  (*  |progress sm_unfold_all *)
    |progress ginv
    |progress smash_sm
    ].

Ltac sm_brute_force :=
  intros;
  repeat sm_brute_force_step.
