Qcert.Translation.TcNNRCtoCAMP

Section TNNRCtoCAMP.

Auxiliary definitions and lemmas

  Context {m:basic_model}.

  Lemma PTdot {τc} {Γ Γ₁:tbindings} {τ₁ τ₂ p k} (s:string) pf :
    NoDup (domain Γ₁) →
    RAssoc.lookup equiv_dec Γ₁ s = Some τ ₁ →
    [τ c &Γ ] |= p ; τ ₁ ~> τ ₂ →
    [τ c &Γ ] |= pdot (loop_var s) p ; (Rec k (nnrc_to_pat_env Γ₁) pf ) ~> τ ₂.

  Lemma wf_env_same_domain {env tenv} v :
    bindings_type env tenv → (In v (domain env) ↔ In v (domain tenv)).

  Lemma loop_var_in_nnrc_to_pat_env {B} {tenv v} :
         In v (@domain _ B tenv) ↔
         In (loop_var v) (domain (nnrc_to_pat_env tenv)).

  Lemma nnrc_to_pat_in {B} Γ v :
    In v (@domain _ B Γ) ↔
    In (loop_var v) (domain (nnrc_to_pat_env Γ)).

  Lemma nnrc_to_pat_nodup {B} Γ :
    NoDup (@domain _ B Γ) ↔
    NoDup (domain (nnrc_to_pat_env Γ)).

  Lemma is_list_sorted_nnrc_to_pat_env_nodup {B} {tenv} :
    is_list_sorted ODT_lt_dec (@domain _ B (nnrc_to_pat_env tenv)) = true →
    NoDup (domain tenv).

  Lemma lookup_incl_perm_nodup {A B} {dec:EqDec A eq} {l1 l2:list (A ×B)} :
    Permutation l1 l2 →
    NoDup (@domain A B l1) →
    lookup_incl l1 l2.

  Lemma lookup_equiv_perm_nodup {A B} {dec:EqDec A eq} {l1 l2:list (A ×B)} :
    Permutation l1 l2 →
    NoDup (@domain A B l1) →
    lookup_equiv l1 l2.

  Lemma nnrc_type_context_perm {Γ Γ'} τ n :
    Permutation Γ Γ' →
    NoDup (domain Γ) →
    shadow_free n = true →
    (∀ x, In x (domain Γ) → ¬ In x (nnrc_bound_vars n)) →
    nnrc_type Γ n τ →
    nnrc_type Γ' n τ.

  Lemma rec_cons_sort_nnrc_to_pat_env_pullback {A} a b Γ :
    NoDup (a :: domain Γ) →
      ∃ Γ' : list (string ×A),
     insertion_sort_insert rec_field_lt_dec (loop_var a , b )
       (nnrc_to_pat_env Γ) = nnrc_to_pat_env Γ' ∧
     Permutation ((a , b ) :: Γ) Γ'.

  Lemma rec_sort_nnrc_to_pat_env_pullback {A} (Γ:list (string ×A)) :
    NoDup (domain Γ) →
    ∃ Γ',
      rec_sort (nnrc_to_pat_env Γ) = nnrc_to_pat_env Γ'
      ∧ Permutation Γ Γ'.

  Lemma fresh_bindings_some {A} `{EqDec A eq} (g g1 g2:list (string ×A)) :
         Some g = merge_bindings g1 g2 ↔
         compatible g1 g2 = true ∧
         g = rec_concat_sort g1 g2.

Proving ``forwards'' type preservation: if the compiled pattern is well-typed, then the source nnrc is well-typed (with the same type)

  Lemma nnrc_to_pat_ns_type_preserve n τc Γ τout :
    is_list_sorted ODT_lt_dec (domain (nnrc_to_pat_env Γ)) = true →
    shadow_free n = true →
    (∀ x, In x (domain Γ) → ¬ In x (nnrc_bound_vars n)) →
    nnrc_type Γ n τ out →
    ∀ τ₀,
      [τ c &(nnrc_to_pat_env Γ )] |= (nnrcToPat_ns n ) ; τ ₀ ~> τ out.

  Lemma nnrc_to_pat_ns_top_type_preserve n τc τout :
    shadow_free n = true →
    nnrc_type nil n τ out →
    ∀ τ₀,
      [τ c &nil ] |= (nnrcToPat_ns n ) ; τ ₀ ~> τ out.

  Lemma nnrc_to_pat_type_preserve n τc Γ τout :
    is_list_sorted ODT_lt_dec (domain (nnrc_to_pat_env Γ)) = true →
    nnrc_type Γ n τ out →
    ∀ τ₀,
      [τ c &(nnrc_to_pat_env Γ )] |= (nnrcToPat (domain Γ) n ) ; τ ₀ ~> τ out.

  Lemma fresh_bindings_cons_loop_var a l p :
    fresh_bindings ((loop_var a )::l) p
    ↔ fresh_bindings l p.

  Lemma nnrcToPat_ns_type_ignored_let_binding τc b x xv τ₁ τ₂ n :
    nnrcIsCore n →
    shadow_free n = true →
    RSort.is_list_sorted ODT_lt_dec (domain b) = true →
    fresh_bindings (domain b) (nnrcToPat_ns n) →
    (∀ x, In x (domain b) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
    NoDup (domain b) →
    ¬ In (let_var x) (let_vars (nnrcToPat_ns n)) →
    ¬ In (let_var x) (domain b) →
    ([τ c &b ] |= (nnrcToPat_ns n ) ; τ ₁ ~> τ ₂ ) →
    [τ c &(rec_concat_sort b ((let_var x , xv )::nil))] |= (nnrcToPat_ns n ) ; τ ₁ ~> τ ₂.

  Lemma nnrc_to_pat_ns_let_type_equiv n τc Γ τout :
    nnrcIsCore n →
    is_list_sorted ODT_lt_dec (domain Γ) = true →
    fresh_bindings (domain Γ) (nnrcToPat_ns_let n) →
    shadow_free n = true →
    (∀ x, In x (domain Γ) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
    ∀ τ₀,
      [τ c &Γ ] |= (nnrcToPat_ns n ) ; τ ₀ ~> τ out →
                                   [τ c &Γ ] |= (nnrcToPat_ns_let n ) ; τ ₀ ~> τ out.

  Lemma fresh_bindings_from_tnnrc {A} e l :
    fresh_bindings (@domain _ A (nnrc_to_pat_env e)) l.

  Lemma nnrc_to_pat_let_type_preserve n τc Γ τout :
    nnrcIsCore n →
    is_list_sorted ODT_lt_dec (domain (nnrc_to_pat_env Γ)) = true →
    nnrc_type Γ n τ out →
    ∀ τ₀,
      [τ c &(nnrc_to_pat_env Γ )] |= (nnrcToPat_let (domain Γ) n ) ; τ ₀ ~> τ out.

  Lemma nnrc_to_pat_ns_let_top_type_preserve n τc τout :
    nnrcIsCore n →
    shadow_free n = true →
    nnrc_type nil n τ out →
    ∀ τ₀,
    [τ c &nil ] |= (nnrcToPat_ns_let n ) ; τ ₀ ~> τ out.

Proving ``backwards'' type preservation: if the compiled pattern is well-typed, then the source nnrc is well-typed (with the same type)

  Lemma nnrc_to_pat_ns_type_preserve_back n τc Γ τout :
    nnrcIsCore n →
    is_list_sorted ODT_lt_dec (domain (nnrc_to_pat_env Γ)) = true →
    shadow_free n = true →
    (∀ x, In x (domain Γ) → ¬ In x (nnrc_bound_vars n)) →
    ∀ τ₀,
      [τ c &(nnrc_to_pat_env Γ )] |= (nnrcToPat_ns n ) ; τ ₀ ~> τ out →
                                                     nnrc_type Γ n τ out.

  Lemma nnrc_to_pat_ns_top_type_preserve_back n τc τout :
    nnrcIsCore n →
    shadow_free n = true →
    ∀ τ₀,
      [τ c &nil ] |= (nnrcToPat_ns n ) ; τ ₀ ~> τ out →
                                     nnrc_type nil n τ out.

  Lemma PTmapall_let τc {Γ : tbindings} {τ₁ τ₂ : rtype} {p : pat} :
    NoDup (domain Γ) →
    fresh_bindings (domain Γ) (mapall_let p) →
    ([τ c &Γ ] |= p ; τ ₁ ~> τ ₂ ) → [τ c &Γ ] |= mapall_let p ; Coll τ ₁ ~> Coll τ ₂.

  Lemma PTmapall_let_inv τc {Γ : tbindings} {τ₁ τ₂ : rtype} {p : pat} :
    RSort.is_list_sorted ODT_lt_dec (domain Γ) = true →
    fresh_bindings (domain Γ) (mapall_let p) →
    [τ c &Γ ] |= mapall_let p ; τ ₁ ~> τ ₂ →
                            ∃ τ₁' τ₂',
                              τ ₁ = Coll τ ₁' ∧
                              τ ₂ = Coll τ ₂' ∧
                              ([τ c &Γ ] |= p ; τ ₁' ~> τ ₂').

  Lemma nnrcToPat_ns_type_weaken_let_binding τc b x xv τ₁ τ₂ n :
    nnrcIsCore n →
    shadow_free n = true →
    RSort.is_list_sorted ODT_lt_dec (domain b) = true →
    fresh_bindings (domain b) (nnrcToPat_ns n) →
    (∀ x, In x (domain b) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
    NoDup (domain b) →
    ¬ In (let_var x) (let_vars (nnrcToPat_ns n)) →
    ¬ In (let_var x) (domain b) →
    [τ c &(rec_concat_sort b
                         ((let_var x , xv )::nil))] |= (nnrcToPat_ns n ) ; τ ₁ ~> τ ₂ →
                                                                        [τ c &b ] |= (nnrcToPat_ns n ) ; τ ₁ ~> τ ₂.

  Lemma nnrc_to_pat_ns_let_type_equiv_back n τc Γ τout :
    nnrcIsCore n →
      is_list_sorted ODT_lt_dec (domain Γ) = true →
    fresh_bindings (domain Γ) (nnrcToPat_ns_let n) →
    shadow_free n = true →
    (∀ x, In x (domain Γ) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
    ∀ τ₀,
      [τ c &Γ ] |= (nnrcToPat_ns_let n ) ; τ ₀ ~> τ out →
                                       [τ c &Γ ] |= (nnrcToPat_ns n ) ; τ ₀ ~> τ out.

  Lemma nnrc_to_pat_let_type_preserve_back n τc Γ τout :
    nnrcIsCore n →
    is_list_sorted ODT_lt_dec (domain (nnrc_to_pat_env Γ)) = true →
    ∀ τ₀,
      [τ c &(nnrc_to_pat_env Γ )] |= (nnrcToPat_let (domain Γ) n ) ; τ ₀ ~> τ out →
      nnrc_type Γ n τ out.

  Lemma nnrc_to_pat_ns_let_top_type_preserve_back n τc τout :
    nnrcIsCore n →
    shadow_free n = true →
    ∀ τ₀,
      [τ c &nil ] |= (nnrcToPat_ns_let n ) ; τ ₀ ~> τ out →
                                         nnrc_type nil n τ out.

Theorem 7.4, NNRC<->CAMP. Final iff Theorem of type preservation for the translation from NNRC back to Patterns

  Theorem nnrc_to_pat_let_top_type_preserve_iff τc Γ n τout τ₀:
    nnrcIsCore n →
    is_list_sorted ODT_lt_dec (domain (nnrc_to_pat_env Γ)) = true →
    (nnrc_type Γ n τ out ↔
    [τ c &(nnrc_to_pat_env Γ )] |= (nnrcToPat_let (domain Γ) n ) ; τ ₀ ~> τ out ).

End TNNRCtoCAMP.