(** Contents :

   0: General House Keeping

   1: Syntax definitions 

   2: Equality, membership and extraction functions for the syntax
      2A: Equality functions
      2B: Membership functions
      2C: Extraction of submembers functions


   3: Substitution

   4: Ground terms and rules instances

   5: Tamarin Reduction

   6: Example

   7: Definitions from Chapter 5 of the thesis


   8: Tests and Definitions for Well formedness 
       8A: Functions to test no or One Input / Output in facts
       8B: Definitions on Variables and Terms  for Equivalence proof 
       8C: Well formedness definitions 
       
    9: Some useful lemmas on well formedness

   10: Definitions from Chapter 6 of the thesis
      10A: Types of Facts allowed in the system  

   11: Props and Theorems from Chapter 6 

**)


Load Sec2_EqualityMemberships.

(** ===================== 
  *** 3: Substitution
 ===================== **)

(** This section defines the mechanics of how Substitution works. 

 based on SOFTWARE FOUNDATIONS: 
https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html **)

Definition substitution := variable -> name.

Definition substitutions := list substitution.

Definition null : name := Pub "null".

Definition subs_empty  : substitution :=
  (fun _ => null).

Definition update (sigma : substitution)
                   (v : variable ) (n : name)  :=
  fun x' => if beq_string v x' then n else sigma x'.

Notation "v '!->' n" := (update subs_empty v n) (at level 100).
Notation "v '!->' n ';' sigma" := (update sigma v n)
                              (at level 100, n at next level, right associativity).

Definition compose (sigma1 : substitution) (sigma2 : substitution) : variable -> name :=
  fun v => if (beq_name (sigma1 v) null) then (sigma2 v) else (sigma1 v).  

Definition substsAgree (sigma1 : substitution) (sigma2 : substitution) : Prop :=
  forall x, sigma1 x = null \/ sigma2 x = null \/ sigma1 x=sigma2 x.

Lemma agreeSubstComposeOrder : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall x, compose sigma1 sigma2 x = compose sigma2 sigma1 x.
Proof.
  intros. unfold compose. 
  destruct (beq_name (sigma1 x0) null) eqn:D1; destruct (beq_name (sigma2 x0) null) eqn:D2.
  + apply beq_name_EQ in D1. apply beq_name_EQ in D2. rewrite D1. rewrite D2. reflexivity. 
  + reflexivity.
  + reflexivity.
  + unfold substsAgree in H. destruct (H x0).
   - rewrite H0 in D1. inversion D1.
   - inversion H0.
     * rewrite H1 in D2. inversion D2.
     * assumption.
Qed.

Definition exampleSubs := "ltkA" !-> Fresh_S "ltkA"; subs_empty.

Fixpoint applySubBaseTerm (sigma:substitution) (t:baseTerm) : baseTerm :=
  match t with
  | Var v  =>  if (beq_name (sigma v)  null) then (Var v) else Name (sigma v)
  | Name n =>  Name n
  end.

Definition applySubBaseTerms (sigma:substitution) (ts:baseTerms) : baseTerms 
     := map (applySubBaseTerm sigma) ts.

Fixpoint applySubTerm (sigma:substitution) (t:term) : term :=
  match t with
  | Func f bts => Func f (applySubBaseTerms sigma bts)
  | Bterm bt => Bterm (applySubBaseTerm sigma bt)
  end.

Definition applySubTerms  : substitution -> terms -> terms 
     := fun sigma => map (applySubTerm sigma).

Fixpoint applySubActionLabel (sigma:substitution) (lb:actionLabel) : actionLabel :=
  match lb with
   | ActLabel n ts => ActLabel n (applySubTerms sigma ts)
  end.

Definition applySubLabel (sigma:substitution) (lb:label) : label :=
  match lb with
    | BasicLabel ll     => BasicLabel (map ( applySubActionLabel sigma) ll) 
    | LoggedLabel lg ll => LoggedLabel (applySubActionLabel sigma lg) (map (applySubActionLabel sigma) ll) 
    | LoggedSIDLabel t lg ll => LoggedSIDLabel (applySubBaseTerm sigma t)(applySubActionLabel sigma lg) (map (applySubActionLabel sigma) ll) 
  end.

Fixpoint applySubFact (sigma:substitution) (f:fact) : fact :=
match f with
  | IN terms  => IN (applySubTerms sigma terms)
  | OUT terms  => OUT (applySubTerms sigma terms)
  | K terms  => K (applySubTerms sigma terms)
  | STATE name terms  => STATE  name (applySubTerms sigma terms)
  | FR_P freshName => FR_P (applySubBaseTerm sigma freshName)
  end.

Definition applySubFacts  : substitution -> facts -> facts 
     := fun sigma => map (applySubFact sigma).

Fixpoint applySubRule (sigma:substitution) (r:rule) : rule :=
match r with
  | RuleSetup f1 l f2 => RuleSetup (applySubFacts sigma f1) (applySubLabel sigma l)  (applySubFacts sigma f2)
  | RuleProto f1 l f2 => RuleProto (applySubFacts sigma f1) (applySubLabel sigma l)  (applySubFacts sigma f2)
