Library LanguageFoundations

This file was written by Colm Bhandal, PhD student, Foundations and Methods group, School of Computer Science and Statistics, Trinity College, Dublin, Ireland.

Require Import ComhCoq.Extras.LibTactics.

This file lays down the foundation for the software language file by defining things like expressions and evaluation of expressions.

Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Export Relations.
Require Export Lists.ListSet.
Require Export Reals.
Require Export List.
Require Export Logic.FunctionalExtensionality.
Require Import ComhCoq.ComhBasics.

Open Scope nat_scope.

A countably infinite set of variables indexed by natural numbers.

Inductive Var : Type:=
| var : nat -> Var.

Lemma eqDecVar : eqDec Var.

BaseType type elements are either a mode, a time, a position, a distance or a delay. We use coercions to reduce constructor verbosity.

Equality on the base type is decidable.

Lemma eqDecBase : eqDec BaseType.

A simple expression language over the base types.

Equality is decidable on expressions.

Lemma eqDecExp : eqDec Exp.

A set of channels.

Equality on channels is decidable.

Lemma eqDecChannel : eqDec Channel.

A substitution is a mapping from variables to expressions.

Definition Subst := Var -> Exp.

The id substitution simply lifts every variable to an expression i.e. it maps every variable to itself, with the eVar constructor as a wrapper.

Definition idSubst (v : Var) : Exp :=
  (eVar v).

Fixpoint subExp (s : Subst) (e : Exp) : Exp :=
  match e with
  | eVar v => s v
  | eBase b => eBase b
  | eSubtract e1 e2 => eSubtract (subExp s e1) (subExp s e2)
  | eAdd e1 e2 => eAdd (subExp s e1) (subExp s e2)
  | eMult e1 e2 => eMult (subExp s e1) (subExp s e2)
  | eWaitTime e1 e2 => eWaitTime (subExp s e1) (subExp s e2)
  | ePeriod e' => ePeriod (subExp s e')
  | eDist e1 e2 => eDist (subExp s e1) (subExp s e2)
  | eFailSafeSucc e1 => eFailSafeSucc (subExp s e1)
  end.

Lemma lt_neq_nat : forall n m : nat,
  n < m -> n <> m.

Lemma natDec : forall n m : nat,
  {n = m} + {n <> m}.

Lemma varEqDec : forall x y : Var,
  {x = y} + {x <> y}.

Definition varEq (v1 v2 : Var) : bool :=
  match (varEqDec v1 v2) with
  | left _ => true
  | right _ => false
  end.

