Module TcNRAEnv

Section TcNRAEnv.
  Require Import String.
  Require Import List.
  Require Import Compare_dec.
  Require Import Program.

  Require Import Utils BasicSystem.

  Require Import cNRAEnv cNRAEnvEq.

  Local Open Scope nraenv_core_scope.
  
  Section typ.
    Context {m:basic_model}.
    Context (τconstants:tbindings).
  
  Inductive nraenv_core_type : nraenv_core -> rtype -> rtype -> rtype -> Prop :=
  | ANTID {τenv τ} :
      nraenv_core_type ANID τenv τ τ
  | ANTConst {τenv τin τout} c :
      data_type (normalize_data brand_relation_brands c) τout -> nraenv_core_type (ANConst c) τenv τin τout
  | ANTBinop {τenv τin τ₁ τ₂ τout} b op1 op2 :
      binOp_type b τ₁ τ₂ τout ->
      nraenv_core_type op1 τenv τin τ₁ ->
      nraenv_core_type op2 τenv τin τ₂ ->
      nraenv_core_type (ANBinop b op1 op2) τenv τin τout
  | ANTUnop {τenv τin τ τout} u op :
      unaryOp_type u τ τout ->
      nraenv_core_type op τenv τin τ ->
      nraenv_core_type (ANUnop u op) τenv τin τout
  | ANTMap {τenv τin τ₁ τ₂} op1 op2 :
      nraenv_core_type op1 τenv τ₁ τ₂ ->
      nraenv_core_type op2 τenv τin (Coll τ₁) ->
      nraenv_core_type (ANMap op1 op2) τenv τin (Coll τ₂)
  | ANTMapConcat {τenv τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
      nraenv_core_type op1 τenv (Rec Closed τ₁ pf1) (Coll (Rec Closed τ₂ pf2)) ->
      nraenv_core_type op2 τenv τin (Coll (Rec Closed τ₁ pf1)) ->
      rec_concat_sort τ₁ τ₂ = τ₃ ->
      nraenv_core_type (ANMapConcat op1 op2) τenv τin (Coll (Rec Closed τ₃ pf3))
  | ANTProduct {τenv τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
      nraenv_core_type op1 τenv τin (Coll (Rec Closed τ₁ pf1)) ->
      nraenv_core_type op2 τenv τin (Coll (Rec Closed τ₂ pf2)) ->
      rec_concat_sort τ₁ τ₂ = τ₃ ->
      nraenv_core_type (ANProduct op1 op2) τenv τin (Coll (Rec Closed τ₃ pf3))
  | ANTSelect {τenv τin τ} op1 op2 :
      nraenv_core_type op1 τenv τ Bool ->
      nraenv_core_type op2 τenv τin (Coll τ) ->
      nraenv_core_type (ANSelect op1 op2) τenv τin (Coll τ)
  | ANTDefault {τenv τin τ} op1 op2 :
      nraenv_core_type op1 τenv τin (Coll τ) ->
      nraenv_core_type op2 τenv τin (Coll τ) ->
      nraenv_core_type (ANDefault op1 op2) τenv τin (Coll τ)
  | ANTEither {τenv τl τr τout} opl opr :
      nraenv_core_type opl τenv τl τout ->
      nraenv_core_type opr τenv τr τout ->
      nraenv_core_type (ANEither opl opr) τenv (Either τl τr) τout
  | ANTEitherConcat {τenv τin rll pfl rlr pfr rlo pfo lo ro} op1 op2 pflo pfro :
      nraenv_core_type op1 τenv τin (Either (Rec Closed rll pfl) (Rec Closed rlr pfr)) ->
      nraenv_core_type op2 τenv τin (Rec Closed rlo pfo) ->
      rec_concat_sort rll rlo = lo ->
      rec_concat_sort rlr rlo = ro ->
      nraenv_core_type (ANEitherConcat op1 op2) τenv τin (Either (Rec Closed lo pflo) (Rec Closed ro pfro))
  | ANTApp {τenv τin τ1 τ2} op2 op1 :
      nraenv_core_type op1 τenv τin τ1 ->
      nraenv_core_type op2 τenv τ1 τ2 ->
      nraenv_core_type (ANApp op2 op1) τenv τin τ2
  | ANTGetConstant {τenv τin τout} s :
      tdot τconstants s = Some τout ->
      nraenv_core_type (ANGetConstant s) τenv τin τout
  | ANTEnv {τenv τin} :
      nraenv_core_type ANEnv τenv τin τenv
  | ANTAppEnv {τenv τenv' τin τ2} op2 op1 :
      nraenv_core_type op1 τenv τin τenv' ->
      nraenv_core_type op2 τenv' τin τ2 ->
      nraenv_core_type (ANAppEnv op2 op1) τenv τin τ2
  | ANTMapEnv {τenv τin τ₂} op1 :
      nraenv_core_type op1 τenv τin τ₂ ->
      nraenv_core_type (ANMapEnv op1) (Coll τenv) τin (Coll τ₂).
  End typ.

  Notation "Op ▷ A >=> B ⊣ C ; E" := (nraenv_core_type C Op E A B) (at level 70).


  Context {m:basic_model}.
  
  Lemma rmap_typed {τc} {τenv τ₁ τ₂ : rtype} c (op1 : nraenv_core) (env:data) (dl : list data) :
    (bindings_type c τc) ->
    (env ▹ τenv) ->
    (Forall (fun d : data => data_type d τ₁) dl) ->
    (op1 ▷ τ₁ >=> τ₂ ⊣ τc; τenv) ->
    (forall d : data,
       data_type d τ₁ -> exists x : data, brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c; env = Some x /\ x ▹ τ₂) ->
    exists x : list data, (rmap (nraenv_core_eval brand_relation_brands c op1 env) dl = Some x) /\ data_type (dcoll x) (Coll τ₂).

  Lemma rmap_env_typed {τc} {τenv τ₁ τ₂ : rtype} c (op1 : nraenv_core) (x0:data) (dl : list data) :
    bindings_type c τc ->
    (x0 ▹ τ₁) ->
    (Forall (fun d : data => data_type d τenv) dl) ->
    (op1 ▷ τ₁ >=> τ₂ ⊣ τc;τenv) ->
    (forall env : data,
       data_type env τenv ->
       forall d : data,
         data_type d τ₁ ->
         exists x : data, brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c;env = Some x /\ data_type x τ₂) ->
    exists x : list data, (rmap (fun env' => (nraenv_core_eval brand_relation_brands c op1 env' x0)) dl = Some x) /\ data_type (dcoll x) (Coll τ₂).

  Lemma recover_rec k d r τ pf:
    data_type d r ->
    ` r =
    Rec₀ k
      (map
         (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
            (fst x, ` (snd x))) τ) ->
    data_type d (Rec k τ pf).

  Lemma recover_rec_forall k l r τ pf:
    Forall (fun d : data => data_type d r) l ->
    ` r =
    Rec₀ k
      (map
         (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
            (fst x, ` (snd x))) τ) ->
    Forall (fun d : data => data_type d (Rec k τ pf)) l.

  Lemma omap_concat_typed_env
        (τenv:rtype) (τ₁ τ₂ τ₃: list (string * rtype)) (env:data) (dl2: list data)
        (x : list (string * data)) pf1 pf2 pf3:
    (data_type env τenv) ->
    (forall x : data, In x dl2 -> data_type x (Rec Closed τ₂ pf2)) ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    data_type (drec x) (Rec Closed τ₁ pf1) ->
    (exists y : list data,
       rmap (fun x1 : data => orecconcat (drec x) x1) dl2
       = Some y /\ data_type (dcoll y) (Coll (Rec Closed τ₃ pf3))).

  Lemma rproduct_typed_env {τenv:rtype} {τ₁ τ₂ τ₃: list (string * rtype)} (env:data) (dl dl0: list data) pf1 pf2 pf3:
    data_type env τenv ->
    Forall (fun d : data => data_type d (Rec Closed τ₂ pf2)) dl0 ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    exists x : list data, (rproduct dl dl0 = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).
  
  Lemma data_type_concat l1 l2 τ:
    data_type (dcoll l1) (Coll τ) ->
    data_type (dcoll l2) (Coll τ) ->
    data_type (dcoll (l1 ++ l2)) (Coll τ).

  Lemma rmap_concat_typed_env {τc} {τenv:rtype} {τ₁ τ₂ τ₃ : list (string * rtype)} (op1 : nraenv_core) c (env:data) (dl: list data) pf1 pf2 pf3:
    bindings_type c τc ->
    env ▹ τenv ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    (op1 ▷ Rec Closed τ₁ pf1 >=> Coll (Rec Closed τ₂ pf2) ⊣ τc;τenv) ->
    (forall d : data,
                data_type d (Rec Closed τ₁ pf1) ->
                exists x : data,
                   brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c;env = Some x /\ data_type x (Coll (Rec Closed τ₂ pf2))) ->
    exists x : list data, (rmap_concat (nraenv_core_eval brand_relation_brands c op1 env) dl = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).

  Lemma rmap_concat_typed2_env {τc} {τenv:rtype} {τ₁ τ₂ τ₃ : list (string * rtype)} τin c (op1 : nraenv_core) (env:data) y (dl: list data) pf1 pf2 pf3:
    bindings_type c τc ->
    env▹ τenv ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    (op1 ▷ τin >=> Coll (Rec Closed τ₂ pf2) ⊣ τc;τenv) ->
    (forall d : data,
                data_type d (Rec Closed τ₁ pf1) ->
                exists x : data,
                   brand_relation_brands ⊢ₑ op1 @ₑ y ⊣ c;env = Some x /\ data_type x (Coll (Rec Closed τ₂ pf2))) ->
    exists x : list data, (rmap_concat (fun z => brand_relation_brands ⊢ₑ op1@ₑ y ⊣ c;env) dl = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).


  Theorem typed_nraenv_core_yields_typed_data {τc} {τenv τin τout} c (env:data) (d:data) (op:nraenv_core):
    bindings_type c τc ->
    (env ▹ τenv) -> (d ▹ τin) -> (op ▷ τin >=> τout ⊣ τc;τenv) ->
    (exists x, (brand_relation_brands ⊢ₑ op @ₑ d ⊣ c;env = Some x /\ (x ▹ τout))).



  Definition typed_nraenv_core_total {τc} {τenv τin τout} (op:nraenv_core) (HOpT: op ▷ τin >=> τout ⊣ τc;τenv) c (env:data) (d:data)
    (dt_c: bindings_type c τc) :
    (env ▹ τenv) ->
    (d ▹ τin) ->
    { x:data | x ▹ τout }.

  Definition tnraenv_core_eval {τc} {τenv τin τout} (op:nraenv_core) (HOpT: op ▷ τin >=> τout ⊣ τc;τenv) c (env:data) (d:data)
             (dt_c: bindings_type c τc) :
    (env ▹ τenv) -> (d ▹ τin) -> data.

  Require Import NRASystem.
  

  Definition nra_context_type tbind tpid : rtype :=
    Rec Closed (("PBIND"%string,tbind) :: ("PDATA"%string,tpid) :: nil) (eq_refl _).

  Lemma ATdot {p s τc τin τ pf τout}:
      p ▷ τin >=> Rec Closed τ pf ⊣ τc ->
      tdot τ s = Some τout ->
      AUnop (ADot s) p ▷ τin >=> τout ⊣ τc.

  Lemma ATdot_inv {p s τc τin τout}:
      AUnop (ADot s) p ▷ τin >=> τout ⊣ τc ->
      exists τ pf k,
      p ▷ τin >=> Rec k τ pf ⊣ τc /\
      tdot τ s = Some τout.

  Lemma ATnra_data τc τ τin :
    nra_data ▷ nra_context_type τ τin >=> τin ⊣ τc.

  Lemma ATnra_data_inv' k τc τ τin pf τout:
      nra_data ▷ Rec k [("PBIND"%string, τ); ("PDATA"%string, τin)] pf >=> τout ⊣ τc ->
      τin = τout.
    
  Lemma ATnra_data_inv τc τ τin τout:
    nra_data ▷ nra_context_type τ τin >=> τout ⊣ τc ->
    τin = τout.

  Hint Constructors nra_type unaryOp_type binOp_type.
  Hint Resolve ATdot ATnra_data.
  
  Lemma ATunnest_two (s1 s2:string) (op:NRA.nra) τc τin τ₁ pf1 τs τrem pf2 :
    op ▷ τin >=> (Coll (Rec Closed τ₁ pf1)) ⊣ τc ->
    tdot τ₁ s1 = Some (Coll τs) ->
    τrem = (rremove (rec_concat_sort τ₁ ((s2,τs)::nil)) s1) ->
    NRAExt.unnest_two s1 s2 op ▷
               τin >=> Coll (Rec Closed τrem pf2) ⊣ τc.

  Ltac nra_inverter :=
  match goal with
    | [H:Coll _ = Coll _ |- _] => inversion H; clear H
    | [H: `?τ₁ = Coll₀ (`?τ₂) |- _] => rewrite (Coll_right_inv τ₁ τ₂) in H; subst
    | [H: Coll₀ (`?τ₂) = `?τ₁ |- _] => symmetry in H
    | [H:@nra_type _ _ AID _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AMap _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AMapConcat _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AEither _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AEitherConcat _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (ARecEither _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (ADefault _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AApp _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AProduct _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (ASelect _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AUnop _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (ABinop _ _ _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (AConst _) _ _ |- _ ] => inversion H; clear H
    | [H:@nra_type _ _ (nra_data) _ _ |- _ ] => apply ATnra_data_inv' in H
    | [H:@nra_type _ _ (nra_data) (nra_context_type _ _) _ |- _ ] => apply ATnra_data_inv in H
    | [H: (_,_) = (_,_) |- _ ] => inversion H; clear H
    | [H: map (fun x2 : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                 (fst x2, ` (snd x2))) ?x0 = [] |- _] => apply (map_rtype_nil x0) in H; simpl in H; subst
    | [H: (map
             (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                (fst x, proj1_sig (snd x))) _)
          =
          (map
             (fun x' : string * {τ₀' : rtype₀ | wf_rtype₀ τ₀' = true} =>
                (fst x', proj1_sig (snd x'))) _) |- _ ] =>
      apply map_rtype_fequal in H; trivial
    | [H:Rec _ _ _ = Rec _ _ _ |- _ ] => generalize (Rec_inv H); clear H; intro H; try subst
    | [H: context [(_::nil) = map
                                (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                                   (fst x, proj1_sig (snd x))) _] |- _] => symmetry in H
                                                                                         
    | [H: context [map
                     (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                        (fst x, proj1_sig (snd x))) _ = (_::_) ] |- _] => apply map_eq_cons in H;
        destruct H as [? [? [? [??]]]]
    | [H: Coll₀ _ = Coll₀ _ |- _ ] => inversion H; clear H
    | [H: Rec₀ _ _ = Rec₀ _ _ |- _ ] => inversion H; clear H
    | [H: nraenv_core_type _ _ (snd ?x) _ |- _] => destruct x; simpl in *; subst
    | [H:unaryOp_type AColl _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type AFlatten _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type (ARec _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type (ADot _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type (ARecRemove _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type ARight _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type ALeft _ _ |- _ ] => inversion H; clear H; subst
    | [H:binOp_type AConcat _ _ _ |- _ ] => inversion H; clear H
    | [H:binOp_type AAnd _ _ _ |- _ ] => inversion H; clear H
    | [H:binOp_type AMergeConcat _ _ _ |- _ ] => inversion H; clear H
  end; try rtype_equalizer; try assumption; try subst; simpl in *; try nra_inverter.

  Lemma ATunnest_two_inv (s1 s2:string) (op:NRA.nra) τc τin rec :
    unnest_two s1 s2 op ▷
                       τin >=> Coll rec ⊣ τc ->
    exists τ₁ pf1 τs τrem pf2,
    op ▷ τin >=> (Coll (Rec Closed τ₁ pf1)) ⊣ τc /\
    tdot τ₁ s1 = Some (Coll τs) /\
    rec = (Rec Closed τrem pf2) /\
    τrem = (rremove (rec_concat_sort τ₁ ((s2,τs)::nil)) s1).
    
  Lemma ATRecEither s τc τl τr pf1 pf2:
    nra_type τc (ARecEither s) (Either τl τr)
             (Either
                (Rec Closed ((s,τl)::nil) pf1)
                (Rec Closed ((s,τr)::nil) pf2)).
  
  Theorem typed_nraenv_core_to_typed_nra {τc} {τenv τin τout} (op:nraenv_core):
    (nraenv_core_type τc op τenv τin τout) -> (nra_type τc (nra_of_nraenv_core op) (nra_context_type τenv τin) τout).

  Lemma fold_nra_context_type (env d: {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true}) pf :
    Rec Closed [("PBIND"%string, env); ("PDATA"%string, d)] pf
    = nra_context_type env d.

  Ltac defst l
    := match l with
       | @nil (string*rtype₀) => constr:(@nil (string*rtype))
       | cons (?x,proj1_sig ?y) ?l' =>
         let l'' := defst l' in
         constr:(cons (x,y) l'')
       end.
  
  Ltac rec_proj_simpler
    := repeat
         match goal with
         | [H: Rec₀ ?k ?l = proj1_sig ?τ |- _ ] => symmetry in H
         | [H: proj1_sig ?τ = Rec₀ ?k ?l |- _ ] =>
           let ll := defst l in
           let HH:=fresh "eqq" in
           generalize (@Rec₀_eq_proj1_Rec _ _ τ k ll); intros HH;
           simpl in HH; specialize (HH H); clear H; destruct HH;
           try subst τ
         end.
  
  Require Import Eqdep_dec.
  Require Import Bool.
  
  Lemma UIP_bool {a b:bool} (pf1 pf2:a = b) : pf1 = pf2.

  Ltac nra_inverter_ext
    :=
      simpl in *; match goal with
                  | [H:@nra_type _ _ (unnest_two _ _ _) _ (Coll _) |- _ ] => apply ATunnest_two_inv in H;
                                                                           destruct H as [? [? [? [? [? [? [?[??]]]]]]]]
                  | [H: prod _ _ |- _ ] => destruct H; simpl in *; try subst
                  | [H: context [Rec Closed [("PBIND"%string, ?env); ("PDATA"%string, ?d)] ?pf ] |- _ ] => unfold rtype in H; rewrite (fold_nra_context_type env d pf) in H
                  | [H: Rec₀ ?k ?l = proj1_sig ?τ |- _ ] => symmetry in H
                  | [H: proj1_sig ?τ = Rec₀ ?k ?l |- _ ] =>
                    let ll := defst l in
                    let HH:=fresh "eqq" in
                    generalize (@Rec₀_eq_proj1_Rec _ _ τ k ll); intros HH;
                    simpl in HH; specialize (HH H); clear H; destruct HH;
                    try subst τ
                  | [H:proj1_sig _ =
                       Rec₀ Closed
                            (map
                               (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                                  (fst x, ` (snd x))) _) |- _ ]
                    => let Hpf := fresh "spf" in
                       apply Rec₀_eq_proj1_Rec in H; destruct H as [? Hpf]
                  | [H1:@eq bool ?a ?b,
                        H2:@eq bool ?a ?b |- _] => destruct (UIP_bool H1 H2)
                  end.

  Ltac nra_inverter2 :=
    repeat (try unfold nra_wrap, nra_wrap_a1, nra_wrap_bind_a1, nra_context, nra_double, nra_bind, nra_wrap in *; (nra_inverter_ext || nra_inverter); try subst).

  Ltac tdot_inverter :=
    repeat
      match goal with
        | [H: tdot _ _ = Some _ |- _ ] =>
          let HH:= fresh "eqq" in
          inversion H as [HH];
            match type of HH with
              | ?x1 = ?x2 => try (subst x2 || subst x1); clear H
              | _ => fail 1
            end
      end.

  Lemma typed_nraenv_core_to_typed_nra_inv' {k τc τenv τin τout pf} (op:nraenv_core):
    nra_type τc (nra_of_nraenv_core op) (Rec k [("PBIND"%string, τenv); ("PDATA"%string, τin)] pf) τout ->
    nraenv_core_type τc op τenv τin τout.
  
  Theorem typed_nraenv_core_to_typed_nra_inv {τc} {τenv τin τout} (op:nraenv_core):
    nra_type τc (nra_of_nraenv_core op) (nra_context_type τenv τin) τout ->
    nraenv_core_type τc op τenv τin τout.

  Lemma typed_nraenv_core_const_sort_f {τc op τenv τin τout} :
    nraenv_core_type (rec_sort τc) op τenv τin τout ->
    nraenv_core_type τc op τenv τin τout.

  Lemma typed_nraenv_core_const_sort_b {τc op τenv τin τout} :
      nraenv_core_type τc op τenv τin τout ->
      nraenv_core_type (rec_sort τc) op τenv τin τout.

  Lemma typed_nraenv_core_const_sort τc op τenv τin τout :
    nraenv_core_type (rec_sort τc) op τenv τin τout <->
    nraenv_core_type τc op τenv τin τout.

End TcNRAEnv.


Notation "Op ▷ A >=> B ⊣ C ; E" := (nraenv_core_type C Op E A B) (at level 70).
Notation "Op @▷ d ⊣ C ; e" := (tnraenv_core_eval C Op e d) (at level 70).

  
Hint Constructors nraenv_core_type.
Hint Constructors unaryOp_type.
Hint Constructors binOp_type.

Ltac nraenv_core_inverter :=
  match goal with
    | [H:Coll _ = Coll _ |- _] => inversion H; clear H
    | [H: `?τ₁ = Coll₀ (`?τ₂) |- _] => rewrite (Coll_right_inv τ₁ τ₂) in H; subst
    | [H: Coll₀ (`?τ₂) = `?τ₁ |- _] => symmetry in H
    | [H:ANID ▷ _ >=> _ ⊣ _ ; _ |- _ ] => inversion H; clear H
    | [H:ANEnv ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANMap _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANMapConcat _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANMapEnv _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANDefault _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANApp _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANAppEnv _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANEither _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANEitherConcat _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANProduct _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANSelect _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANUnop _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANBinop _ _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:ANConst _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H: (_,_) = (_,_) |- _ ] => inversion H; clear H
    | [H: map (fun x2 : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                 (fst x2, ` (snd x2))) ?x0 = [] |- _] => apply (map_rtype_nil x0) in H; simpl in H; subst
    | [H: (map
             (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                (fst x, proj1_sig (snd x))) _)
          =
          (map
             (fun x' : string * {τ₀' : rtype₀ | wf_rtype₀ τ₀' = true} =>
                (fst x', proj1_sig (snd x'))) _) |- _ ] =>
      apply map_rtype_fequal in H; trivial
    | [H:Rec _ _ _ = Rec _ _ _ |- _ ] => generalize (Rec_inv H); clear H; intro H; try subst
    | [H: context [(_::nil) = map
                                (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                                   (fst x, proj1_sig (snd x))) _] |- _] => symmetry in H
                                                                                         
    | [H: context [map
                     (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                        (fst x, proj1_sig (snd x))) _ = (_::nil) ] |- _] => apply map_eq_cons in H;
        destruct H as [? [? [? [??]]]]
    | [H: Coll₀ _ = Coll₀ _ |- _ ] => inversion H; clear H
    | [H: Rec₀ _ _ = Rec₀ _ _ |- _ ] => inversion H; clear H
    | [H: _ ▷ _ >=> snd ?x ⊣ _ ;_ |- _] => destruct x; simpl in *; subst
    | [H:unaryOp_type AColl _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type AFlatten _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type (ARec _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type (ADot _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type (ARecProject _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type (ARecRemove _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type ALeft _ _ |- _ ] => inversion H; clear H; subst
    | [H:unaryOp_type ARight _ _ |- _ ] => inversion H; clear H; subst
    | [H:binOp_type AConcat _ _ _ |- _ ] => inversion H; clear H
    | [H:binOp_type AAnd _ _ _ |- _ ] => inversion H; clear H
    | [H:binOp_type AMergeConcat _ _ _ |- _ ] => inversion H; clear H
  end; try rtype_equalizer; try assumption; try subst; simpl in *; try nraenv_core_inverter.

Ltac nraenv_core_inferer := try nraenv_core_inverter; subst; try eauto.


Ltac input_well_typed :=
  repeat progress
         match goal with
           | [HO:?op ▷ ?τin >=> ?τout ⊣ ?τc ; ?τenv,
              HI:?x ▹ ?τin,
              HC:bindings_type ?c ?τc,
              HE:?env ▹ ?τenv
              |- context [(nraenv_core_eval ?h ?c ?op ?env ?x)]] =>
             let xout := fresh "dout" in
             let xtype := fresh "τout" in
             let xeval := fresh "eout" in
             destruct (typed_nraenv_core_yields_typed_data c _ _ op HC HE HI HO)
               as [xout [xeval xtype]]; rewrite xeval in *; simpl
         end.