end.


Definition applySubRuleList : substitution ->  ruleList -> ruleList := fun sigma => map (applySubRule sigma).

Definition applySubRuleLists : substitution ->  list ruleList -> list ruleList := fun sigma => map (applySubRuleList sigma).

Definition applySubTrace : substitution ->  trace -> trace := fun sigma => map (applySubLabel sigma).

Definition applySubTraces : substitution ->  list trace -> list trace := fun sigma => map (applySubTrace sigma).


Lemma agreeSubstComposeOrderBaseTerm : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall bt, applySubBaseTerm (compose sigma1 sigma2) bt 
                                            = applySubBaseTerm (compose sigma2 sigma1) bt.
Proof.
  intros. destruct bt.
  + simpl. unfold compose. destruct (beq_name (sigma1 v) null) eqn:D1; destruct (beq_name (sigma2 v) null) eqn:D2.
    - rewrite D1. reflexivity.
    - rewrite D2. reflexivity.
    - rewrite D1. reflexivity.
    - rewrite D1. rewrite D2.  unfold substsAgree in H. destruct (H v).
      * rewrite H0 in D1. inversion D1.
      * inversion H0.
        ++ rewrite H1 in D2.  inversion D2.
        ++ rewrite H1.  reflexivity. 
   +  reflexivity. 
Qed.

Lemma agreeSubstComposeOrderBaseTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall bt, applySubBaseTerms (compose sigma1 sigma2) bt 
                                            = applySubBaseTerms (compose sigma2 sigma1) bt.
Proof.
  intros. induction bt.
  + reflexivity. 
  + simpl. apply listEq. apply agreeSubstComposeOrderBaseTerm. assumption. apply IHbt.
  Qed.

Lemma agreeSubstComposeOrderTerm : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerm (compose sigma1 sigma2) tm 
                                            = applySubTerm (compose sigma2 sigma1) tm.
Proof.
  intros. induction tm.
  + simpl. apply f_equal. apply agreeSubstComposeOrderBaseTerms. assumption.
  + simpl. apply f_equal. apply agreeSubstComposeOrderBaseTerm. assumption.
Qed.

Lemma agreeSubstComposeOrderTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerms (compose sigma1 sigma2) tm 
                                            = applySubTerms (compose sigma2 sigma1) tm.
Proof.
  intros. induction tm.
  + reflexivity.
  + simpl. apply listEq. 
    - apply agreeSubstComposeOrderTerm. assumption.
    - assumption.
Qed.

Lemma agreeSubstComposeOrderActionLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall al, applySubActionLabel (compose sigma1 sigma2) al 
                                            = applySubActionLabel (compose sigma2 sigma1) al.
Proof. 
 intros. induction al. induction t.
  + reflexivity.
  + simpl. apply f_equal. apply listEq.
    - apply agreeSubstComposeOrderTerm. assumption.
    - apply agreeSubstComposeOrderTerms. assumption.
Qed.


Lemma agreeSubstComposeOrderLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall l, applySubLabel (compose sigma1 sigma2) l 
                                            = applySubLabel (compose sigma2 sigma1) l.
Proof.
 intros. induction l as [ls|al ls|b al ls].
  +  induction ls.
    * reflexivity.
    * simpl. apply f_equal. apply listEq.
      ** apply agreeSubstComposeOrderActionLabel.  assumption.
      **  inversion IHls. rewrite H1. reflexivity.
  + induction ls.
    * simpl. apply agreeSubstComposeOrderActionLabel with (al:=al) in H.
      rewrite H. reflexivity.
    * simpl.  assert (HA := H).
      apply agreeSubstComposeOrderActionLabel with (al:=al) in H. 
      rewrite H. apply f_equal. apply listEq.
      ** apply agreeSubstComposeOrderActionLabel.  assumption.
      ** inversion IHls.  rewrite H2. reflexivity.
  + induction ls.
    * simpl. assert (HA := H). apply agreeSubstComposeOrderActionLabel with (al:=al) in H.
      rewrite H. apply agreeSubstComposeOrderBaseTerm with (bt:=b) in HA.
      rewrite HA. reflexivity.
    * simpl in IHls. inversion IHls. simpl. assert (HA := H). assert (HB := H). assert (HC := H). 
      apply agreeSubstComposeOrderActionLabel with (al:=al) in H.
      apply agreeSubstComposeOrderActionLabel with (al:=a) in HA.
      rewrite H. rewrite HA. apply agreeSubstComposeOrderBaseTerm with (bt:=b) in HB.
      rewrite HB. apply f_equal. apply listEq.
      -- reflexivity.
      -- apply H3.
Qed.

Lemma agreeSubstComposeOrderTrace : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall t, applySubTrace (compose sigma1 sigma2) t 
                                            = applySubTrace (compose sigma2 sigma1) t.
Proof.
  intros. induction t.
  + reflexivity.
  + simpl. apply listEq.
    - apply agreeSubstComposeOrderLabel. assumption.
    - apply IHt.
Qed.