Library CoLoR.Term.SimpleType.TermsEnv

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Operations on environments of terms of simply typed lambda-calculus are introduced in this file.

Set Implicit Arguments.


Module TermsEnv (Sig : TermsSig.Signature).

  Module Export TL := TermsLifting.TermsLifting Sig.

  Definition emptyEnv E := forall p, E |= p :! .

  Lemma varD_tail : forall E A i, E |= S i := A -> tail E |= i := A.

  Lemma varD_tail_rev : forall E A i, tail E |= i := A -> E |= S i := A.

  Lemma varUD_tail : forall E i, E |= S i :! -> tail E |= i :! .

  Lemma varUD_tail_rev : forall E i, tail E |= i :! -> E |= S i :! .

  Lemma varD_UD_absurd : forall E p A, E |= p := A -> E |= p :! -> False.

  Definition equiv E x E' x' :=
    (forall A, E |= x := A <-> E' |= x' := A) /\ (E |= x :! <-> E' |= x' :!).

  Lemma split_beyond : forall E k n p, p < k -> length E <= p ->
    (initialSeg E k ++ copy n None ++ finalSeg E k) |= p :! .

  Lemma equiv_copy_split_l : forall E k p n, p < k ->
    equiv E p (initialSeg E k ++ copy n None ++ finalSeg E k) p.

  Lemma copy_split_l_varD : forall E k p n A, p < k -> E |= p := A ->
    (initialSeg E k ++ copy n None ++ finalSeg E k) |= p := A.

  Lemma copy_split_l_varUD : forall E k p n, p < k -> E |= p :! ->
    (initialSeg E k ++ copy n None ++ finalSeg E k) |= p :! .

  Lemma copy_split_l_rev_varD : forall E k p n A, p < k ->
    (initialSeg E k ++ copy n None ++ finalSeg E k) |= p := A -> E |= p := A.

  Lemma copy_split_l_rev_varUD : forall E k p n, p < k ->
    (initialSeg E k ++ copy n None ++ finalSeg E k) |= p :! -> E |= p :! .

  Lemma equiv_copy_split_r : forall E k n p p', p >= k -> p' = p + n ->
    equiv E p (initialSeg E k ++ copy n None ++ finalSeg E k) p'.

  Lemma copy_split_r_varD : forall E k n p p' A, p >= k -> p' = p + n ->
    E |= p := A -> (initialSeg E k ++ copy n None ++ finalSeg E k) |= p' := A.

  Lemma copy_split_r_varUD : forall E k n p p', p >= k -> p' = p + n ->
    E |= p :! -> (initialSeg E k ++ copy n None ++ finalSeg E k) |= p' :! .

  Lemma copy_split_r_rev_varD : forall E k n p p' A, p >= k -> p' = p + n ->
    (initialSeg E k ++ copy n None ++ finalSeg E k) |= p' := A -> E |= p := A.

  Lemma copy_split_r_rev_varUD : forall E k n p p', p >= k -> p' = p + n ->
    (initialSeg E k ++ copy n None ++ finalSeg E k) |= p' :! -> E |= p :! .

  Lemma equiv_hole_l : forall E k p, p < k ->
    equiv E p (initialSeg E k ++ finalSeg E (S k)) p.

  Lemma hole_l_varD : forall E k p A, p < k -> E |= p := A ->
    (initialSeg E k ++ finalSeg E (S k)) |= p := A.

  Lemma hole_l_varUD : forall E k p, p < k -> E |= p :! ->
    (initialSeg E k ++ finalSeg E (S k)) |= p :! .

  Lemma hole_l_rev_varD : forall E k p A, p < k ->
    (initialSeg E k ++ finalSeg E (S k)) |= p := A -> E |= p := A.

  Lemma hole_l_rev_varUD : forall E k p, p < k ->
    (initialSeg E k ++ finalSeg E (S k)) |= p :! -> E |= p :! .

  Lemma equiv_hole_r : forall E k p p', p > k -> p = S p' ->
    equiv E p (initialSeg E k ++ finalSeg E (S k)) p'.

  Lemma hole_r_varD : forall E k p p' A, p > k -> p = S p' -> E |= p := A ->
    (initialSeg E k ++ finalSeg E (S k)) |= p' := A.

  Lemma hole_r_varUD : forall E k p p', p > k -> p = S p' -> E |= p :! ->
    (initialSeg E k ++ finalSeg E (S k)) |= p' :! .

  Lemma hole_r_rev_varD : forall E k p p' A, p > k -> p = S p' ->
    (initialSeg E k ++ finalSeg E (S k)) |= p' := A -> E |= p := A.

  Lemma hole_r_rev_varUD : forall E k p p', p > k -> p = S p' ->
    (initialSeg E k ++ finalSeg E (S k)) |= p' :! -> E |= p :! .

  Lemma emptyEnv_empty : emptyEnv EmptyEnv.

  Lemma emptyEnv_tail : forall E, emptyEnv (None :: E) -> emptyEnv E.

  Lemma tail_emptyEnv : forall E, emptyEnv E -> emptyEnv (tail E).

  Lemma emptyEnv_cons : forall E, emptyEnv E -> emptyEnv (None :: E).

  Lemma emptyEnv_copyNone : forall k, emptyEnv (copy k None).

  Lemma emptyEnv_absurd : forall a E P, emptyEnv (Some a :: E) -> P.

  Definition isNotEmpty (e: option SimpleType) := e <> None.

  Lemma isNotEmpty_dec : forall e, {isNotEmpty e} + {~isNotEmpty e}.

  Definition dropEmptySuffix (E: Env) : Env :=
    match find_last isNotEmpty isNotEmpty_dec E with
    | None => EmptyEnv
    | Some i => initialSeg E (S i)
    end.

  Lemma dropSuffix_decl : forall E x A,
    E |= x := A -> dropEmptySuffix E |= x := A.

  Lemma dropSuffix_decl_rev : forall E x A,
    dropEmptySuffix E |= x := A -> E |= x := A.

  Lemma dropSuffix_last : forall E (E' := dropEmptySuffix E),
    length E' = 0 \/ exists A, E' |= pred (length E') := A.

  Fixpoint env_compose (E F: Env) : Env :=
    match E, F with
    | nil, nil => EmptyEnv
    | L, nil => L
    | nil, L => L
    | _::E', Some a::F' => Some a :: env_compose E' F'
    | e1::E', None::F' => e1 :: env_compose E' F'
    end.

  Notation "E [+] F" := (env_compose E F) (at level 50, left associativity).

  Lemma env_sum_empty_l : forall E, EmptyEnv [+] E = E.

  Lemma env_sum_empty_r : forall E, E [+] EmptyEnv = E.

  Hint Rewrite env_sum_empty_l env_sum_empty_r : terms.

  Lemma env_sum_assoc : forall (E1 E2 E3: Env),
    E1 [+] E2 [+] E3 = E1 [+] (E2 [+] E3).

  Lemma tail_distr_sum : forall E1 E2, tail (E1 [+] E2) = tail E1 [+] tail E2.

  Lemma env_sum_ln_rn : forall E1 E2 x,
    E1 |= x :! -> E2 |= x :! -> E1 [+] E2 |= x :!.

  Lemma env_sumn_ln : forall x E1 E2, E1 [+] E2 |= x :! -> E1 |= x :! .

  Lemma env_sumn_rn : forall x E1 E2, E1 [+] E2 |= x :! -> E2 |= x :! .

  Lemma env_sum_ry : forall E1 E2 x A, E2 |= x := A -> E1 [+] E2 |= x := A.

  Lemma env_sum_right : forall E1 E2 x A1 A2,
    E1 |= x := A1 -> E2 [+] E1 |= x := A2 -> A1 = A2.

  Lemma env_sum_ly_rn : forall E1 E2 x A,
    E1 |= x := A -> E2 |= x :! -> E1 [+] E2 |= x := A.

  Lemma env_sum_length : forall El Er,
    length (El [+] Er) = Max.max (length El) (length Er).

  Definition env_comp_on E F x : Prop :=
    forall A B, E |= x := A -> F |= x := B -> A = B.

  Lemma env_comp_on_sym : forall E1 E2 x,
    env_comp_on E1 E2 x -> env_comp_on E2 E1 x.

  Definition env_comp E F : Prop := forall x, env_comp_on E F x.

  Notation "E [<->] F" := (env_comp E F) (at level 70).

  Lemma env_comp_refl : forall E, E [<->] E.

  Lemma env_comp_sym : forall E1 E2, E1 [<->] E2 -> E2 [<->] E1.

  Lemma env_comp_empty : forall E, E [<->] EmptyEnv.

  Lemma env_comp_empty_r : forall E, EmptyEnv [<->] E.

  Lemma env_comp_dropSuffix : forall E1 E2,
    E1 [<->] dropEmptySuffix E2 -> E1 [<->] E2.

  Hint Immediate env_comp_refl env_comp_empty env_comp_empty_r : terms.

  Lemma env_comp_tail : forall e1 e2 E1 E2,
    (e1::E1) [<->] (e2::E2) -> E1 [<->] E2.

  Lemma env_comp_cons : forall e1 e2 E1 E2, E1 [<->] E2 ->
    (e1 = e2 \/ e1 = None \/ e2 = None) -> (e1::E1) [<->] (e2::E2).

  Lemma env_comp_single : forall A x E, (E |= x :! \/ E |= x := A) ->
    (copy x None ++ A [#] EmptyEnv) [<->] E.

  Hint Resolve env_comp_cons : terms.

  Lemma env_sum_ly : forall E1 E2 x A, env_comp_on E1 E2 x ->
    E1 |= x := A -> E1 [+] E2 |= x := A.

  Lemma typing_ext_env_l : forall Pt E E' A,
    E |- Pt := A -> E' [+] E |- Pt := A.

  Lemma typing_ext_env_r : forall Pt E E' A,
    E [<->] E' -> E |- Pt := A -> E [+] E' |- Pt := A.

  Fixpoint env_subtract (E F: Env) : Env :=
  match E, F with
  | nil, _ => EmptyEnv
  | E, nil => E
  | None :: E', _ :: F' => None :: env_subtract E' F'
  | Some e :: E', None :: F' => Some e :: env_subtract E' F'
  | Some e :: E', Some f :: F' => None :: env_subtract E' F'
  end.

  Notation "E [-] F" := (env_subtract E F) (at level 50, left associativity).

  Lemma env_sub_empty : forall E, E [-] EmptyEnv = E.

  Hint Rewrite env_sub_empty : terms.

  Lemma env_sub_Empty : forall E1 E2, emptyEnv E2 -> E1 [-] E2 = E1.

  Lemma env_sub_ln : forall E E' x, E |= x :! -> E [-] E' |= x :!.

  Lemma env_sub_ry : forall E E' x A, E' |= x := A -> E [-] E' |= x :!.

  Lemma env_sub_ly_rn : forall E E' x A,
    E |= x := A -> E' |= x :! -> E [-] E' |= x := A.

  Lemma env_sub_suby_rn : forall E E' x A, E [-] E' |= x := A -> E' |= x :! .

  Lemma env_sub_suby_ly : forall E E' x A, E [-] E' |= x := A -> E |= x := A.

  Lemma env_sum_double : forall E, E [+] E = E.

  Hint Rewrite env_sum_double : terms.

  Lemma env_comp_sum_comp_right : forall E1 E2 E3,
    E1 [<->] E2 [+] E3 -> E1 [<->] E3.

  Lemma env_comp_ext_l : forall E1 E2, E1 [+] E2 [<->] E2.

  Lemma env_comp_sub : forall E1 E2 E3, E1 [<->] E2 -> E1 [-] E3 [<->] E2.

  Lemma env_sub_varDecl : forall E1 E2 p A,
    E1 [-] E2 |= p := A -> E1 |= p := A /\ E2 |= p :!.

  Lemma env_sum_varDecl : forall E1 E2 p A, E1 [+] E2 |= p := A ->
    {E1 |= p := A /\ E2 |= p :!} + {E2 |= p := A}.

  Lemma env_comp_sum_comm : forall E1 E2, E1 [<->] E2 -> E1 [+] E2 = E2 [+] E1.

  Lemma env_comp_sum : forall E1 E2 E3,
    E1 [<->] E2 -> E1 [<->] E3 -> E1 [<->] E2 [+] E3.

  Lemma env_sum_disjoint : forall E1 E2,
    (copy (length E1) None ++ E2) [+] E1 = E1 ++ E2.

  Lemma env_sub_sub_sum : forall E1 E2 E3,
    E1 [-] E2 [-] E3 = E1 [-] (E2 [+] E3).

  Lemma env_sub_disjoint : forall E F,
    (forall p, E |= p :! \/ F |= p :!) -> E [-] F = E.

  Lemma env_sum_sub : forall E1 E2 E3, (forall p, E2 |= p :! \/ E3 |= p :!) ->
    E1 [+] E2 [-] E3 = E1 [-] E3 [+] E2.

  Lemma env_extend : forall M A,
    (copy (length M) None ++ A [#] EmptyEnv) [+] M = M ++ A [#] EmptyEnv.

  Lemma env_comp_sum_l : forall M N, M [<->] N [+] M.

  Lemma env_sum_remove_double : forall E1 E2, E1 [+] E2 [+] E1 = E2 [+] E1.

  Lemma env_sub_move : forall E1 E2 E3,
    (E1 [-] E2) [+] (E3 [-] E2) = E1 [+] E3 [-] E2.

  Definition envSubset E F := forall x A, E |= x := A -> F |= x := A.

  Lemma env_subset_empty : forall E, envSubset EmptyEnv E.

  Lemma env_subset_refl : forall E, envSubset E E.

  Lemma env_subset_trans : forall E1 E2 E3,
    envSubset E1 E2 -> envSubset E2 E3 -> envSubset E1 E3.

  Lemma env_subset_cons : forall a E E',
    envSubset E' E -> envSubset (a [#] E') (a [#] E).

  Lemma env_subset_cons_none : forall E E',
    envSubset E' E -> envSubset (None :: E') (None :: E).

  Lemma env_subset_cons_rev : forall a b E E',
    envSubset (a :: E') (b :: E) -> envSubset E' E.

  Lemma env_subset_tail : forall E' E,
    envSubset E' E -> envSubset (tail E') (tail E).

  Lemma env_subset_lowered : forall E E' n, envSubset E E' ->
    envSubset (loweredEnv E n) (loweredEnv E' n).

  Lemma env_subset_comp : forall E E', envSubset E E' -> E [<->] E'.

  Lemma env_subset_as_sum_l : forall E E',
    length E' <= length E -> envSubset E' E -> E = E' [+] E.

  Lemma env_subset_as_sum_r : forall E E',
    length E' <= length E -> envSubset E' E -> E = E [+] E'.

  Lemma env_comp_on_subset : forall El El' Er Er' i,
    env_comp_on El Er i -> envSubset El' El ->
    envSubset Er' Er -> env_comp_on El' Er' i.

  Lemma env_comp_subset : forall El Er El' Er', El [<->] Er ->
    envSubset El' El -> envSubset Er' Er -> El' [<->] Er'.

  Lemma env_subset_sum_l : forall E El Er, El [<->] Er ->
    envSubset E El -> envSubset E (El [+] Er).

  Lemma env_subset_sum_r : forall E El Er,
    envSubset E Er -> envSubset E (El [+] Er).

  Lemma env_subset_sum : forall El El' Er Er', El' [<->] Er' ->
    envSubset El El' -> envSubset Er Er' ->
    envSubset (El [+] Er) (El' [+] Er').

  Lemma env_subset_lsum : forall El Er E,
    envSubset El E -> envSubset Er E -> envSubset (El [+] Er) E.

  Lemma env_subset_sum_req : forall El El' Er,
    envSubset El El' -> envSubset (El [+] Er) (El' [+] Er).

  Lemma env_subset_sum_leq : forall El Er Er', El [<->] Er' ->
    envSubset Er Er' -> envSubset (El [+] Er) (El [+] Er').

  Lemma varDecl_single : forall x A B w,
    (copy x None ++ A[#]EmptyEnv) |= w := B -> A = B /\ x = w.

  Lemma env_subset_single : forall A x E,
    E |= x := A -> envSubset (copy x None ++ A [#] EmptyEnv) E.

  Lemma typing_ext_env : forall Pt E E' A,
    envSubset E' E -> E' |- Pt := A -> E |- Pt := A.

  Lemma env_subset_dropSuffix_length : forall E E', envSubset E' E ->
    length (dropEmptySuffix E') <= length E.

  Lemma varUD_hole : forall E i,
    (initialSeg E i ++ None :: finalSeg E (S i)) |= i :!.

  Lemma varD_hole : forall E i j A, i <> j -> E |= j := A ->
    (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A.

  Lemma varD_hole_env_length : forall E i j A,
    (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A -> length E > j.

  Lemma varD_hole_env_length_j_ge_i : forall E i j A, j >= i ->
    (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A -> length E > i.

  Lemma varD_hole_rev : forall E i j A, i <> j ->
    (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A -> E |= j := A.

  Lemma env_hole_subset : forall E i,
    envSubset (initialSeg E i ++ None :: finalSeg E (S i)) E.

  Definition env_eq E1 E2 := envSubset E1 E2 /\ envSubset E2 E1.

  Notation "E1 [=] E2" := (env_eq E1 E2) (at level 70).

  Lemma env_eq_refl : forall E, E [=] E.

  Lemma env_eq_sym : forall E E', E [=] E' -> E' [=] E.

  Lemma env_eq_trans : forall E1 E2 E3, E1 [=] E2 -> E2 [=] E3 -> E1 [=] E3.

  Lemma env_eq_some_none_absurd : forall E1 E2 A,
    Some A :: E1 [=] None :: E2 -> False.

  Lemma env_eq_some_nil_absurd : forall E1 A,
    Some A :: E1 [=] EmptyEnv -> False.

  Lemma env_eq_tail : forall E1 E2, E1 [=] E2 -> tail E1 [=] tail E2.

  Lemma env_eq_cons : forall a b E E', a = b -> E [=] E' -> a :: E [=] b :: E'.

  Lemma env_eq_cons_inv : forall a b E E', (a :: E) [=] (b :: E') -> E [=] E'.

  Lemma env_eq_cons_inv_hd : forall a b E E', (a :: E) [=] (b :: E') -> a = b.

  Lemma env_eq_comp : forall E1 E2, E1 [=] E2 -> E1 [<->] E2.

  Lemma env_eq_empty_none_empty : EmptyEnv [=] None :: EmptyEnv.

  Lemma env_eq_empty_cons : forall E, None :: E [=] EmptyEnv -> E [=] EmptyEnv.

  Lemma env_eq_empty_cons_rev : forall E,
    E [=] EmptyEnv -> None :: E [=] EmptyEnv.

  Lemma env_eq_empty_tail : forall E n, E [=] E ++ copy n None.

  Lemma env_eq_empty : forall E, emptyEnv E -> E [=] EmptyEnv.

  Lemma env_eq_empty_empty : forall E E', emptyEnv E -> emptyEnv E' -> E [=] E'.

  Lemma env_eq_empty_subset : forall E E', E [=] EmptyEnv -> envSubset E E'.

  Lemma env_eq_def : forall E1 E2,
    (forall i A, E1 |= i := A <-> E2 |= i := A) -> E1 [=] E2.

  Lemma env_equiv_eq : forall E E', E [=] E' -> length E = length E' -> E = E'.

  Hint Immediate env_eq_refl env_eq_sym env_eq_empty_none_empty : terms.

  Instance env_eq_Equivalence : Equivalence env_eq.


  Instance envSubset_morph : Proper (env_eq ==> env_eq ==> iff) envSubset.


  Instance loweredEnv_morph : Proper (env_eq ==> eq ==> env_eq) loweredEnv.


  Instance env_comp_morph : Proper (env_eq ==> env_eq ==> iff) env_comp.


  Instance VarD_morph : Proper (env_eq ==> eq ==> eq ==> iff) VarD.


  Instance VarUD_morph : Proper (env_eq ==> eq ==> iff) VarUD.


  Lemma env_compose_morph_aux0 : forall El Er El' Er',
    (forall El El' Er', El [=] El' -> Er [=] Er' ->
      envSubset (El [+] Er) (El' [+] Er')) ->
    El [=] El' -> None :: Er [=] Er' ->
    envSubset (El [+] (None :: Er)) (El' [+] Er').

  Lemma env_compose_morph_aux : forall El Er El' Er',
    El [=] El' -> Er [=] Er' -> envSubset (El [+] Er) (El' [+] Er').

  Instance env_compose_morph :
    Proper (env_eq ==> env_eq ==> env_eq) env_compose.


  Lemma env_eq_sum : forall El El' Er Er',
    El [=] El' -> Er [=] Er' -> El [+] Er [=] El' [+] Er'.

  Lemma env_eq_subset_sum_l : forall E E', envSubset E' E -> E [=] E' [+] E.

  Lemma env_subset_dropSuffix_eq : forall E, env_eq (dropEmptySuffix E) E.

  Lemma typing_drop_suffix : forall E Pt A,
    E |- Pt := A -> dropEmptySuffix E |- Pt := A.

  Lemma liftedEnv_empty : forall E n k,
    emptyEnv E -> liftedEnv n E k [=] EmptyEnv.

  Lemma liftedEnv_distr_sum_equiv : forall El Er n k,
    liftedEnv n (El [+] Er) k [=] liftedEnv n El k [+] liftedEnv n Er k.

  Lemma liftedEnv_distr_sum : forall El Er n k,
    liftedEnv n (El [+] Er) k = liftedEnv n El k [+] liftedEnv n Er k.

  Lemma loweredEnv_distr_sum_equiv : forall El Er n,
    loweredEnv (El [+] Er) n [=] loweredEnv El n [+] loweredEnv Er n.

  Lemma loweredEnv_distr_sum : forall El Er n,
    loweredEnv (El [+] Er) n = loweredEnv El n [+] loweredEnv Er n.

  Lemma lift_tail : forall E n k,
    liftedEnv n (tail E) k [=] tail (liftedEnv n E (S k)).

  Lemma lower_tail : forall E n,
    loweredEnv (tail E) n = tail (loweredEnv E (S n)).

End TermsEnv.