Require Import Terms.
Require Import Misc.
Require Omega.
Require Import GenericTactics.
Require Import Inverse_Image.
Require Import Contexts.
Require Import Relation_Operators.
Require Import ZArith.
Require Import Wf_nat.

Section weightterms.
Definition weight_sc c := match c with
  | KM => 1
  | KEK => 2
  | P => 3
  | KEK2 => 4
  | EXP1 => 5
end.

Definition weight_pc c := match c with
  | DATA => 6
  | PIN => 7
  | ID => 8
  | IMP => 9
  | K3 => 10
  | ACC => 11
  | KP => 12
  | EXP => 13
end
.

Definition term_head t := match t with
  | Zero => 0
  | PC c => 1
  | SC c => 2
  | E t1 t2 => 3
  | Xor t1 t2 => 5 (* Xor has the maximum weight *)
  | Hash t1 t2 => 4
end.

Lemma weight_pc_inj : forall c1 c2, weight_pc c1 = weight_pc c2 -> c1 = c2.
induction c1;induction c2;simpl;intro H;try discriminate H;apply refl_equal.
Qed.

Lemma weight_sc_inj : forall c1 c2, weight_sc c1 = weight_sc c2 -> c1 = c2.
induction c1;induction c2;simpl;intro H;try discriminate H;apply refl_equal.
Qed.

Fixpoint weight_term (t:term) : nat := match t with
  | Zero => 1
  | PC c => 2
  | SC c => 3
  | E t1 t2 => 1 + weight_term t1 + weight_term t2
  | Xor t1 t2 => 2 + weight_term t1 + weight_term t2
  | Hash t1 t2 => 1 + weight_term t1 + weight_term t2
end.

Lemma weight_term_gt_0 : forall t, (weight_term t > 0).
intro t; case t;simpl;intros;try omega.
Qed. 

Definition lt_weight_term t1 t2 := weight_term t1 < weight_term t2.

Remark lt_w_wf : well_founded lt_weight_term.
unfold lt_weight_term.
apply (Inverse_Image.wf_inverse_image term nat).
apply lt_wf.
Qed.

Definition weight_le n := fun t => weight_term t <= n.

Open Local Scope Z_scope.

Definition index_sc (c : Z) := match c with
  | 0 => KM
  | 1 => KEK
  | 2 => P
  | 3 => KEK2
  | 4 => EXP1
  | _ => KM
end.

Remark finite_sc : finite secret_const (fun c => True).
apply finite_n_imp_finite with 6%Z.
apply F with index_sc.
intros c H.
exists ((Z_of_nat (weight_sc c)) - 1).
case c; simpl;unfold Pminus;simpl;intuition.
Qed.

Definition index_pc c := match c with
  | 6 => DATA
  | 7 => PIN
  | 8 => ID
  | 9 => IMP
  | 10 => K3
  | 11 => ACC
  | 12 => KP
  | 13 => EXP
  | _ => EXP
end.

Remark finite_pc : finite public_const (fun c => True).
apply finite_n_imp_finite with 14%Z.
apply F with index_pc.
intros c H.
exists (Z_of_nat (weight_pc c)).
case c;simpl;intuition.
Qed.

Remark finite_zero : finite term (fun t => t = Zero).
apply finite_n_imp_finite with 1.
apply F with (fun (_:Z) => Zero).
intros.
exists 0.
intuition.
Qed.

Definition u := Misc.union term.
Definition img2 := image2 term term term.
Definition consts := u (image public_const term (fun _ => True) PC)
  (u (image secret_const term (fun _ => True) SC) (fun t => t = Zero)).

Remark finite_consts : finite term consts.
unfold consts; unfold u.
repeat apply finite_union ; try apply finite_img.
  apply finite_pc.
  apply finite_sc.
  apply finite_zero.
Qed.

Definition term_iterator (P : term -> Prop) := 
  (u consts (u (img2 P P E) (u (img2 P P Xor) (img2 P P Hash)))).

Remark le_finite_ind : forall (P : term -> Prop),
  finite term P ->
    finite term (term_iterator P)
.
intros P HP.
unfold term_iterator.
repeat apply (finite_union term);try apply finite_consts;
apply (finite_img2 term term term);try assumption.
Qed.

Lemma le_finite : forall n, finite term (weight_le n).
induction n.
  apply finite_n_imp_finite with 0.
  apply F with (fun (_:Z) => Zero).
  unfold weight_le; intros x H.
  generalize (weight_term_gt_0 x).
  repeat PROGRESS0.
assert (finite term (term_iterator (weight_le n))).
  apply le_finite_ind;assumption.
apply finite_incl with (term_iterator (weight_le n));trivial.
unfold weight_le; unfold term_iterator;unfold consts ; unfold u; unfold img2; unfold Misc.union ; unfold image2;unfold image.
intros t.
case t;simpl;
try (intros ; assert (weight_term t0 <= n)%nat ; [omega | idtac];
     assert (weight_term t1 <= n)%nat ; [omega | idtac]);
intuition eauto.
Qed.

Lemma finite_wf_le : forall n, finite_wf term (weight_le n).
intro n.
apply finite_imp_finite_wf.
exact (le_finite n).
Qed.
(*
Lemma lt_weight_embedding : forall t c, context c -> lt_weight_term t (c t) \/ t = c t.
unfold lt_weight_term.
induction 1; auto;
elim H0 ; simpl; intuition;
try match goal with [ H : ?t = ?c ?t |- _ ] => rewrite <- H ;clear H end;
auto with * .
Qed.
*)
End weightterms.