Definition update {X : Type} (f : Var -> X) (v : Var) (x : X) : (Var -> X) :=
  fun v' => if (varEq v v') then x else (f v').

Fixpoint listsToSub (lv : list Var) (lex : list Exp) : Subst :=
  match lv , lex with
  | v :: lv' , e :: lex' => (update (listsToSub lv' lex') v e)
  | [] , _ :: _ => idSubst
  | _ , [] => idSubst
  end.

Definition listSub (s : Subst) (l : list Exp) : list Exp :=
  map (subExp s) l.

Fixpoint inVarList (v : Var) (lv : list Var) : bool :=
  match lv with
  | [] => false
  | v' :: lv' => if (varEq v v') then true else (inVarList v lv')
  end.

Definition resetSub (s : Subst) (lv : list Var) (v : Var) : Exp :=
  match (inVarList v lv) with
  | true => eVar v
  | false => s v
  end.

Open Scope R_scope.

Evaluates certain base values (Delay, Time, Distance, Nonneg) to nonnegative reals. Used to "normalise" the types of things so that +, - and * can be computed over expressions.

Inductive evalBaseNonneg : BaseType -> nonnegreal -> Prop :=
  | ebnDel r : evalBaseNonneg (baseDelay (mkDelay r)) (posToNonneg r)
  | ebnTime r : evalBaseNonneg (baseTime (mkTime r)) r
  | ebnDistance r : evalBaseNonneg (baseDistance (mkDistance r)) r
  | ebnNonneg r : evalBaseNonneg (baseNonneg r) r.
Notation "b \_/ r" := (evalBaseNonneg b r) (at level 45).

Lemma evalBaseNonneg_unique b r1 r2 :
  b \_/ r1 -> b \_/ r2 -> r1 = r2.

Definition evalBaseNonnegFun (b : BaseType) : option nonnegreal :=
  match b with
  | baseDelay (mkDelay r) => Some (posToNonneg r)
  | baseTime (mkTime r) => Some r
  | baseDistance (mkDistance r) => Some r
  | baseNonneg r => Some r
  | _ => None
  end.

Lemma evalBaseNonneg_rel_fun b r :
  b \_/ r -> evalBaseNonnegFun b = Some r.

Lemma evalBaseNonneg_fun_rel b r :
  evalBaseNonnegFun b = Some r -> b \_/ r.

Inductive evalExp : Exp -> BaseType -> Prop :=
  | evalBase : forall b : BaseType, evalExp (eBase b) b
  | evalSub : forall (e1 e2 : Exp) (b1 b2 : BaseType) (r1 r2 : nonnegreal),
  evalExp e1 b1 -> evalExp e2 b2 -> b1 \_/ r1 -> b2 \_/ r2 ->
  evalExp (eSubtract e1 e2) (r1 -nn- r2)
  | evalAdd : forall (e1 e2 : Exp) (b1 b2 : BaseType) (r1 r2 : nonnegreal),
  evalExp e1 b1 -> evalExp e2 b2 -> b1 \_/ r1 -> b2 \_/ r2 ->
  evalExp (eAdd e1 e2) (r1 +nn+ r2)
  | evalMult : forall (e1 e2 : Exp) (b1 b2 : BaseType) (r1 r2 : nonnegreal),
  evalExp e1 b1 -> evalExp e2 b2 -> b1 \_/ r1 -> b2 \_/ r2 ->
  evalExp (eMult e1 e2) (r1 *nn* r2)
  | evalWait : forall (e1 e2 : Exp) (m1 : Mode) (m2 : Mode)
  (p : m1 -mtr-> m2), evalExp e1 m1 -> evalExp e2 m2 ->
  evalExp (eWaitTime e1 e2) (waitTime m1 m2 p)
  | evalPeriod : forall (e : Exp) (m : Mode), evalExp e m ->
  evalExp (ePeriod e) (period m)
  | evalDist : forall (e1 e2 : Exp) (p1 p2 : Position),
  evalExp e1 p1 -> evalExp e2 p2 ->
  evalExp (eDist e1 e2) (mkDistance (dist2d p1 p2))
  | evalFailSafeSucc : forall (e : Exp) (m : Mode),
  evalExp e m -> evalExp (eFailSafeSucc e) (failSafeSucc m).
Notation "e |_| b" := (evalExp e b) (at level 50).

Option map function for two arguments.

Definition optionMap2 {A B C : Type} (f : A -> B -> C)
  (a : option A) (b : option B) : option C :=
  match (option_map f a) with
  | Some g => option_map g b
  | None => None
  end.

A functional encoding of the evaluation relation as a partial function. The proof that the two coincide is a separate issue! This function, due to its dealings with the horrid option type, is quite ugly and hard to understand, but its advantage is its computability. Once it is linked to the relation via proofs, it can be left as an under the hood engine that "computes" the relation.

Fixpoint evalExpFun (e : Exp) : option BaseType :=
  match e with
  | eVar v => None
  | eBase b => Some b
  | eSubtract e1 e2 =>
    match (evalExpFun e1), (evalExpFun e2) with
    | Some b1, Some b2 =>
      match (evalBaseNonnegFun b1), (evalBaseNonnegFun b2) with
      | Some r1, Some r2 => Some (baseNonneg (r1 -nn- r2))
      | _, _ => None
      end
    | _, _ => None
    end
  | eAdd e1 e2 =>
    match (evalExpFun e1), (evalExpFun e2) with
    | Some b1, Some b2 =>
      match (evalBaseNonnegFun b1), (evalBaseNonnegFun b2) with
      | Some r1, Some r2 => Some (baseNonneg (r1 +nn+ r2))
      | _, _ => None
      end
    | _, _ => None
    end
  | eMult e1 e2 =>
    match (evalExpFun e1), (evalExpFun e2) with
    | Some b1, Some b2 =>
      match (evalBaseNonnegFun b1), (evalBaseNonnegFun b2) with
      | Some r1, Some r2 => Some (baseNonneg (r1 *nn* r2))
      | _, _ => None
      end
    | _, _ => None
    end

  | eWaitTime e1 e2 =>
    match (evalExpFun e1), (evalExpFun e2) with
    | Some b1, Some b2 =>
      match b1, b2 with
      | baseMode m1, baseMode m2 => option_map baseTime
        (option_map (waitTime m1 m2) (modeTransRelOpt m1 m2))
      | _, _ => None
      end
    | _, _ => None
    end
  | ePeriod e' =>
    match (evalExpFun e') with
    | Some b =>
      match b with
      | baseMode m => Some (baseTime (period m))
      | _ => None
      end
    | None => None
    end
  | eDist e1 e2 =>
    match (evalExpFun e1), (evalExpFun e2) with
    | Some b1, Some b2 =>
      match b1, b2 with
      | basePosition p1, basePosition p2 =>
        Some (baseDistance ((mkDistance (dist2d p1 p2))))
      | _, _ => None
      end
    | _, _ => None
    end
  | eFailSafeSucc e' =>
    match (evalExpFun e') with
    | Some b =>
      match b with
      | baseMode m => Some (baseMode (failSafeSucc m))
      | _ => None
      end
    | None => None
    end
  end.

Ltac evalBaseNonneg_rel_fun_step := match goal with
  [V : _ \_/ _ |- _] => apply evalBaseNonneg_rel_fun in V end.

Ltac evalBaseNonneg_rel_fun_tac := repeat evalBaseNonneg_rel_fun_step.

Ltac evalBaseNonneg_fun_rel_step := match goal with
  [V : Some _ = evalBaseNonnegFun _ |- _] => symmetry in V;
  apply evalBaseNonneg_fun_rel in V end.

Ltac evalBaseNonneg_fun_rel_tac := repeat evalBaseNonneg_fun_rel_step.

If e evaluates to b via the evaluation relation then it does so also by the evalution function.

Theorem evalExpRelFun : forall (e : Exp) (b : BaseType),
evalExp e b -> evalExpFun e = Some b.

If e evaluates to b via the evaluation function then it does so also by the evalution relation.

Theorem evalExpFunRel : forall (e : Exp) (b : BaseType),
evalExpFun e = Some b -> evalExp e b.

Subtract case.

Add case.

Multiply case.

waitTime case.

period case.

distance case.

failSafeSucc case.

A function that tries to evaluate the expression e into a time or fails.

Definition evalExpFunTime (e : Exp) : option Time :=
  match evalExpFun e with
  | Some b => match evalBaseNonnegFun b with
    | Some r => Some (mkTime r)
    | None => None end
  | _ => None
  end.

Inductive evalExpLists : list Exp -> list BaseType -> Prop :=
  | evalElNil : evalExpLists [] []
  | evalElCons : forall (e : Exp) (b : BaseType) (l1 : list Exp) (l2 : list BaseType),
    evalExp e b -> evalExpLists l1 l2 -> evalExpLists (e :: l1) (b :: l2).

Definition listBaselistExp (l1 : list BaseType) : list Exp :=
  map eBase l1.

Inductive BoolExp : Type :=
  | bSufficient : Exp -> Exp -> BoolExp
  | bNot : BoolExp -> BoolExp
  | bEqual : Exp -> Exp -> BoolExp
  | bPossInc : Exp -> Exp -> Exp -> BoolExp.

Equality is decidable on boolean expressions.

Lemma eqDecBoolExp : eqDec BoolExp.

Fixpoint subBoolExp (s : Subst) (b : BoolExp) : BoolExp :=
  match b with
  | bSufficient e1 e2 => bSufficient (subExp s e1) (subExp s e2)
  | bNot b => bNot (subBoolExp s b)
  | bEqual e1 e2 => bEqual (subExp s e1) (subExp s e2)
  | bPossInc e1 e2 e3 => bPossInc (subExp s e1) (subExp s e2) (subExp s e3)
  end.

Inductive evalBoolExp : BoolExp -> bool -> Prop :=
  | bevalSufficient : forall (e1 e2 : Exp) (m : Mode) (r : Distance),
    evalExp e1 m -> evalExp e2 r ->
    evalBoolExp (bSufficient e1 e2) (suffBool m r)
  | bevalNot : forall (e : BoolExp) (b : bool),
    evalBoolExp e b -> evalBoolExp (bNot e) (negb b)
  | bevalEqualTrue : forall (e1 e2 : Exp) (b : BaseType),
    evalExp e1 b -> evalExp e2 b -> evalBoolExp (bEqual e1 e2) true
  | bevalEqualFalse : forall (e1 e2 : Exp) (b1 b2 : BaseType),
    evalExp e1 b1 -> evalExp e2 b2 -> (b1 <> b2) -> evalBoolExp (bEqual e1 e2) false
  | bevalPossInc : forall (e1 e2 e3 : Exp) (m1 m2 : Mode) (d : Distance),
    evalExp e1 m1 -> evalExp e2 m2 -> evalExp e3 d ->
    evalBoolExp (bPossInc e1 e2 e3) (possIncBool m1 m2 d).

A functional definition of the evaluation on boolean expressions.

Fixpoint evalBoolExpFun (b : BoolExp) : option bool :=
  match b with
  | bSufficient e1 e2 =>
    match (evalExpFun e1), (evalExpFun e2) with
    | Some (baseMode m), Some (baseDistance r) => Some (suffBool m r)
    | _, _ => None
    end
  | bNot b => option_map negb (evalBoolExpFun b)
  | bEqual e1 e2 =>
    match (evalExpFun e1), (evalExpFun e2) with
    | Some b1, Some b2 =>
      match eqDecBase b1 b2 with
      | left _ => Some true
      | right _ => Some false
      end
    | _, _ => None
    end
  | bPossInc e1 e2 e3 =>
    match (evalExpFun e1), (evalExpFun e2), (evalExpFun e3) with
    | Some (baseMode m1), Some (baseMode m2), Some (baseDistance d)
      => Some (possIncBool m1 m2 d)
    | _, _, _ => None
    end
  end.

A total function for evaluating boolean expressions, which is identical to the function evalBoolExpFun on well formed inputs, but differs in that it maps ill formed inputs to false instead of None. This function will be used in the semantics since a total

Definition evalBoolExpFunTot (e : BoolExp) : bool :=
  match evalBoolExpFun e with
  | Some b => b
  | None => false
  end.

Sub-Languages syntax notations

Notation "E1 (-) E2" := (eSubtract E1 E2) (at level 30).
Notation "E1 (+) E2" := (eAdd E1 E2) (at level 30).
Notation "E1 (.) E2" := (eMult E1 E2) (at level 29).
Notation "e1 =b= e2" := (bEqual e1 e2) (at level 20).
Notation "| e1 , e2 |" := (eDist e1 e2) (at level 30).
Notation "!~ b" := (bNot b) (at level 25).

The evaluation relation on expressions is a partial function i.e. every expression evaluates to at most one value.

Theorem evalExpUnique : forall (e : Exp) (b1 b2 : BaseType),
  evalExp e b1 -> evalExp e b2 -> b1 = b2.

Theorem evalBoolExpRelFun : forall (e : BoolExp) (b : bool),
  evalBoolExp e b -> evalBoolExpFun e = Some b.

Require Import Bool.

Theorem evalBoolExpFunRel : forall (e : BoolExp) (b : bool),
  evalBoolExpFun e = Some b -> evalBoolExp e b.

bSufficient case

bNot case

Equality case

bPossInc case

The evaluation relation on boolean expressions is a partial function i.e. every expression evaluates to at most one boolean.

Theorem evalBoolExpUnique : forall (e : BoolExp) (b1 b2 : bool),
evalBoolExp e b1 -> evalBoolExp e b2 -> b1 = b2.

If the evaluation of the bool exp function is true, then the total function will evaluate to true, and vice versa.

Theorem evalBoolExpTrueTot : forall (e : BoolExp),
  evalBoolExp e true <-> evalBoolExpFunTot e = true.

Inductive DiscAct :=
  | inAct : Channel -> list BaseType -> DiscAct
  | outAct : Channel -> list BaseType -> DiscAct
  | tauAct : DiscAct.
Notation "c *?" := (inAct c []) (at level 30).
Notation "c *!" := (outAct c []) (at level 30).
Notation "c ;? v" := (inAct c v) (at level 30).
Notation "c ;! v" := (outAct c v) (at level 30).

The complement function converts inputs to outputs and vice versa.

Definition complement (a : DiscAct) : DiscAct :=
  match a with
  | c ;? v => c ;! v
  | c ;! v => c ;? v
  | tauAct => tauAct
  end.
Notation "a ^" := (complement a) (at level 25).

The complement function cancels itself out.

Lemma complementInvol (a : DiscAct) : a^^ = a.

Lemma complementNotTau (a : DiscAct) : a <> tauAct -> a^ <> tauAct.

Lemma evalExpRelFunEquiv (e : Exp) (b : BaseType) :
  evalExp e b <-> evalExpFun e = Some b.

Ltac evalExp_rel_fun_step := match goal with
  [V : _ |_| _ |- _] => apply evalExpRelFun in V end.

Ltac evalExp_rel_fun_tac := repeat evalExp_rel_fun_step.

Ltac evalExp_fun_rel_step := match goal with
  [V : Some _ = evalExpFun _ |- _] => symmetry in V;
  apply evalExpFunRel in V end.

Ltac evalExp_fun_rel_tac := repeat evalExp_fun_rel_step.

Lemma evalExp_evalExpFunTime (e : Exp) (t : Time) :
  evalExp e t -> evalExpFunTime e = Some t.

For every natural number, there is a list of base expressions whose length is the length of that natural number. The existential witness used here is simply 0, 0, 0, ..., the list of all zero times.

Lemma baseListEx (n : nat) : exists v, @length BaseType v = n.

If one list evaluated to another, then the lengths match.

Lemma evalExpListsLength (l : list Exp) : forall (l' : list BaseType),
evalExpLists l l' -> length l = length l'.

Evaluation on expressions is decidable.

Lemma evalExpDec (e : Exp) (b : BaseType) : decidable (evalExp e b).

Evaluation on lists of expressions is decidable.

Lemma evalExpListsDec (l : list Exp) (l' : list BaseType) :
decidable (evalExpLists l l').

A functional version of eval exp for lists.

Fixpoint evalExpListsFun (l : list Exp) : option (list BaseType) :=
  match l with
  | [] => Some []
  | e :: l => optionMap2 (cons (A := BaseType)) (evalExpFun e) (evalExpListsFun l)
  end.

The evaluation function on lists implies the relation.

Theorem evalExpListsFunRel (l : list Exp) : forall (l' : list BaseType),
evalExpListsFun l = Some l' -> evalExpLists l l'.

The evaluation relation on lists implies the function.

Theorem evalExpListsRelFun (l : list Exp) : forall (l' : list BaseType),
evalExpLists l l' -> evalExpListsFun l = Some l'.

l either evaluates to something or not.

Lemma evalExpListsExDec (l : list Exp) :
{l' : list BaseType | (evalExpLists l l')} +
{~exists l', (evalExpLists l l')}.

If f updated by x onto y is applied to x, then the result is y.

Lemma updateAppEq : forall (X : Type) (f : Var -> X) (x : Var) (y : X),
update f x y x = y.

If f updated by x to y is applied to z and z is not equal to x, then the result is (f z).

Lemma updateAppNeq : forall (X : Type) (f : Var -> X) (x z : Var) (y : X),
x <> z -> update f x y z = f z.

Lift a variable to a list of variables.

Coercion liftVarList (v : Var) : list Var := [v].

Lift an expression to a list of expressions.

Coercion liftExpList (e : Exp) : list Exp := [e].

Coercion liftTimeExp (t : Time) : Exp := eBase (baseTime t).

Lift a list of variables to a list of expressions.

Definition liftListVarExp (l : list Var) : list Exp :=
map eVar l.

Require Import FunctionalExtensionality.

The substitution of l -> liftListVarExp l is equal to the identity substitution.

Lemma listSubRefl : forall (l : list Var),
  listsToSub l (liftListVarExp l) = idSubst.

Theorem listSubNormal : forall (x : list Var) (l : list Exp),
  {l' : list Exp | length l' = length x /\
  listsToSub x l = listsToSub x l'}.

In the case where target list is empty, the equivalent substitution is just the source list.

In the case where the target list is not empty, we can proceed by induction.

Lemma idSubExp : forall (e : Exp),
  subExp idSubst e = e.

Lemma idSubList : forall (l : list Exp),
  listSub idSubst l = l.

Lemma idSubBoolExp : forall (b : BoolExp),
  subBoolExp idSubst b = b.
Lemma resetPreservesId : forall (l : list Var),
  resetSub idSubst l = idSubst.
Notation "( a , b )" := (pair a b).

Definition splitSrc {A B : Type} (l : list (A * B)) : list A :=
  fst (split l).

Definition splitTgt {A B : Type} (l : list (A * B)) : list B :=
  snd (split l).

Definition bindListToSub (l : list (Var * Exp)) : Subst :=
  listsToSub (splitSrc l) (splitTgt l).

A characterisation of the application of a substitution based on a bindings list to a variable, which bypasses the conversion to a substitution.

Fixpoint bindApp (l : list (Var * Exp)) (x : Var) : Exp :=
  match l with
  | (y, e) :: l' => if eqDecVar x y then e else bindApp l' x
  | _ => eVar x
  end.

Lemma bindListToSubCons (x : Var) (e : Exp) (l : list (Var * Exp)) :
  bindListToSub ((x, e) :: l) = update (bindListToSub l) x e.

Proof that the bindApp function is correct w.r.t. the substitution conversion.

Theorem bindApp_subst (l : list (Var * Exp)) (x : Var) :
bindApp l x = (bindListToSub l) x.

(x, e) is the first occurrence of a map of x in l if there is no (x, e') preceding it in the list.

Inductive firstOcc (x : Var) (e : Exp) : list (Var * Exp) -> Prop :=
  | fstocHd (l : list (Var * Exp)) : firstOcc x e ((x, e) :: l)
  | fstocTl (y : Var) (e' : Exp) (l : list (Var * Exp)) :
    firstOcc x e l -> x <> y -> firstOcc x e ((y, e') :: l).

Lemma firstOcc_unique (x : Var) (e e' : Exp) (l : list (Var * Exp)) :
  firstOcc x e l -> firstOcc x e' l -> e = e'.

Lemma splitSrcCons (x : list (Var*Exp)) (a : Var) (e : Exp):
  splitSrc ((a, e) :: x) = a :: (splitSrc x).

Lemma firstOcc_splitSrc (x : Var) (e : Exp) (l : list (Var * Exp)) :
  firstOcc x e l -> x _: splitSrc l.

Lemma splitSrc_firstOcc_ex (x : Var) (l : list (Var * Exp)) :
  x _: splitSrc l -> exists e, firstOcc x e l.

A preorder on binding lists that puts one list before the other if the latter agrees with the former on all variables in the source of the former.

Definition preordBindList (l1 l2 : list (Var * Exp)) : Prop :=
forall (x : Var) (e : Exp), firstOcc x e l1 -> firstOcc x e l2.
Notation "l1 <[] l2" := (preordBindList l1 l2) (at level 70).

Lemma preord_emp (l : list (Var * Exp)) :
[] <[] l.

The preorder that has been defined is reflexive.

Lemma preordBindList_refl (l : list (Var * Exp)) : l <[] l.

Lemma incl_hd_eq {A : Type} (l1 l2 : list A) (x : A) :
incl l1 l2 -> incl (x :: l1) (x :: l2).

If one binding list is less than another according to the preorder, then the source of the former is contained in the source of the latter according to incl.

Lemma pre_incl_splitSrc (l1 l2 : list (Var * Exp)) :
l1 <[] l2 -> incl (splitSrc l1) (splitSrc l2).

The preorder that has been defined is transitive.

Lemma preordBindList_trans (l1 l2 l3: list (Var * Exp)) :
l1 <[] l2 -> l2 <[] l3 -> l1 <[] l3.

Gives back a list whose elements are those of l minus the ones containing a variable from l'.

Fixpoint excludeSrc (l : list (Var * Exp)) (l' : list Var) : list (Var * Exp) :=
  match l with
  | [] => []
  | (x, e) :: ls => if (in_dec eqDecVar x l') then excludeSrc ls l'
    else (x, e) :: excludeSrc ls l'
  end.

The source of l with l' excluded is included within the source of l.

Lemma excludeSrc_incl (l : list (Var * Exp)) (l' : list Var) :
  incl (splitSrc (excludeSrc l l')) (splitSrc l).

Lemma set_inter_nil {A : Type} (l : list A)
  (p : forall (x y : A), {x = y} + {x <> y}) : set_inter p l [] = [].

Lemma excludeSrc_inter_emp (l : list (Var * Exp)) (l' : list Var) :
  set_inter eqDecVar (splitSrc (excludeSrc l l')) l' = [].

Lemma exclude_nil (l : list (Var * Exp)) :
  excludeSrc l [] = l.

Lemma exclude_in_splitSrc (v : Var) (x : list Var) (l : list (Var * Exp)) :
  v _: x -> ~v _: splitSrc (excludeSrc l x).

Lemma pre_notIn_cons (x : Var) (e : Exp) (l l' : list (Var * Exp)) :
  ~x _: splitSrc l -> l <[] l' -> l <[] ((x, e) :: l').
Lemma exclude_preord (l' : list Var) (l : list (Var * Exp)) :
  (excludeSrc l l') <[] l.

Lemma preord_exclude (l1 l2 : list (Var * Exp)) (x : list Var) :
  preordBindList l1 (excludeSrc l2 x) -> preordBindList l1 l2.

Lemma exclude_firstOcc (x : Var) (e : Exp)
  (l1 : list (Var * Exp)) (l2 : list Var) :
  firstOcc x e (excludeSrc l1 l2) -> firstOcc x e l1.

Lemma firstOcc_notIn_exclude (x : Var) (e : Exp)
  (l1 : list (Var * Exp)) (l2 : list Var) :
  firstOcc x e l1 -> ~x _: l2 -> firstOcc x e (excludeSrc l1 l2).

Lemma preord_cons_excl (v : Var) (e : Exp) (l1 l2 : list (Var * Exp)) :
  l1 <[] ((v, e) :: l2) -> (excludeSrc l1 [v]) <[] l2.

If (v, e) is the first occurrence of v in l1, then the question of whether l1 is less than l2 by the preorder is the same as the question as to whether l1 with v excluded is less than l2.

Lemma fst_pre_cons_excl (v : Var) (e : Exp) (l1 l2 : list (Var * Exp)) :
  firstOcc v e l1 -> (l1 <[] ((v, e) :: l2) <->
  excludeSrc l1 v <[] l2).

Lemma in_src_ex_firstOcc (v : Var) (l : list (Var * Exp)) :
  v _: splitSrc l -> exists e, firstOcc v e l.

Lemma notIn_src_cons_eq (v : Var) (e : Exp) (l1 l2 : list (Var * Exp)) :
  ~ v _: (splitSrc l1) -> (l1<[](v, e) :: l2 <-> l1 <[] l2).

Theorem dec_preordBindList (l1 l2 : list (Var * Exp)) :
  decidable (l1 <[] l2).

Fixpoint idBindList (x : list Var) : list (Var * Exp) :=
  match x with
  | [] => []
  | a :: xs => (a, eVar a) :: idBindList xs
  end.

Lemma idBindList_idSub (x : list Var) :
  bindListToSub (idBindList x) = idSubst.

The source of the identity bindings list built from x is itself x.

Lemma srcIdBindList (x : list Var) : splitSrc (idBindList x) = x.

Lemma preord_emp_eq (l : list (Var * Exp)) :
  l<[][] -> l = [].

Lemma bindApp_cons_eq (x : Var) (e : Exp) (l : list (Var * Exp)) :
  bindApp ((x, e) :: l) x = e.

Lemma bindApp_cons_neq (x y : Var) (e : Exp) (l : list (Var * Exp)) :
  x <> y -> bindApp ((x, e) :: l) y = bindApp l y.

Lemma firstOcc_bindApp (x : Var) (e : Exp) (l : list (Var * Exp)) :
  firstOcc x e l -> bindApp l x = e.

Lemma firstOcc_cons_eq (x : Var) (e e' : Exp) (l : list (Var * Exp)) :
  firstOcc x e' ((x, e) :: l) -> e = e'.

Lemma excl_cons (x : Var) (e : Exp) (l1 : list (Var * Exp)) (l2 : list Var) :
  ~x _: l2 -> excludeSrc ((x, e) :: l1) l2 = (x, e) :: excludeSrc l1 l2.

Lemma notIn_bindApp_excl (x : Var) (l1 : list (Var * Exp)) (l2 : list Var) :
  ~x _: l2 -> bindApp l1 x = bindApp (excludeSrc l1 l2) x.

Lemma in_splitSrc_excl (x : Var) (l1 : list (Var * Exp)) (l2 : list Var) :
  ~x _: l2 -> x _: splitSrc l1 -> x _: splitSrc (excludeSrc l1 l2).

If l1 <☐ l2 then the substitutions generated by l1 and l2 are equivalent for all variables in the source of l1.

Theorem preord_subst (l1 l2 : list (Var * Exp)) (x : Var) :
l1 <[] l2 -> x _: splitSrc l1 -> (bindListToSub l1) x = (bindListToSub l2) x.

Takes the binding list l and restricts its source to x, preserving any bindings of l based in x and acting as the identity otherwise.

Fixpoint restrictSrc (l : list (Var * Exp)) (x : list Var) :
  list (Var * Exp) :=
  match x with
  | [] => []
  | a :: xs => (a, ((bindListToSub l) a)) :: (restrictSrc l xs)
  end.

The source of the restrict source function is actually correct.

Lemma restrictSrc_source (l : list (Var * Exp)) (x : list Var) :
  splitSrc (restrictSrc l x) = x.

Lemma restrictSrc_in (y : Var) (x : list Var) (l : list (Var * Exp)) :
  y _: x -> (bindListToSub (restrictSrc l x)) y = (bindListToSub l) y.

Lemma listSub_notIn (x : Var) (l : list Var) (l' : list Exp) :
  ~x _: l -> (listsToSub l l') x = (eVar x).

If the source of l is included in x, then restricting l to x will yield a binding list whose corresponding substitution is the same as that of l.

Lemma restrictSrc_incl_subEq (l : list (Var * Exp)) (x : list Var) :
  incl (splitSrc l) x -> bindListToSub (restrictSrc l x) = bindListToSub l.

Lemma inVarList_in (x : Var) (l : list Var) :
  inVarList x l = true <-> x _: l.

Lemma preord_inter_exclude (l l' : list (Var * Exp)) (x : list Var) :
  set_inter eqDecVar (splitSrc l) x = [] -> preordBindList l l' ->
  preordBindList l (excludeSrc l' x).

Definition joinBindList (l l1 l2 : list (Var * Exp)) : Prop :=
  preordBindList l1 l /\ preordBindList l2 l.

Lemma joinBindList_symm (l l1 l2 : list (Var * Exp)) :
  joinBindList l l1 l2 -> joinBindList l l2 l1.

Lemma dec_joinBindList (l l1 l2 : list (Var * Exp)) :
  decidable (joinBindList l l1 l2).

Normalise the list l, by removing all redundant pairs (x, e) that are preceded in the list, and thus overwritten, by (x, e').

Fixpoint normBindList (l : list (Var * Exp)) : list (Var * Exp) :=
  match l with
  | [] => []
  | (x, e) :: l' => (x, e) :: excludeSrc (normBindList l') [x]
  end.

Lemma src_norm_in_equiv (x : Var) (l : list (Var * Exp)) :
  x _: splitSrc (normBindList l) <-> x _: splitSrc l.

Lemma norm_sub_equiv (l : list (Var * Exp)) :
  bindListToSub l = bindListToSub (normBindList l).

Theorem preordBindListAlt (l1 l2 : list (Var * Exp)) :
  l1 <[] l2 <->
  (forall x : Var, x _: (splitSrc l1) -> x _: (splitSrc l2) /\
  (bindListToSub l1) x = (bindListToSub l2) x).

Lemma preord_norm (l1 : list (Var * Exp)) :
  l1 <[] (normBindList l1) /\ (normBindList l1) <[] l1.

lubBindList l l1 l2 roughly means that l is a least upper bound for bind lists l1 and l2.

Inductive lubBindList : list (Var * Exp) -> list (Var * Exp) ->
  list (Var * Exp) -> Prop :=
  | lubbl (l1 l2 : list (Var * Exp)) :
    joinBindList (normBindList (excludeSrc l1 (splitSrc l2) ++ l2)) l1 l2 ->
    lubBindList (normBindList (excludeSrc l1 (splitSrc l2) ++ l2)) l1 l2.

Lemma lubPreordFst (l l1 l2 : list (Var * Exp)) :
  lubBindList l l1 l2 -> preordBindList l1 l.

Lemma lubPreordSnd (l l1 l2 : list (Var * Exp)) :
  lubBindList l l1 l2 -> preordBindList l2 l.

Lemma lubBindListUnique (l l' l1 l2 : list (Var * Exp)) :
  lubBindList l l1 l2 -> lubBindList l' l1 l2 ->
  l = l'.

The existence of a least upper bound for any pair of binding lists is a decidable property.

Lemma decLubBindList (l1 l2 : list (Var * Exp)) :
  decidable (exists l, lubBindList l l1 l2).

Lemma notIn_bindList_id (x : Var) (l : list (Var * Exp)) :
  ~x _: (splitSrc l) -> eVar x = bindListToSub l x.

Lemma excludeSrc_in_cons_eq (v : Var) (l1 : list (Var * Exp))
  (l2 : list Var) (e : Exp) :
  v _: l2 -> excludeSrc ((v, e) :: l1) l2 = excludeSrc l1 l2.

Lemma append_firstOcc (x : Var) (e : Exp) (l1 l2 : list (Var * Exp)) :
  firstOcc x e (l1 ++ l2) -> firstOcc x e l1 \/ firstOcc x e l2.

Lemma firstOcc_append (x : Var) (e : Exp) (l1 l2 : list (Var * Exp)) :
  firstOcc x e l1 -> firstOcc x e (l1 ++ l2).

Lemma lubBindList_pre_join (l l1 l2 : list (Var * Exp)) :
  joinBindList l l1 l2 -> (normBindList (excludeSrc l1 (splitSrc l2) ++ l2)) <[] l.

Lemma firstOcc_exclude_append (x : Var) (e : Exp) (l1 l2 : list (Var * Exp)) :
  firstOcc x e l2 ->
  firstOcc x e (excludeSrc l1 (splitSrc l2) ++ l2).

Lemma join_firstOcc_eq (x : Var) (e e' : Exp) (l l1 l2 : list (Var * Exp)) :
  joinBindList l l1 l2 -> firstOcc x e l1 -> firstOcc x e' l2 ->
  e = e'.

Lemma join_lubBindList_ex (l l1 l2 : list (Var * Exp)) :
  joinBindList l l1 l2 -> exists l',
  lubBindList l' l1 l2 /\ preordBindList l' l.

If a substitution based on a list l is reset on the list of variables x, and none of these variables of x is in the source of l, then the substitution remains unchanged after the reset operation.

Theorem reset_id (l : list (Var * Exp)) (x : list Var) :
  set_inter eqDecVar (splitSrc l) x = [] ->
  resetSub (bindListToSub l) x = (bindListToSub l).

Lemma exclude_reset (l : list (Var * Exp)) (x : list Var) :
  bindListToSub (excludeSrc l x) = resetSub (bindListToSub l) x.

A characterisation of the matching problem for expressions. This says that the e1 is equal to the e2 with the substitution l applied.

Inductive matchExp : Exp -> Exp -> list (Var * Exp) -> Prop :=
  | meVar (x : Var) (e : Exp) : matchExp e (eVar x) ([(x, e)])
  | meBase (b : BaseType) : matchExp (eBase b) (eBase b) []
  | meSub (l l1 l2 : list (Var * Exp)) (e1 e2 e1' e2' : Exp) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> lubBindList l l1 l2 ->
    matchExp (eSubtract e1 e2) (eSubtract e1' e2') l
  | meAdd (l l1 l2 : list (Var * Exp)) (e1 e2 e1' e2' : Exp) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> lubBindList l l1 l2 ->
    matchExp (eAdd e1 e2) (eAdd e1' e2') l
  | meMult (l l1 l2 : list (Var * Exp)) (e1 e2 e1' e2' : Exp) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> lubBindList l l1 l2 ->
    matchExp (eMult e1 e2) (eMult e1' e2') l
  | meWaitTime (l l1 l2 : list (Var * Exp)) (e1 e2 e1' e2' : Exp) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> lubBindList l l1 l2 ->
    matchExp (eWaitTime e1 e2) (eWaitTime e1' e2') l
  | mePeriod (l : list (Var * Exp)) (e e' : Exp) :
    matchExp e e' l -> matchExp (ePeriod e) (ePeriod e') l
  | meDist (l l1 l2 : list (Var * Exp)) (e1 e2 e1' e2' : Exp) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> lubBindList l l1 l2 ->
    matchExp (eDist e1 e2) (eDist e1' e2') l
  | meFailSafeSucc (l : list (Var * Exp)) (e e' : Exp) :
    matchExp e e' l -> matchExp (eFailSafeSucc e) (eFailSafeSucc e') l.

There is at most one "minimal" solution to the matching problem for expressions, as characterised by the matchExp relation.

Lemma matchExpUnique (e1 e2 : Exp) (l1 l2 : list (Var * Exp)) :
  matchExp e1 e2 l1 -> matchExp e1 e2 l2 -> l1 = l2.

Lemma decMatchExp (e1 e2 : Exp) :
  decidable (exists l, matchExp e1 e2 l).

Lemma matchExpSubEquivPre (e1 e2 : Exp) (l l' : list (Var * Exp)) :
  matchExp e1 e2 l -> preordBindList l l' ->
  e1 = subExp (bindListToSub l') e2.

Fixpoint freeVarsExp (e : Exp) : set Var :=
  match e with
  | eVar v => [v]
  | eBase b => empty_set Var
  | eSubtract e1 e2 => set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)
  | eMult e1 e2 => set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)
  | eAdd e1 e2 => set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)
  | eWaitTime e1 e2 => set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)
  | ePeriod e' => freeVarsExp e'
  | eFailSafeSucc e' => freeVarsExp e'
  | eDist e1 e2 => set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)
  end.

Definition freeVarsListExp (l : list Exp) : set Var :=
  fold_right (set_union eqDecVar) [] (map freeVarsExp l).

Fixpoint freeVarsListExpAlt (l : list Exp) : set Var :=
  match l with
  | [] => []
  | e :: l' => set_union eqDecVar (freeVarsExp e) (freeVarsListExpAlt l')
  end.

Lemma freeVarsListAlt_correct (l : list Exp) :
  freeVarsListExp l = freeVarsListExpAlt l.

Fixpoint freeVarsBoolExp (b : BoolExp) : set Var :=
  match b with
  | bSufficient e1 e2 => set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)
  | bNot b' => freeVarsBoolExp b'
  | bEqual e1 e2 => set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)
  | bPossInc e1 e2 e3 => set_union eqDecVar
    (set_union eqDecVar (freeVarsExp e1) (freeVarsExp e2)) (freeVarsExp e3)
  end.

Lemma in_cons_not {X : Type} (p : forall (a b : X), {a = b} + {a <> b})
  (x y : X) (l : list X) :
  x _: (y :: l) -> x = y \/ x <> y /\ x _: l.

Lemma in_cons_not_var (x y : Var) (l : list Var) :
  x _: (y :: l) -> x = y \/ x <> y /\ x _: l.

Lemma firstOcc_res_exp_sub (v : Var) (e : Exp) (l : list (Var * Exp)) (x : list Var) :
  firstOcc v e (restrictSrc l x) -> e = (bindListToSub l) v.

Lemma in_firstOcc_res (v : Var) (l : list (Var * Exp)) (x : list Var) :
  v _: x -> firstOcc v ((bindListToSub l) v) (restrictSrc l x).

Lemma firstOcc_restrict_incl (v : Var) (e : Exp) (l : list (Var * Exp)) (x y : list Var) :
  firstOcc v e (restrictSrc l x) -> incl x y -> firstOcc v e (restrictSrc l y).

Lemma preord_res_splitSrc (l1 l2 : list (Var * Exp)) :
  l1 <[] l2 -> l1 <[] (restrictSrc l2 (splitSrc l2)).

Lemma preord_restrict_union1 (l l' : list (Var * Exp)) (x y : list Var) :
  l <[] restrictSrc l' x -> l <[] restrictSrc l' (set_union eqDecVar x y).

Lemma preord_restrict_union2 (l l' : list (Var * Exp)) (x y : list Var) :
  l <[] restrictSrc l' y -> l <[] restrictSrc l' (set_union eqDecVar x y).

Lemma lub_join_preordBindList (l l' l1 l2 : list (Var * Exp)) :
  lubBindList l l1 l2 -> joinBindList l' l1 l2 -> l <[] l'.

Any Exp e with substitution from bindList x applied can be matched by some bindList z to e, where z is less than x in the preorder.

Theorem sub_matchExp_ex (e : Exp) (l : list (Var * Exp)) :
exists z, matchExp (subExp (bindListToSub l) e) e z
/\ z <[] (restrictSrc l (freeVarsExp e)).

A characterisation of the matching problem for a list of expressions. This says that the list l1 is equal to the list l2 with the substitution l applied.

Inductive matchExpLists : list Exp -> list Exp -> list (Var * Exp) -> Prop :=
  | melNil : matchExpLists [] [] []
  | melCons (e1 e2 : Exp) (l1 l2 : list Exp) (x1 x2 x3 : list (Var * Exp)) :
    matchExp e1 e2 x1 -> matchExpLists l1 l2 x2 -> lubBindList x3 x1 x2 ->
    matchExpLists (e1 :: l1) (e2 :: l2) x3.

A characterisation of the matching problem for a boolean expressions. This says that the b1 equals b2 with the substitution l applied.

Inductive matchBoolExp : BoolExp -> BoolExp -> list (Var * Exp) -> Prop :=
  | mbeSuff (e1 e1' e2 e2' : Exp) (l l1 l2 : list (Var * Exp)) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> lubBindList l l1 l2 ->
    matchBoolExp (bSufficient e1 e2) (bSufficient e1' e2') l
  | mbeNot (b b' : BoolExp) (l : list (Var * Exp)) :
    matchBoolExp b b' l -> matchBoolExp (bNot b) (bNot b') l
  | mbeEqual (e1 e1' e2 e2' : Exp) (l l1 l2 : list (Var * Exp)) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> lubBindList l l1 l2 ->
    matchBoolExp (bEqual e1 e2) (bEqual e1' e2') l
  | mbePossInc (e1 e1' e2 e2' e3 e3' : Exp) (l l' l1 l2 l3 : list (Var * Exp)) :
    matchExp e1 e1' l1 -> matchExp e2 e2' l2 -> matchExp e3 e3' l3 ->
    lubBindList l l1 l2 -> lubBindList l' l l3 ->
    matchBoolExp (bPossInc e1 e2 e3) (bPossInc e1' e2' e3') l'.

There is at most one "minimal" solution to the matching problem for lists of expressions as characterised by the matchExpLists relation.

Lemma matchExpListsUnique (e1 e2 : list Exp) (l1 l2 : list (Var * Exp)) :
matchExpLists e1 e2 l1 -> matchExpLists e1 e2 l2 -> l1 = l2.

There is at most one "minimal" solution to the matching problem for boolean expressions, as characterised by the matchExp relation.

Lemma matchBoolExpUnique (e1 e2 : BoolExp) (l1 l2 : list (Var * Exp)) :
  matchBoolExp e1 e2 l1 -> matchBoolExp e1 e2 l2 -> l1 = l2.

Lemma decMatchBoolExp (e1 e2 : BoolExp) :
  decidable (exists l, matchBoolExp e1 e2 l).

Lemma decMatchExpLists (e1 e2 : list Exp) :
  decidable (exists l, matchExpLists e1 e2 l).

Lemma split_append_fst {A B : Type} (l1 l2 : list (A * B)) :
  fst (split (l1 ++ l2)) = fst (split l1) ++ fst (split l2).

Lemma split_append_snd {A B : Type} (l1 l2 : list (A * B)) :
  snd (split (l1 ++ l2)) = snd (split l1) ++ snd (split l2).

Lemma bindSub_app_id (l1 l2 : list (Var * Exp)) :
  bindListToSub l1 = idSubst -> bindListToSub l2 = idSubst ->
  bindListToSub (l1 ++ l2) = idSubst.

Lemma notIn_src_bindApp_id (x : Var) (l : list (Var * Exp)) :
  ~ x _: splitSrc l -> bindApp l x = idSubst x.

Lemma in_sing {X : Type} (x y : X) :
  x _: [y] -> x = y.

Lemma restrict_nil_id (l : list (Var * Exp)) (x : list Var) :
  l<[]restrictSrc [] x -> bindListToSub l = idSubst.

Lemma matchExp_refl (e : Exp) :
  exists z, matchExp e e z /\ (bindListToSub z = idSubst).

Lemma incl_restrict_refl (l : list (Var * Exp)) (x y : list Var) :
  incl x y -> restrictSrc l x <[] restrictSrc l y.

Any list l with substitution from bindList x applied can be matched by some bindList z to l, where z is less than x in the preorder.

Theorem sub_matchLists_ex (l : list Exp) (x : list (Var * Exp)) :
  exists z, matchExpLists
  (listSub (bindListToSub x) l) l z /\
  preordBindList z (restrictSrc x (freeVarsListExp l)).

Lemma joinBinList_comm (l1 l2 l3 : list (Var * Exp)) :
  joinBindList l1 l2 l3 -> joinBindList l1 l3 l2.

Any boolexp b with substitution from bindList x applied can be matched by some bindList z to b, where z is less than x in the preorder.

Theorem sub_matchBool_ex (b : BoolExp) (x : list (Var * Exp)) :
  exists z, matchBoolExp
  (subBoolExp (bindListToSub x) b) b z
  /\ preordBindList z (restrictSrc x (freeVarsBoolExp b)).

Lemma matchListsSubEquivPre (l1 l2 : list Exp) (z z' : list (Var * Exp)) :
  matchExpLists l1 l2 z -> preordBindList z z' ->
  l1 = listSub (bindListToSub z') l2.

Lemma matchListsSubEquiv (e1 e2 : list Exp) (l : list (Var * Exp)) :
  matchExpLists e1 e2 l -> e1 = listSub (bindListToSub l) e2.

Lemma matchBoolExpSubEquivPre (e1 e2 : BoolExp) (l l' : list (Var * Exp)) :
  matchBoolExp e1 e2 l -> preordBindList l l' ->
  e1 = subBoolExp (bindListToSub l') e2.

Lemma subExp_restrict_eq (l1 l2 : list (Var * Exp)) (e : Exp) :
  subExp (bindListToSub l2) e = subExp (bindListToSub l1) e ->
  subExp (bindListToSub l2) e =
  subExp (bindListToSub (restrictSrc l1 (splitSrc l2))) e.

Lemma subBoolExp_restrict_eq (l1 l2 : list (Var * Exp)) (b : BoolExp) :
  subBoolExp (bindListToSub l2) b = subBoolExp (bindListToSub l1) b ->
  subBoolExp (bindListToSub l2) b =
  subBoolExp (bindListToSub (restrictSrc l1 (splitSrc l2))) b.

Lemma listSub_restrict_eq (l1 l2 : list (Var * Exp)) (l : list Exp) :
  listSub (bindListToSub l2) l = listSub (bindListToSub l1) l ->
  listSub (bindListToSub l2) l =
  listSub (bindListToSub (restrictSrc l1 (splitSrc l2))) l.

Exclude distributes over restrict

Lemma res_excl_distr (l1 l2 : list (Var * Exp)) (l : list Var) :
  restrictSrc (excludeSrc l1 l) (splitSrc (excludeSrc l2 l)) =
  excludeSrc (restrictSrc l1 (splitSrc l2)) l.

Lemma in_exclude_sub_eq (v : Var) (x : list Var) (l : list (Var * Exp)) :
  v _: x -> bindListToSub (excludeSrc l x) v = v.

passiveSrc x l, read x is passive in the source of l, or just x is passive in l, means that all variables in x are only mapped to themselves by l.

Inductive passiveSrc : list Var -> list (Var * Exp) -> Prop :=
  | psrcEmp (l : list (Var * Exp)) : passiveSrc [] l
  | psrcConsFstOcc (x : list Var) (v : Var) (l : list (Var * Exp)) :
    passiveSrc x l -> firstOcc v (eVar v) l -> passiveSrc (v :: x) l
  | psrcConsNotIn (x : list Var) (v : Var) (l : list (Var * Exp)) :
    passiveSrc x l -> ~v _: (splitSrc l) -> passiveSrc (v :: x) l.

Lemma passive_nil (x : list Var) : passiveSrc x [].

Lemma passive_tl (a : Var) (x : list Var) (l : list (Var * Exp)) :
  passiveSrc (a :: x) l -> passiveSrc x l.
Lemma passive_cons_eq (v : Var) (x : list Var) (l : list (Var * Exp)) :
  passiveSrc x l -> passiveSrc x ((v, eVar v) :: l).

Lemma notIn_cons {X : Type} (x y : X) (l : list X) :
  ~ x _: (y :: l) -> ~ x _: l.

Lemma passive_cons_notIn (v : Var) (e : Exp) (x : list Var) (l : list (Var * Exp)) :
  passiveSrc x l -> ~v _: x -> passiveSrc x ((v, e) :: l).

Lemma notIn_src_excl (v : Var) (x : list Var) (l : list (Var * Exp)) :
  ~ v _: splitSrc l ->
  bindListToSub (excludeSrc l (v :: x)) = bindListToSub (excludeSrc l x).

If all members of x are mapped to themselves by l, then x is passive in l.

Lemma idSrc_passive (x : list Var) (l : list (Var * Exp)) :
(forall v : Var, v _: x -> (bindListToSub l) v = eVar v) ->
passiveSrc x l.

If x is passive in l, then excluding it from l yields the same substitution function, and vice versa.

Theorem passiveSrc_exclude_equiv (x : list Var) (l : list (Var * Exp)) :
  passiveSrc x l <-> bindListToSub (excludeSrc l x) = bindListToSub l.

Theorem dec_passiveSrc (x : list Var) (l : list (Var * Exp)) :
  decidable (passiveSrc x l).

Lemma passive_in_firstOcc_eq (v : Var) (e : Exp) (x : list Var)
  (l : list (Var * Exp)) :
  passiveSrc x l -> v _: x -> firstOcc v e l -> e = eVar v.

Lemma in_firstOcc_id (v : Var) (x : list Var) :
  v _: x -> firstOcc v v (idBindList x).

Lemma firstOcc_notIn_append (v : Var) (e : Exp) (l1 l2 : list (Var * Exp)) :
  firstOcc v e l2 -> ~v _: (splitSrc l1) -> firstOcc v e (l1 ++ l2).

Lemma passive_excl_id (x : list Var) (l l' : list (Var * Exp)) :
  passiveSrc x l -> (excludeSrc l x) <[] l' ->
  l <[] (idBindList x) ++ l'.

Lemma notEq_sub_excl_eq (v v' : Var) (x : list Var) (l : list (Var * Exp)) :
  v <> v' -> bindListToSub (excludeSrc l x) v' =
  bindListToSub (excludeSrc l (v :: x)) v'.

Lemma id_app_excl_sub_eq (x : list Var) (l : list (Var * Exp)) :
  bindListToSub (idBindList x ++ l) = bindListToSub (excludeSrc l x).

Lemma excludeSrc_idem (x : list Var) (l : list (Var * Exp)) :
  (excludeSrc l x) = (excludeSrc (excludeSrc l x) x).

Lemma notIn_restrict (v : Var) (x : list Var) (l : list (Var * Exp)) :
  ~ v _: x -> bindListToSub (restrictSrc l x) v = v.

Lemma pre_excl_res_id (v : Var) (x w : list Var)
  (l1 l2 : list (Var * Exp)) :
  l1 <[] (restrictSrc (excludeSrc l2 x) w) -> v _: x ->
  (bindListToSub l1) v = v.

Lemma pre_excl_res_passive (x w : list Var)
  (l1 l2 : list (Var * Exp)) :
  l1 <[] (restrictSrc (excludeSrc l2 x) w) ->
  passiveSrc x l1.

Lemma preordBindList_cons (a : Var * Exp) (l l' : list (Var * Exp)):
  l <[] l' -> a :: l <[] a :: l'.

Lemma exclude_restrict_cons (v : Var) (e : Exp) (x w : list Var) (l : list (Var * Exp)) :
  v _: x -> excludeSrc (restrictSrc ((v, e) :: l) w) x = excludeSrc (restrictSrc l w) x.

Lemma notIn_sub_excl (v : Var) (x : list Var) (l : list (Var * Exp)) :
  ~v _: x -> bindListToSub (excludeSrc l x) v = bindListToSub l v.

Lemma excl_res_distr (x w : list Var) (l : list (Var * Exp)) :
  excludeSrc (restrictSrc (excludeSrc l x) w) x = excludeSrc (restrictSrc l w) x.

Definition set_equal {A : Type} (l1 l2 : set A) : Prop :=
  forall a : A, a _: l1 <-> a _: l2.
Notation "a ={}= b" := (set_equal a b) (at level 70).

Lemma set_equal_not {A : Type} (l1 l2 : set A) :
  l1 ={}= l2 -> forall a : A, ~a _: l1 <-> ~a _: l2.

Lemma set_equal_refl {A : Type} (l : set A) :
  l ={}= l.

Lemma set_equal_trans {A : Type} (l1 l2 l3 : set A) :
  l1 ={}= l2 -> l2 ={}= l3 -> l1 ={}= l3.

Lemma set_equal_symm {A : Type} (l1 l2 : set A) :
  l1 ={}= l2 -> l2 ={}= l1.

Lemma set_equal_nil_l {A : Type} (l2 : set A) :
  [] ={}= l2 -> l2 = [].

Lemma set_equal_nil_r {A : Type} (l1 : set A) :
  l1 ={}= [] -> l1 = [].

Lemma set_equal_union_app {A : Type} (p : forall a b : A, {a = b} + {a <> b})
  (l1 l2 : set A) :
  set_union p l1 l2 ={}= l1 ++ l2.

Definition equivBindList (l1 l2 : list (Var * Exp)) : Prop :=
  l1 <[] l2 /\ l2 <[] l1.
Notation "a =[]= b" := (equivBindList a b) (at level 70).

Lemma equiv_preordBindList_l (l1 l1' l2 : list (Var * Exp)) :
  l1 <[] l2 -> l1 =[]= l1' -> l1' <[] l2.

Lemma equiv_preordBindList_r (l1 l2 l2' : list (Var * Exp)) :
  l1 <[] l2 -> l2 =[]= l2' -> l1 <[] l2'.

Lemma equivBindList_symm (l1 l2 : list (Var * Exp)) :
  l1 =[]= l2 -> l2 =[]= l1.

Lemma equivBindList_trans (l1 l2 l3 : list (Var * Exp)) :
  l1 =[]= l2 -> l2 =[]= l3 -> l1 =[]= l3.

Lemma equivBindList_refl (l : list (Var * Exp)) :
  l =[]= l.

Lemma firstOcc_exclude_notIn (v : Var) (e : Exp) (x : list Var)
  (l : list (Var * Exp)) :
  firstOcc v e (excludeSrc l x) -> ~ v _: x.

Lemma preord_exclude_pres (l l' : list (Var * Exp)) (x : list Var) :
  l <[] l' -> excludeSrc l x <[] excludeSrc l' x.

Lemma equivBindList_cons (a : Var * Exp) (l l' : list (Var * Exp)):
  l =[]= l' -> a :: l =[]= a :: l'.

Lemma equivBindList_exclude (l l' : list (Var * Exp)) (x : list Var) :
  l =[]= l' -> excludeSrc l x =[]= excludeSrc l' x.

Lemma equivBindList_splitSrc (l l' : list (Var * Exp)) :
  l =[]= l' -> splitSrc l ={}= splitSrc l'.

Lemma equivBindList_join (l l' l1 l2 : list (Var * Exp)) :
  l =[]= l' -> joinBindList l l1 l2 -> joinBindList l' l1 l2.

Lemma equivBindList_restrict (l l' : list (Var * Exp)) (x : list Var) :
  l =[]= l' -> restrictSrc l x = restrictSrc l' x.

Lemma set_eq_excl (l : list (Var * Exp)) (x y : list Var) :
  x ={}= y -> excludeSrc l x = excludeSrc l y.

Lemma set_eq_res_preord (l : list (Var * Exp)) (x y : list Var) :
  x ={}= y -> restrictSrc l x <[] restrictSrc l y.

Lemma set_eq_res_equiv (l : list (Var * Exp)) (x y : list Var) :
  x ={}= y -> restrictSrc l x =[]= restrictSrc l y.

Lemma set_eq_freeVars_map (x : list Var) :
  (freeVarsListExp (map eVar x)) ={}= x.

Lemma firstOcc_in_src (v : Var) (e : Exp) (x : list Var) (l : list (Var * Exp)) :
  firstOcc v e (restrictSrc l x) -> v _: x.

Lemma restrict_add_cons_equiv (v : Var) (x : list Var) (l : list (Var * Exp)) :
  restrictSrc l (set_add eqDecVar v x) =[]= restrictSrc l (v :: x).

Lemma diff_restrict_exclude (l : list (Var * Exp)) (x y : list Var) :
  restrictSrc l (set_diff eqDecVar x y) =[]= (excludeSrc (restrictSrc l x) y).

Lemma preord_restrict_app_join (x w : list Var) (l l1 l2 : list (Var * Exp)) :
  l1 <[] restrictSrc l x -> l2 <[] restrictSrc l w ->
  joinBindList (restrictSrc l (x ++ w)) l1 l2.

Lemma listSub_emp_id l : listsToSub l [] = idSubst.

Lemma resetSub_neq s v1 v2 :
  v1 <> v2 -> (resetSub s [v1]) v2 = s v2.

Lemma varEq_eq x a : true = varEq x a <-> x = a.

Lemma varEq_neq x a : false = varEq x a <-> x <> a.

Lemma inVarList_out (x : Var) (l : list Var) :
  inVarList x l = false <-> ~ x _: l.

Lemma resetSub_eq s v : (resetSub s [v]) v = v.

Replace a single true varEqDec

Ltac varEqDec_true := let U := fresh in
  match goal with [ |- context[varEqDec ?x ?x]] =>
    remember (varEqDec x x) as U;
    match goal with [U1 : U = varEqDec x x |- _] =>
      clear U1; destruct U;[
      match goal with [U2 : x = x |- _] =>
        clear U2
      end |
      match goal with [U2 : x <> x |- _] =>
        contradiction U2; reflexivity
      end]
    end
  end.

Replace a single false varEqDec. The tactic will fail if it matches an x and a y that aren't obviously false by inversion.

Ltac varEqDec_false := let U := fresh in
  match goal with [ |- context[varEqDec ?x ?y]] =>
    remember (varEqDec x y) as U;
    match goal with [U1 : U = varEqDec x y |- _] =>
      clear U1; destruct U;[
      match goal with [U2 : x = y |- _] =>
        inversion U2
      end |
      match goal with [U2 : x <> y |- _] =>
        clear U2
      end]
    end
  end.

Gets rid of lingering occurrences of resetSub in the goal.

Ltac remove_resets := simpl; repeat rewrite resetPreservesId;
unfold idSubst; simpl; unfold liftVarList; unfold resetSub;
simpl; unfold varEq; repeat varEqDec_true; repeat varEqDec_false.

Gets rid of lingering occurrences of update in the goal.

Ltac remove_updates := repeat (repeat rewrite updateAppEq;
repeat (rewrite updateAppNeq;[ | solve [neq_inversion]]));
unfold idSubst.

Gets rid of lingering occurrences of resetSub in the hypothesis. Tactic will halt as soon as it encounters a resetSub that can't be eliminated, so doesn't necessarily remove ALL possible resets from all hypotheses.

Ltac remove_resets_hyp U := generalize dependent U; remove_resets; intro U.

Gets rid of lingering occurrences of resetSub in the hypothesis.

Ltac remove_updates_hyp U := generalize dependent U; remove_updates; intro U.

Performs some simplifications to goal like removing updates and resets.

Ltac clean_proc := simpl; remove_resets; remove_updates.

If there's one hypothesis U (usually without any dependencies), this tactic generalises it, applys some tactic t, and then re-assumed the hypothesis into the hypotheses.

Ltac gen_app_intro t U := generalize dependent U; t; intro U.

Ltac clean_proc_hyp U := gen_app_intro clean_proc U.

Lemma eval_pres_sub e b s : e |_| b -> subExp s e = e.

A stronger version of the uniqueness property of the evalution relation over expressions. In this version, any substitution is allowed to be applied to the expression in one of the evaluations and the equality still holds.

Lemma evalExp_sub_unique_strong e b b' s : e |_| b -> subExp s e |_| b' -> b = b'.

Repeatedly matches the goal to matching evaluations, creates the equality that the corresponding base type are equal, inverts this to unpackage the contents of the base types, and clear the original evaluations.

Ltac unique_exps := repeat let U := fresh in
  match goal with
  | [ U1 : ?e1 |_| ?b1, U2 : ?e1 |_| ?b2 |- _] =>
    assert (b1 = b2) as U;
    [eapply evalExpUnique; [apply U1 | apply U2] | ]; clear U1 U2; invertClear U
  | [ U1 : ?e1 |_| ?b1, U2 : subExp _ ?e1 |_| ?b2 |- _] =>
    assert (b1 = b2) as U;
    [eapply evalExp_sub_unique_strong; [apply U1 | apply U2] | ]; clear U1 U2;
    invertClear U
  end.

Given a goal of type a _: l, this tactic repeatedly checks if a is the head of l, drilling into l until either the empty list is reached, in which case the tactic fails, or the value a is found, in which case it proceeds with the constructor

Ltac inList_in_tac := match goal with
  | [ |- ?a _: (?a :: _)] => apply in_eq
  | [ |- _ _: (_ :: _)] => apply in_cons; inList_in_tac
  end.

Lemma cons_notIn {T : Type} (a b : T) l : b <> a -> ~b _: l -> ~b _: (a :: l).

Given a goal of type ~a _: l, this tactic repeatedly checks if a is the head of l, drilling into l until either the empty list is reached, in which case the tactic fails, or the value a is found, in which case it proceeds with the constructor

This page has been generated by coqdoc