Qcert.NNRC.Lang.NNRCShadow

Section NNRCShadow.





  Context {fruntime:foreign_runtime}.

  Lemma nnrc_ext_eval_remove_duplicate_env {h:brand_relation_t} l v x l' x' l'' e :
    @nnrc_ext_eval _ h (l ++ (v,x)::l' ++ (v,x')::l'') e =
    @nnrc_ext_eval _ h (l ++ (v,x)::l' ++ l'') e.

  Lemma nnrc_ext_eval_remove_duplicate_env_weak {h:list (string×string)} v1 v2 x x' x'' l e :
    @nnrc_ext_eval _ h ((v1,x)::(v2,x')::(v1,x'')::l) e =
    @nnrc_ext_eval _ h ((v1,x)::(v2,x')::l) e.

  Lemma nnrc_ext_eval_remove_duplicate_env_weak_cons {h:list (string×string)} v1 v2 x x' x'' l e :
    @nnrc_ext_eval _ h ((v1,x)::(v2,x')::(v2,x'')::l) e =
    @nnrc_ext_eval _ h ((v1,x)::(v2,x')::l) e.

  Lemma nnrc_ext_eval_remove_free_env {h:list (string×string)} l v x l' e :
          ¬ In v (nnrc_free_vars e) →
          @nnrc_ext_eval _ h (l ++ (v,x)::l') e = @nnrc_ext_eval _ h (l ++ l') e.

  Lemma nnrc_ext_eval_remove_free_env_weak {h:list (string×string)} v1 x1 v x e :
    ¬ In v (nnrc_free_vars e) →
    @nnrc_ext_eval _ h ((v1,x1)::(v,x)::nil) e = @nnrc_ext_eval _ h ((v1,x1)::nil) e.

  Lemma nnrc_ext_eval_swap_neq {h:list (string×string)} l1 v1 x1 v2 x2 l2 e : v1 ≠ v2 →
           @nnrc_ext_eval _ h (l1++(v1,x1)::(v2,x2)::l2) e =
           @nnrc_ext_eval _ h (l1++(v2,x2)::(v1,x1)::l2) e.

  Lemma nnrc_ext_eval_subst_dunit {h:list (string×string)} env e v :
    @nnrc_ext_eval _ h ((v,dunit)::env) e =
    @nnrc_ext_eval _ h env (nnrc_subst e v (NNRCConst dunit)).

  Lemma nnrc_ext_eval_cons_subst {h:list (string×string)} e env v x v' :
    ¬ (In v' (nnrc_free_vars e)) →
    ¬ (In v' (nnrc_bound_vars e)) →
    @nnrc_ext_eval _ h ((v',x)::env) (nnrc_subst e v (NNRCVar v')) =
    @nnrc_ext_eval _ h ((v,x)::env) e.

  Lemma nnrc_ext_eval_equiv_free_in_env:
    ∀ n,
    ∀ env1 env2,
      (∀ x, In x (nnrc_free_vars n) → lookup equiv_dec env1 x = lookup equiv_dec env2 x) →
      ∀ h,
        @nnrc_ext_eval _ h env1 n = @nnrc_ext_eval _ h env2 n.

  Lemma nnrc_ext_eval_equiv_env:
    ∀ n,
    ∀ env1 env2,
      (∀ x, lookup equiv_dec env1 x = lookup equiv_dec env2 x) →
      ∀ h,
        @nnrc_ext_eval _ h env1 n = @nnrc_ext_eval _ h env2 n.

  Lemma nnrc_no_free_vars_eval_equiv_env:
    ∀ n,
    ∀ env1 env2,
      nnrc_free_vars n = nil →
      ∀ h,
        @nnrc_ext_eval _ h env1 n = @nnrc_ext_eval _ h env2 n.

  Lemma nnrc_ext_eval_single_context_var_uncons h env n v d:
    lookup equiv_dec env v = Some d →
    @nnrc_ext_eval _ h env n = @nnrc_ext_eval _ h ((v, d) :: env) n.

  Lemma nnrc_ext_eval_single_context_var h env n v d:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    lookup equiv_dec env v = Some d →
    @nnrc_ext_eval _ h ((v, d) :: nil) n = @nnrc_ext_eval _ h env n.

  Lemma nnrc_ext_eval_single_context_var_cons h env n v d:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    @nnrc_ext_eval _ h ((v, d) :: nil) n = @nnrc_ext_eval _ h ((v,d)::env) n.

  Lemma nnrc_ext_eval_single_context_var_cons_keepone h env n v d v1 d1:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    @nnrc_ext_eval _ h ((v, d) :: (v1, d1) :: nil) n =
    @nnrc_ext_eval _ h ((v,d) :: (v1,d1) :: env) n.

  Lemma nnrc_ext_eval_single_context_var_two_cons h env n v1 d1 v2 d2 :
    (∀ x, In x (nnrc_free_vars n) → x = v1 ∨ x = v2) →
    @nnrc_ext_eval _ h ((v1,d1) :: (v2,d2) :: nil) n =
    @nnrc_ext_eval _ h ((v1,d1) :: (v2,d2) :: env) n.

  Lemma nnrc_ext_eval_single_context_var_cons_rmap h env n v l:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    rmap (fun d ⇒ @nnrc_ext_eval _ h ((v, d) :: nil) n) l =
    rmap (fun d ⇒ @nnrc_ext_eval _ h ((v,d)::env) n) l.

  Lemma nnrc_ext_eval_single_context_var_cons_keepone_rmap h env n v v1 d1 l:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    rmap (fun d ⇒ @nnrc_ext_eval _ h ((v, d) :: (v1,d1) :: nil) n) l =
    rmap (fun d ⇒ @nnrc_ext_eval _ h ((v,d) :: (v1,d1) :: env) n) l.

  Lemma rmap_skip_free_var h v1 v2 d2 n l:
    ¬ In v2 (nnrc_free_vars n) →
    (rmap (fun d : data ⇒ @nnrc_ext_eval _ h ((v1, d) :: (v2, d2) :: nil) n) l) =
    (rmap (fun d : data ⇒ @nnrc_ext_eval _ h ((v1, d) :: nil) n) l).

  Lemma nnrc_ext_eval_cons_subst_disjoint {h: list (string×string)} e e' env v d :
    disjoint (nnrc_bound_vars e) (nnrc_free_vars e') →
         @nnrc_ext_eval _ h env e' = Some d →
         @nnrc_ext_eval _ h ((v,d)::env) e = @nnrc_ext_eval _ h env (nnrc_subst e v e').

  Lemma nnrc_pick_name_neq_nfree sep renamer avoid v e :
    v =/= nnrc_pick_name sep renamer avoid v e →
    ¬ In (nnrc_pick_name sep renamer avoid v e) (nnrc_free_vars e).

  Lemma nnrc_ext_eval_cons_rename_pick h sep renamer avoid v e d env:
    @nnrc_ext_eval _ h ((nnrc_pick_name sep renamer avoid v e, d) :: env)
             (nnrc_rename_lazy e v (nnrc_pick_name sep renamer avoid v e)) =
    @nnrc_ext_eval _ h ((v, d) :: env) e.

  Theorem unshadow_ext_eval {h:list (string×string)} sep renamer avoid e env :
    @nnrc_ext_eval _ h env (unshadow sep renamer avoid e) = @nnrc_ext_eval _ h env e.

  Lemma nnrc_pick_name_id_nin_eq sep avoid v e :
    ¬ In v (nnrc_bound_vars e) →
    ¬ In v avoid →
    (nnrc_pick_name sep id avoid v e) = v.

  Lemma unshadow_id_idempotent sep renamer1 avoid (e:nnrc)
    : unshadow sep id avoid (unshadow sep renamer1 avoid e) = unshadow sep renamer1 avoid e.

  Definition nnrc_unshadow_sep := "$"%string.
  Definition unshadow_simpl := unshadow nnrc_unshadow_sep id.

  Definition nnrc_substlist_subst (substlist:list (var×var)) (e:nnrc) :=
    List.fold_left
      (fun e (subst: var × var) ⇒
         let (x, x') := subst in
         nnrc_subst e x (NNRCVar x'))
      substlist e.

End NNRCShadow.