Definition perm_list (l : list Name) p : list Name :=
map p l.
Notation "p *- l" := (perm_list l p) (at level 70).
Lemma perm_list_step A a p :
p *- (a::A) = (p a) :: (p *- A).
Proof.
reflexivity.
Qed.
Lemma perm_list_inv A p p' :
Inv p p' -> (p *- (p' *- A)) = A.
Proof.
intros H1. induction A as [|a A IH]; simpl; auto.
specialize (H1 a) as [_ H2]. rewrite H2, IH. reflexivity.
Qed.
(*
Identity and associativity are satisfied by the action.
List of Name is therefore a sym type
*)
Fact list_id A :
id *- A = A.
Proof.
induction A as [|a A IH]; simpl; auto; rewrite IH; auto.
Qed.
Fact list_assoc A p p':
(p ** p' *- A) = (p *- (p' *- A)).
Proof.
induction A; simpl; auto.
rewrite IHA. reflexivity.
Qed.
Lemma list_swap_perm A p p' :
(forall a, a el A -> p a = p' a) -> p *- A = (p' *- A).
Proof.
intros H1. induction A as [|a A IH]; simpl; auto. f_equal.
- apply H1. now left.
- apply IH. intros b H2. apply H1. now right.
Qed.
(*
With itself as the finite support, the list is a nominal type
*)
Lemma list_nominal A p :
(forall a, a el A -> p a = a) -> p *- A = A.
Proof.
induction A as [| a A IH]; intros H1; auto; simpl; rewrite (H1 a), IH; auto.
Qed.
Lemma perm_list_el' A a p :
a el A -> (p a) el (p *- A).
Proof.
induction A; auto. intros [<-|H1]; simpl; auto.
Qed.
Lemma perm_list_el'' A a p p' :
Inv p p' -> (p a) el (p *- A) -> a el A.
Proof.
intros HP. induction A; simpl; trivial.
simpl in *. intros [H1|H1]; auto.
left. now rewrite <-perm_inj' with (p := p)(p' := p').
Qed.
Lemma perm_list_el A a p :
Perm p -> (p a) el (p *- A) <-> a el A.
Proof.
intros HP. split.
- destruct HP as [ _ [p' HP]]. apply (perm_list_el'' HP).
- apply perm_list_el'.
Qed.
Lemma perm_list_shift A a p p' :
Inv p p' -> a el (p' *- A) <-> (p a) el A.
Proof.
intros HP. split; induction A as [ | b A IH]; auto; simpl in *; intros [H1|H2]; subst; auto.
Qed.
Lemma transp_list_el A a b c :
c el A -> c <> a -> c <> b -> c el (a$b *- A).
Proof.
intros. rewrite perm_list_shift with (p:=a$b); auto. solve_dec.
Qed.
Lemma transp_list_indep A a b :
~ a el A -> ~ b el A -> (a$b) *- A = A.
Proof.
intros. induction A; auto.
simpl. f_equal; auto. simpl in *. solve_dec; intuition.
Qed.
Lemma concat_el (X: Type) (x : X) (ll : list (list X)) :
x el concat ll <-> exists (l : list X), x el l /\ l el ll.
Proof.
split.
- induction ll as [| A ll IH]; simpl; auto. intros [H1|H1] % in_app_or.
+ exists A. auto.
+ specialize (IH H1) as [c [H2 H3]]. exists c. auto.
- intros [l [H1 H2]]. induction ll as [| A ll IH]; simpl; auto.
apply in_or_app. destruct H2 as [->|H2]; auto.
Qed.
Lemma concat_el_sub (X : Type) (x : X) (A B: list (list X)) :
A <<= B -> x el concat A -> x el concat B.
Proof.
intros H1 [E [H2 H3]] % concat_el. apply concat_el; eauto.
Qed.
Lemma concat_nil' (X : Type) (ll : list (list X)) :
concat ll = [] <-> (forall l, l el ll -> l = []).
Proof.
split; induction ll as [|A ll IH]; simpl; auto.
- intros H1 % app_eq_nil l [H2|H2].
+ now subst.
+ now apply IH.
- intros H1. rewrite IH, (H1 A); auto.
Qed.
Lemma concat_map_el (X Y : Type) (A : list X) (f : X -> list Y) (y : Y) :
y el concat (map f A) <-> exists x, x el A /\ y el f x.
Proof.
split.
- intros [l [H1 [x [H2 H3]] % in_map_iff]] % concat_el. subst. now exists x.
- intros [x [H1 H2]]. apply concat_el. exists (f x). split; trivial.
apply in_map_iff. exists x. split; trivial.
Qed.
Lemma incl_cons (X: Type) (x : X) (A B : list X) :
A <<= B -> A <<= (x :: B).
Proof.
intros H1 a H2. right. apply H1, H2.
Qed.
Lemma concat_incl_list (X Y : Type) l (f g : X -> list Y) :
(forall x, x el l -> f x <<= g x) -> concat (map f l) <<= concat (map g l).
Proof.
induction l as [|t l IH]; intros H1; auto.
simpl. apply incl_app.
- apply incl_appl, H1. auto.
- apply incl_appr, IH. auto.
Qed.
Lemma map_nth_indep (X : Type) (f : X->X) (l : list X) (d : X) (k: nat):
k < |l| -> nth k (map f l) d = f (nth k l d).
Proof.
intros. rewrite nth_indep with (d':=f d); try now rewrite map_length. now rewrite map_nth.
Qed.
Lemma nth_el_indx (X:Type) (x:X) (A:list X) :
x el A <-> exists k, k < |A| /\ (nth k A x) = x.
Proof.
split.
- intros H1. induction A as [|b A]; simpl in *; auto. destruct H1 as [H1|H1].
+ exists 0. split; try assumption. omega.
+ specialize (IHA H1). destruct IHA as [k [H2 H3]]. exists (S k).
split; try assumption. omega.
- intros [k [H1 <-]]. apply nth_In, H1.
Qed.
Lemma nth_el_indx_map (X Y :Type) (x:X)(y:Y) (A:list X) (f:X->Y) :
y el (map f A) <-> exists k, k < |A| /\ f (nth k A x) = y.
Proof.
split.
- intros [a [H1 [k [H2 H3]] % nth_el_indx ]] % in_map_iff.
exists k. split; try assumption.
now rewrite (nth_indep A x a H2), H3.
- intros [k [H1 H2]]. apply in_map_iff.
exists (nth k A x). split; auto using nth_In.
Qed.
(*
If every element x in a list l has a corresponding y, such that P x y holds,
then there is a list l' that has all those elements y in the right order
*)
Lemma list_prop_rel (X Y : Type) (l : list X) (P : X -> Y -> Prop) (xd : X) (yd : Y) :
(forall x, x el l -> exists y, P x y) -> exists l', |l| = |l'| /\ forall k, k < |l| -> (P (nth k l xd) (nth k l' yd)).
Proof.
induction l as [| a l IHl]; intros H.
- exists []. split; trivial. simpl. intros. omega.
- assert(H1 : a el a :: l) by auto.
assert(H2 : forall x, x el l -> exists y, P x y) by auto.
destruct (H a H1) as [y H3]. destruct (IHl H2) as [l' [H4 H5]].
exists (y::l'). split; simpl; try congruence.
intros. destruct k; auto. apply H5. omega.
Qed.
(*
The next are more advanced implementations on lists used in decision procedures.
We implement map2, a pointwise map, a big 'and', and a big 'or'.
We also introduce an inductive predicate for two lists of the same length.
*)
(*
Like map2 in ocaml
*)
Fixpoint map2 (X Y Z :Type) (f : X -> Y -> Z) (l: list X) (l' : list Y) : list Z :=
match l, l' with
| a :: xs, b :: ys => (f a b) :: (map2 f xs ys)
| _, _ => []
end.
(*
A big boolean 'and' on the list
*)
Fixpoint all_true (l : list bool) : bool :=
match l with
| [] => true
| a :: xs => if a then all_true xs else false
end.
Lemma all_true_true l :
all_true l = true <-> forall x, x el l -> x = true.
Proof.
split; induction l; simpl in *; auto; intros; try destruct H0; destruct a; auto.
Qed.
(*
Induction principle for two lists of same length
*)
Lemma dl_induction (X Y : Type) (p : list X -> list Y -> Prop) :
(p [] []) ->
(forall x y l l', p l l' -> p (x::l) (y::l')) ->
forall (l : list X) (l' : list Y), |l| = |l'| -> p l l'.
Proof.
induction l, l'; intros; simpl in *; auto; omega.
Qed.
(*
Inductive predicate for two lists of same length.
plist for "parallel lists"
*)
Inductive plist (X Y : Type) : list X -> list Y -> Prop :=
| pListN : plist [] []
| pListC l l' x y : plist l l' -> plist (x::l) (y::l').
Lemma plist_len (X Y : Type) (l: list X) (l': list Y) :
|l| = |l'| -> plist l l'.
Proof.
apply dl_induction; now constructor.
Qed.
Lemma len_plist (X Y : Type) (l: list X) (l': list Y) :
plist l l' -> |l| = |l'|.
Proof.
induction 1; simpl; auto.
Qed.
Lemma plist_eq (X: Type) l l' (x:X) :
|l| = |l'| -> (forall k, k < |l| -> nth k l x = nth k l' x) -> l = l'.
Proof.
intros H1 H2. induction (plist_len H1); simpl in *; auto.
rewrite (H2 0); try omega. rewrite IHp; auto. intros k H3. apply (H2 (S k)). omega.
Qed.
Lemma map_eq (X Y : Type) (f: X -> Y) (l l' : list X) (x:X) :
|l| = |l'| -> (forall k, k < |l| -> f (nth k l x) = f (nth k l' x)) -> map f l = map f l'.
Proof.
intros H1 H2. apply plist_eq with (x:=f x); try now rewrite map_length, map_length.
intros k H3. rewrite map_length in H3. rewrite map_nth, map_nth. now apply H2.
Qed.
Lemma app_equi (X : Type) (x y l l' : list X) :
x === y -> l === l' -> x++l === y++l'.
Proof.
intros H1 H2. split; intros a [H3|H3] % in_app_iff; apply in_app_iff.
- left. now apply H1.
- right. now apply H2.
- left. now apply H1.
- right. now apply H2.
Qed.
Lemma concat_equi (X : Type) (l l' : list (list X)) (x : list X) :
|l| = |l'| -> (forall k, k < |l| -> (nth k l x) === (nth k l' x)) -> concat (l) === concat (l').
Proof.
intros H1. induction (plist_len H1); auto.
intros H2. simpl. apply app_equi.
- specialize (H2 0). simpl in H2. apply H2. omega.
- apply IHp; auto. intros. specialize (H2 (S k)). simpl in H2. apply H2. omega.
Qed.
Lemma concat_map_equi (X Y : Type) (l l' : list X) (f : X -> list Y) (x : X) :
|l| = |l'| -> (forall k, k < |l| -> f (nth k l x) === f (nth k l' x)) -> concat (map f l) === concat (map f l').
Proof.
intros H1 H2. apply concat_equi with (x:=f x).
- now repeat rewrite map_length.
- intros k. rewrite map_length. intros H3. repeat rewrite map_nth. now apply H2.
Qed.
Lemma in_map2_iff (X Y Z : Type) (f : X -> Y -> Z) (l : list X) (l' : list Y) (z : Z) (x : X) (y : Y) :
|l| = |l'| -> (z el map2 f l l' <-> (exists k, k < |l| /\ f (nth k l x) (nth k l' y) = z)).
Proof.
intros HL. split.
- intros H1. induction (plist_len HL); simpl in *; auto. destruct H1 as [H1|H1].
+ exists 0. split; trivial. omega.
+ inversion HL as [H2]. specialize (IHp H2 H1) as [k [IH1 IH2]]. exists (S k). split; trivial. omega.
- intros [k [H1 H2]]. revert H1 H2. revert k.
induction (plist_len HL), k; intros; simpl in *; try omega; auto.
right. apply (IHp) with (k := k); auto. omega.
Qed.
Lemma map2_all_true (X Y : Type) (f: X -> Y -> bool) (l : list X) (l' : list Y) (x : X) (y : Y) :
|l| = |l'| -> all_true (map2 f l l') = true <-> forall k, k < |l| -> f (nth k l x) (nth k l' y) = true.
Proof.
intros HL. split.
- rewrite all_true_true. intros H1 k H2. apply H1. rewrite (in_map2_iff); eauto.
- intros H1. rewrite all_true_true. intros z H2.
rewrite in_map2_iff with (x:=x)(y:=y) in H2; try assumption.
destruct H2 as [k [H2 H3]]. rewrite <-H3. apply H1, H2.
Qed.
(*
A big 'or' on the list.
*)
Fixpoint some_true (l : list bool) : bool :=
match l with
| [] => false
| a :: xs => if a then true else some_true xs
end.
Lemma some_true_true l :
some_true l = true <-> true el l.
Proof.
split; induction l; simpl; auto; intros H1; destruct a eqn:E; auto. intuition.
Qed.
(*
A pointwise map
*)
Fixpoint map_pw (X Y : Type) (FL : list (X -> Y)) (PL : list X) : list Y :=
match FL, PL with
| f :: FL, x :: PL => (f x) :: (map_pw FL PL)
| _, _ => []
end.
(*
Combining map_pw and map is equivalent to map2.
It is used instead of map2 in some decision procedures,
because coq does not find the decreasing argument when using map2
*)
Lemma map_pw_map (X Y : Type) (f : X -> Y -> bool) l l' z x y :
|l| = |l'| -> z el (map_pw (map f l) l') -> exists k, k < |l| /\ f (nth k l x) (nth k l' y) = z.
Proof.
intros H3 H4. induction (plist_len H3); simpl in *; auto. destruct H4 as [H4|H4].
- exists 0. split; try assumption. omega.
- inversion H3 as [H5]. specialize (IHp H5 H4) as [k [H6 H7]]. exists (S k). split; try assumption. omega.
Qed.
Lemma map_pw_map_eq (X Y : Type) (l:list X) (l':list Y) f x y :
|l| = |l'| -> (forall k, k < |l| -> f (nth k l x) (nth k l' y) = nth k l x) -> map_pw (map f l) l' = l.
Proof.
intros H1. induction (plist_len H1); auto.
intros H2. simpl. f_equal.
- specialize (H2 0). simpl in H2. apply H2. omega.
- apply IHp; auto. intros. specialize (H2 (S k)). simpl in H2. apply H2. omega.
Qed.
(*
all_true on map_pw is like a big 'and' on the applications on functions that return a bool.
*)
Lemma all_true_map_pw (X : Type) (l : list (X -> bool)) (l' : list X) (f : X -> bool) (x : X) :
|l| = |l'| -> all_true (map_pw l l') = true <-> forall k, k < |l| -> (nth k l f) (nth k l' x) = true.
Proof.
intros H1. split.
- induction (plist_len H1) as [| l l' a b H2 H3]; simpl in *; intros H4 k; try omega.
inversion H1 as [HL]. destruct k, (a b); auto. intros H5. apply (H3 HL H4). omega.
- induction (plist_len H1) as [|l l' a b H2 H3]; simpl in *; intros H4; try reflexivity.
destruct(a b) eqn:E.
+ apply H3; intros; auto. assert(H5: (S k) < (S (|l|))) by omega. specialize (H4 (S k) H5). now simpl in H4.
+ assert(H5: 0 < S(|l|)) by omega. specialize(H4 0 H5). simpl in H4. now rewrite <-E, H4.
Qed.
Lemma all_true_map_pw_map (X Y : Type) (l : list X) (l' : list Y) (f : X -> Y -> bool) (x : X) (y : Y) :
|l| = |l'| -> all_true (map_pw (map f l) l') = true <-> forall k, k < |l| -> f (nth k l x) (nth k l' y) = true.
Proof.
intros H1.
split; rewrite all_true_map_pw with (f:= f x)(x:=y); rewrite map_length;
try assumption; intros H2 k H3; specialize (H2 k H3).
- now rewrite map_nth in H2.
- now rewrite map_nth.
Qed.
Section NatNumList.
Implicit Type x y z : nat.
Implicit Type l : list nat.
Fixpoint num_max x y: nat :=
match x,y with
| 0, 0 => 0
| 0, b => b
| a, 0 => a
| S a, S b => S (num_max a b)
end.
Fixpoint list_max' l (acc : nat) : nat :=
match l with
| [] => acc
| x :: xs => list_max' xs (num_max x acc)
end.
Definition list_max l : nat :=
list_max' l 0.
Lemma num_max_zero x :
num_max x 0 = x.
Proof.
induction x; simpl; auto.
Qed.
Lemma num_max_or x y :
num_max x y = x \/ num_max x y = y.
Proof.
revert x. induction y; simpl; intros x; induction x; simpl; auto.
destruct (IHy x); f_equal; auto.
Qed.
Lemma num_max_comm x y :
num_max x y = num_max y x.
Proof.
revert y. induction x; intros y; induction y; auto using num_max_zero.
simpl. f_equal. exact (IHx y).
Qed.
Lemma num_max_le x y :
num_max x y = x -> y <= x.
Proof.
revert x. induction y; intros x; induction x; intros H1; simpl in *; try omega.
assert(num_max x y = x) by omega; enough (y <= x) by omega. auto.
Qed.
Lemma list_max_dep' l x y :
x <= y -> list_max' l x <= list_max' l y.
Proof.
revert x y. induction l as [|z l IH]; intros x y H1; simpl; auto.
destruct (num_max_or z x) as [E1|E1], (num_max_or z y) as [E2|E2]; rewrite E1, E2; trivial; apply IH.
- apply num_max_le in E1. rewrite num_max_comm in E2. apply num_max_le in E2. omega.
- apply num_max_le in E2. rewrite num_max_comm in E1. apply num_max_le in E1. omega.
- rewrite num_max_comm in E1. rewrite num_max_comm in E2. apply num_max_le in E1. apply num_max_le in E2. omega.
Qed.
Lemma list_max_cons' l x :
list_max l <= list_max (x::l).
Proof.
revert x. unfold list_max; simpl.
induction l as [|y l IH]; intros x; simpl; auto; try omega.
rewrite num_max_zero, num_max_zero. destruct (num_max_or y x) as [->|E]; trivial.
rewrite E. rewrite num_max_comm in E. apply num_max_le in E. now apply list_max_dep'.
Qed.
Lemma list_max_cons'' l x :
x <= list_max (x::l).
Proof.
unfold list_max. simpl. rewrite num_max_zero. revert x.
induction l as [|y l IH]; auto. simpl. intros x. destruct (num_max_or y x) as [E|E].
- rewrite E. apply num_max_le in E. specialize (IH y). omega.
- rewrite E. rewrite num_max_comm in E. apply num_max_le in E. specialize (IH x). omega.
Qed.
Lemma list_max_max l x :
x el l -> x <= list_max l.
Proof.
induction l as [|y l IH]; simpl; auto.
intros [->|H1].
- exact (list_max_cons'' l x).
- assert(list_max l <= list_max (y::l)) by apply list_max_cons'.
specialize (IH H1). omega.
Qed.
Lemma gt_list_max l x :
x > list_max l -> ~x el l.
Proof.
intros H1 H2 % list_max_max. omega.
Qed.
Fixpoint list_sum l :=
match l with
| [] => 0
| x :: xs => x + (list_sum xs)
end.
Fact list_sum_zero l :
list_sum l = 0 <-> forall x, x el l -> x = 0.
Proof.
assert(Z: forall m n, m + n = 0 <-> m = 0 /\ n = 0) by (intros; omega).
split.
- intros H1. induction l; intros x H2; auto. simpl in H1.
rewrite Z in H1. destruct H1 as [H11 H12]. specialize (IHl H12). destruct H2 as [<-|H2]; auto.
- intros H1. induction l; simpl in *; trivial.
rewrite Z. split; auto.
Qed.
End NatNumList.
Section Freshness.
Definition name_list_max (l : list Name) :=
list_max (map fst l).
Definition fresh' l k : Name :=
(S (name_list_max l), k).
Lemma name_list_max_max l x :
x el l -> fst x <= name_list_max l.
Proof.
intros. apply list_max_max, in_map_iff; eauto.
Qed.
Lemma gt_name_list_max l x :
x > name_list_max l -> forall y, ~(x,y) el l.
Proof.
intros H1 y H2 % name_list_max_max. simpl in H2. omega.
Qed.
Fact freshness' l k :
~(fresh' l k) el l.
Proof.
unfold fresh'. intros H1 % gt_name_list_max; auto.
Qed.
End Freshness.
(*
Replace kth element in l with x.
*)
Fixpoint rep_nth (X : Type) (k : nat) (l : list X) (x : X) : list X :=
match k, l with
| _, [] => []
| S k, (x' :: r) => x' :: rep_nth k r x
| O, (_ :: r) => x :: r
end.
Lemma rep_nth_nil (X : Type) (k : nat) (x : X) :
rep_nth k [] x = [].
Proof.
destruct k; reflexivity.
Qed.
Hint Resolve rep_nth_nil.
Lemma rep_nth_len (X : Type) (k : nat) (l : list X) (x : X) :
|rep_nth k l x| = |l|.
Proof.
revert k. induction l; simpl; intros; induction k; simpl; auto.
Qed.
Lemma rep_nth_len' (X Y : Type) (k : nat) (l : list X) (l' : list Y) (x : X) :
|l| = |l'| -> |rep_nth k l x| = |l'|.
Proof.
intros H1. rewrite <-H1. apply rep_nth_len.
Qed.
Lemma rep_nth_exact (X : Type) (k : nat) (l : list X) (x xd : X) :
k < |l| -> nth k (rep_nth k l x) xd = x.
Proof.
revert k. induction l; simpl; intros; try omega.
induction k; simpl; auto. apply IHl; omega.
Qed.
Lemma rep_nth_el (X : Type) (k : nat) (l : list X) (x : X) :
k < |l| -> x el rep_nth k l x.
Proof.
revert k. induction l; simpl; intros; try omega.
induction k; simpl; auto. right. apply IHl. omega.
Qed.
Lemma rep_nth_el_or (X : Type) (k : nat) (l : list X) (x xr : X) :
x el rep_nth k l xr -> x = xr \/ x el l.
Proof.
revert k. induction l; simpl; intros.
- rewrite rep_nth_nil in H. auto.
- induction k; simpl in*; destruct H; auto. specialize (IHl k H). intuition.
Qed.
Lemma rep_nth_overwrite (X : Type) (k : nat) (l : list X) (x x' : X) :
rep_nth k (rep_nth k l x) x' = rep_nth k l x'.
Proof.
revert k. induction l; simpl; intros.
- now repeat rewrite rep_nth_nil.
- induction k; simpl; auto. f_equal. apply IHl.
Qed.
Lemma rep_nth_indep (X : Type) (k : nat) (l : list X) (x xd : X) :
forall k', k <> k' -> nth k' (rep_nth k l x) xd = nth k' l xd.
Proof.
revert k. induction l; simpl; intros.
- rewrite rep_nth_nil. simpl. now destruct k'.
- destruct k, k'; simpl; auto.
Qed.
Lemma rep_nth_el' (X : Type) (k k' : nat) (l : list X) (x xd : X) :
k < |l| -> k' < |l| -> k <> k' -> nth k' l xd el rep_nth k l x.
Proof.
intros H1 H2 H3.
rewrite <-rep_nth_indep with (k:=k)(x:=x); trivial. apply nth_In.
now rewrite rep_nth_len.
Qed.
Lemma rep_nth_id (X : Type) (k : nat) (l : list X) (xd : X) :
rep_nth k l (nth k l xd) = l.
Proof.
revert k. induction l; simpl; intros.
- now rewrite rep_nth_nil.
- destruct k; simpl; auto. f_equal. apply IHl.
Qed.