(** 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 Sec3_SubstitutionDefs. (** =================================== *** 4: Ground terms and rule instances =================================== **) (* This section defines what a ground instance of a rule, and facts, are *) (* This is used by the "run" prediciate in the next section *) (** Ground Defs, these might be better as Props, rather than bools I'm not sure at this point, we can always change these to Props later **) Fixpoint groundBaseTerm (ts:baseTerm) : Prop := match ts with | Var v => False | _ => True end. Definition groundBaseTerms : baseTerms -> Prop := trueForAll groundBaseTerm. Fixpoint groundTerm (t:term) : Prop := match t with | Func f ts => groundBaseTerms ts | Bterm (Name (Pub n)) => True | Bterm (Name (Fresh_S n)) => True | Bterm (Name (Fresh_P n)) => True | _ => False end. Fixpoint groundTerms (ts:terms) : Prop := match ts with | t::ts => groundTerm t /\ groundTerms ts | [] => True end. Fixpoint groundFact (f:fact) : Prop := match f with | IN ts => groundTerms ts | OUT ts => groundTerms ts | K ts => groundTerms ts | STATE n ts => groundTerms ts | FR_P fn => True end. Fixpoint groundFacts (fs:facts) : Prop := match fs with | f::fs => groundFact f /\ groundFacts fs | [] => True end. Definition groundActionLabel (al:actionLabel) : Prop := match al with | ActLabel n ts => groundTerms ts end. Fixpoint groundBasicLabel (lb:list actionLabel) : Prop := match lb with | al::als => groundActionLabel al /\ groundBasicLabel als | [] => True end. Definition groundLoggedLabel (lg:actionLabel) (lb:list actionLabel) : Prop := groundActionLabel lg /\ groundBasicLabel lb. Definition groundLoggedSIDLabel (t:baseTerm) (lg:actionLabel) (lb:list actionLabel) : Prop := groundBaseTerm t /\ groundActionLabel lg /\ groundBasicLabel lb. Definition groundLabel (lb:label) : Prop := match lb with | BasicLabel ls => groundBasicLabel ls | LoggedLabel lg ls => groundLoggedLabel lg ls | LoggedSIDLabel t lg ls => groundLoggedSIDLabel t lg ls end. Definition groundRule (r:rule) : Prop := match r with | RuleProto f1 l f2 => groundFacts f1 /\ groundFacts f2 /\ groundLabel l | RuleSetup f1 l f2 => groundFacts f1 /\ groundFacts f2 /\ groundLabel l end. (* Ginsts is a function unsed in Tamarin generate all possible ground instances of a rule set. *) Inductive ginst : rule -> rule -> Prop := | Ginst : forall r1 r2, (exists sigma, (applySubRule sigma r2) = r1) /\ (groundRule r1) -> ginst r1 r2. Inductive ginsts : rule -> ruleList -> Prop := | GinstHead : forall r1 r2 rs, (ginst r1 r2) -> ginsts r1 (r2::rs) | GinstTail : forall r1 r2 rs, (ginsts r1 rs) -> ginsts r1 (r2::rs). (* GinstsWithSigma is a function unsed in Tamarin generate a specific ground instance of a rule set using substitution sigma. *) Inductive ginstWithSigma : rule -> substitution -> rule -> Prop := | GinstSigma : forall r1 r2 sigma, (applySubRule sigma r2) = r1 /\ groundRule r1 -> ginstWithSigma r1 sigma r2. Inductive ginstsWithSigma : rule -> substitution -> ruleList -> Prop := | GinstHeadSigma : forall r1 r2 rs sigma, (ginstWithSigma r1 sigma r2) -> ginstsWithSigma r1 sigma (r2::rs) | GinstTailSigma : forall r1 r2 rs sigma, (ginstsWithSigma r1 sigma rs) -> ginstsWithSigma r1 sigma (r2::rs). Lemma composeSubstBaseTerm : forall bt (sigma1:substitution) (sigma2:substitution), groundBaseTerm (applySubBaseTerm sigma1 bt) -> groundBaseTerm (applySubBaseTerm (compose sigma1 sigma2) bt). Proof. intros. destruct bt. - unfold applySubBaseTerm. unfold applySubBaseTerm in H. unfold compose. destruct (beq_name (sigma1 v) null) eqn:D1. + inversion H. + rewrite D1. reflexivity. - reflexivity. Qed. Lemma composeSubstBaseTerms : forall bt (sigma1:substitution) (sigma2:substitution), groundBaseTerms (applySubBaseTerms sigma1 bt) -> groundBaseTerms (applySubBaseTerms (compose sigma1 sigma2) bt). Proof. intros. induction bt. + reflexivity. + simpl. unfold groundBaseTerms. simpl. split. - inversion H. apply composeSubstBaseTerm. apply H0. - apply IHbt. unfold groundBaseTerms in H. simpl in H. destruct H. apply H0. Qed. Lemma composeSubstGroundTerm : forall tm (sigma1:substitution) (sigma2:substitution), groundTerm (applySubTerm sigma1 tm) -> groundTerm (applySubTerm (compose sigma1 sigma2) tm). Proof. intros. induction tm. + simpl. eapply composeSubstBaseTerms. simpl in H. simpl. auto. + destruct b. - unfold applySubTerm in H. unfold applySubBaseTerm in H. unfold groundTerm in H. destruct (beq_name (sigma1 v) null) eqn:D1. * inversion H. * unfold applySubTerm. unfold applySubBaseTerm. unfold groundTerm. unfold compose. rewrite D1. rewrite D1. apply H. - unfold applySubTerm. unfold applySubBaseTerm. unfold groundTerm. destruct n0; reflexivity. Qed. Lemma composeSubstGroundTerms : forall tms (sigma1:substitution) (sigma2:substitution), groundTerms (applySubTerms sigma1 tms) -> groundTerms (applySubTerms (compose sigma1 sigma2) tms). Proof. intros. induction tms. + reflexivity. + simpl. inversion H. split. - apply composeSubstGroundTerm. apply H0. - apply IHtms. apply H1. Qed. Lemma composeSubstGroundAL : forall al (sigma1:substitution) (sigma2:substitution), groundActionLabel (applySubActionLabel sigma1 al) -> groundActionLabel (applySubActionLabel (compose sigma1 sigma2) al). Proof. intros. induction al. simpl. apply composeSubstGroundTerms. unfold groundActionLabel in H. simpl in H. assumption. Qed. Lemma composeSubstGroundBasicLabel : forall l (sigma1:substitution) (sigma2:substitution), groundBasicLabel (map ( applySubActionLabel sigma1) l) -> groundBasicLabel (map (applySubActionLabel (compose sigma1 sigma2)) l). Proof. intros. induction l. + simpl. reflexivity. + simpl. split. unfold groundLabel in H. simpl in H. destruct H. - apply composeSubstGroundAL. auto. - apply IHl. inversion H. apply H1. Qed. Lemma composeSubstGroundLoggedLabel : forall al ls (sigma1:substitution) (sigma2:substitution), groundLoggedLabel (applySubActionLabel sigma1 al) (map (applySubActionLabel sigma1) ls) -> groundLoggedLabel (applySubActionLabel (compose sigma1 sigma2) al) (map (applySubActionLabel (compose sigma1 sigma2)) ls). Proof. intros. unfold groundLoggedLabel in H. inversion H. unfold groundLoggedLabel. split. - apply composeSubstGroundAL. apply H0. - induction ls. + simpl. reflexivity. + simpl. inversion H1. split. * apply composeSubstGroundAL. apply H2. * apply IHls. split. -- apply H0. -- apply H3. -- apply H3. Qed. Lemma composeSubstGroundLoggedSIDLabel : forall al ls t (sigma1:substitution) (sigma2:substitution), groundLoggedSIDLabel (applySubBaseTerm sigma1 t) (applySubActionLabel sigma1 al) (map (applySubActionLabel sigma1) ls) -> groundLoggedSIDLabel (applySubBaseTerm (compose sigma1 sigma2) t) (applySubActionLabel (compose sigma1 sigma2) al) (map (applySubActionLabel (compose sigma1 sigma2)) ls). Proof. intros. unfold groundLoggedSIDLabel in H. inversion H. inversion H1. unfold groundLoggedSIDLabel. split. - apply composeSubstBaseTerm. apply H0. - split. + apply composeSubstGroundAL. apply H2. + apply composeSubstGroundBasicLabel. apply H3. Qed. Lemma composeSubstGroundLabel : forall l (sigma1:substitution) (sigma2:substitution), groundLabel (applySubLabel sigma1 l) -> groundLabel (applySubLabel (compose sigma1 sigma2) l). Proof. intros. induction l as [ls|al ls|ls]. - simpl. apply composeSubstGroundBasicLabel. unfold groundLabel in H. simpl in H. assumption. - unfold groundLabel. simpl. apply composeSubstGroundLoggedLabel. unfold groundLabel in H. simpl in H. apply H. - unfold groundLabel. simpl. apply composeSubstGroundLoggedSIDLabel. unfold groundLabel in H. simpl in H. apply H. Qed.