(*Set Warnings "-notation-overridden,-parsing".*)
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Import Coq.omega.Omega.
Require Import Coq.Sets.Multiset.
Require Import Coq.Lists.ListSet.
Require Import Coq.Strings.String.
(* Require Import Coq.Structures.Orders.
Require Import Ascii. *)
Require Import Coq.Classes.RelationClasses.
Open Scope string_scope.


Import ListNotations.

Set Nested Proofs Allowed. 

Set Implicit Arguments.
Scheme Equality for list.
 
(** 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 

**)


(** ==========================
  *** 0: General House Keeping
   =========================== *)

Fixpoint trueForAll {A:Type} (f:A->Prop) (l:list A)  : Prop := 
  match l with
  | [] => True
  | h::ts =>  (f h) /\ (trueForAll f ts)
  end.

Fixpoint btrueForAll {A:Type} (f:A->bool) (l:list A)  : bool := 
  match l with
  | [] => true
  | h::ts =>  andb (f h) (btrueForAll f ts)
  end.

Fixpoint trueForOne {A:Type} (f:A->Prop) (l:list A)  : Prop := 
  match l with
  | [] => True
  | h::ts =>  (f h) \/ (trueForAll f ts)
  end.


Fixpoint btrueForOne {A:Type} (f:A->bool) (l:list A)  : bool := 
  match l with
  | [] => true
  | h::ts =>  orb (f h) (btrueForOne f ts)
  end.

(* normal generic append has been overwritten by the string library *)
Fixpoint appendAny {A:Type} l1 l2 : list A :=
  match l1 with
  | []     => l2
  | h :: t => h :: (appendAny t l2)
  end.

Fixpoint consEnd {A:Type} fs f : (list A) :=
  match fs with
  | []    => [f]
  | h :: t => h :: (consEnd t f)
  end.

Fixpoint lastElement {A:Type} (a:A) (als:list A) : A :=
  match als with
  | []    => a
  | h :: t => lastElement h t
  end.


Fixpoint secondLastElement {A:Type} (a:A) (als:list A) : A :=
  match als with
  | []    => a
  | h::[] => a
  | h1 :: h2 :: t => lastElement h1 (h2::t)
  end.



Fixpoint listWithoutLastElement {A:Type} (als:list A) : list A :=
  match als with
  | []    => []
  | h::[]    => []
  | h :: t => h:: listWithoutLastElement t
  end.


Definition isLastElement {A:Type} (a:A) (als:list A) : Prop :=  (eq a (lastElement a als)).


Lemma listEq : forall {A:Type} (h1:A) h2 ts2 ts1, h1=h2 -> ts2=ts1 -> h1::ts2=h2::ts1.
Proof.
  intros. induction H. induction H0. reflexivity.
Qed.

Lemma listEqHead : forall {A:Type} (h:A) ts2 ts1, ts2=ts1 -> h::ts2=h::ts1.
Proof.
  intros. apply listEq. reflexivity. assumption.
Qed.

Lemma listEqTail : forall {A:Type} (h1:A) h2 ts, h1=h2 -> h1::ts=h2::ts.
Proof.
  intros. apply listEq. assumption. reflexivity. 
Qed.

(* This removes the first matching element in a list, if any *) 
Fixpoint removeElement {A:Type} (eqA:forall a b : A, {a = b} + {a <> b}) (e:A) (l:list A) : list A :=
  match l with
    | [] => []
    | h::ts => if (eqA h e) then ts else (h::(removeElement eqA e ts))
  end.


Inductive prefixList {A:Type} :  (list A) -> (list A) -> Prop := 
  | Empty_PreFix : forall l, prefixList [] l
  | Head_PreFix : forall l1 l2 a, prefixList l1 l2 -> prefixList (a::l1) (a::l2)
  | Next_PreFix : forall l1 l2 a, prefixList l1 l2 -> prefixList l1 (a::l2).


Fixpoint NotIn {A:Type} (a : A) (ls : list A) : Prop :=
  match ls with
    | [] => True
    | h::ts => a <> h /\ NotIn a ts
  end.



Fixpoint noCommonElements {A:Type} (f1:list A) (f2:list A): Prop :=
 match f1 with
  | []       => True
  | f11::f1s => NotIn f11 f2 /\ noCommonElements f1s f2
end.


Fixpoint termsDoNotAppear {A:Type} (f1: list A) (f2:list (list A)): Prop :=
 match f2 with
  | []       => True
  | f21::f2s => noCommonElements f1 f21 /\ termsDoNotAppear f1 f2s
end.


Fixpoint someCommonElements {A:Type} (f1:list A) (f2:list A): Prop :=
 match f1 with
  | []       => False
  | f11::f1s => In f11 f2 \/ someCommonElements f1s f2
end.

Fixpoint mapFunction {A:Type} {B:Type}  (f:A -> B) (als:list A) : (list B) :=
  match als with
    | []    => []
    | h::ts => (f h)::(mapFunction f ts)
  end.

Fixpoint mapListFunction {A:Type} {B:Type}  (f:A -> (list B)) (als:list A) : (list B) :=
  match als with
    | []    => []
    | h::ts => appendAny (f h) (mapListFunction f ts)
  end.




Inductive orderedSubList {A:Type} : (list A) -> (list A) -> Prop :=
 | Empty_O_SubList : forall l, orderedSubList [] l
 | Same_O_SubList  : forall l1 l2 h1 h2, orderedSubList l1 l2 -> orderedSubList (h1::l1) (h2::l2)
 | Next_O_SubList  : forall (l1:list A) l2 h, orderedSubList l1 l2 -> orderedSubList l1 (h::l2).

Lemma idIsOrderedSublist : forall {A:Type} (rl:list A), orderedSubList rl rl.
Proof.
  induction rl.
  + apply Empty_O_SubList.
  + apply Same_O_SubList. assumption.
Qed.