Module Qcert.TypeSystem.RTypeMeetJoin

Require Import String.
Require Import Bool.
Require Import List.
Require Import Permutation.
Require Import Morphisms.
Require Import RelationClasses.
Require Import EquivDec.
Require Import Utils.
Require Import ForeignType.
Require Import RType.
Require Import BrandRelation.

Section RTypeMeetJoin.

Definition record_kind_rtype_join {B} (k₁ k₂:record_kind) (l₁ l₂:list (string * B))
  := match k₁, k₂ with
       | Closed, Closed =>
         if (domain l₁) == (domain l₂) then Closed else Open
       | _, _ => Open
     end.

Lemma record_kind_rtype_join_open_l {B} k l₁ l₂:
  @record_kind_rtype_join B Open k l₁ l₂ = Open.

Lemma record_kind_rtype_join_open_r {B} k l₁ l₂:
  @record_kind_rtype_join B k Open l₁ l₂ = Open.

Lemma record_kind_rtype_join_closed_inv {B} k₁ k₂ l₁ l₂:
  @record_kind_rtype_join B k₁ k₂ l₁ l₂ = Closed ->
  k₁ = Closed /\ k₂ = Closed /\ domain l₁ = domain l₂.

Lemma record_kind_rtype_join_idempotent {B} k l :
  @record_kind_rtype_join B k k l l = k.

Lemma record_kind_rtype_join_comm_kind {B} k₁ k₂ l₁ l₂ :
  @record_kind_rtype_join B k₁ k₂ l₁ l₂ =
  record_kind_rtype_join k₂ k₁ l₁ l₂.

Lemma record_kind_rtype_join_comm_list {B} k₁ k₂ l₁ l₂ :
  @record_kind_rtype_join B k₁ k₂ l₁ l₂ =
  record_kind_rtype_join k₁ k₂ l₂ l₁.

Lemma record_kind_rtype_join_comm {B} k₁ k₂ l₁ l₂ :
  @record_kind_rtype_join B k₁ k₂ l₁ l₂ =
  record_kind_rtype_join k₂ k₁ l₂ l₁.


Definition rtype_meet_compatible_records {A B} (k₁ k₂:record_kind)
             (l₁:list (string*A)) (l₂:list (string * B)) : Prop
    := match k₁, k₂ with
       | Open, Open => True
       | Open, Closed => sublist (domain l₁) (domain l₂)
       | Closed, Open => sublist (domain l₂) (domain l₁)
       | Closed, Closed => (domain l₂) = (domain l₁)
     end.

Lemma rtype_meet_compatible_records_dec {A B} (k₁ k₂:record_kind)
        (l₁:list (string*A)) (l₂:list (string * B)) :
    {rtype_meet_compatible_records k₁ k₂ l₁ l₂} + {~ rtype_meet_compatible_records k₁ k₂ l₁ l₂}.
    
Definition record_kind_rtype_meet (k₁ k₂:record_kind)
  := match k₁, k₂ with
       | Open, Open => Open
       | _, _ => Closed
     end.

Lemma rtype_meet_compatible_records_idempotent {B} k₁ k₂ r :
  @rtype_meet_compatible_records B B k₁ k₂ r r.

Lemma record_kind_rtype_meet_idempotent k : record_kind_rtype_meet k k = k.

Lemma rtype_meet_compatible_records_commutative {A B} k₁ k₂ r₁ r₂:
  @rtype_meet_compatible_records A B k₁ k₂ r₁ r₂ ->
  @rtype_meet_compatible_records B A k₂ k₁ r₂ r₁.

Lemma record_kind_rtype_meet_commutative k₁ k₂ : record_kind_rtype_meet k₁ k₂ = record_kind_rtype_meet k₂ k₁.

Lemma rtype_meet_compatible_records_domain_eq_l {A B C}
      (k₁ k₂:record_kind) (l₁:list (string*A)) (l₁':list (string*B)) (l₂:list (string * C)) :
  domain l₁ = domain l₁' ->
  rtype_meet_compatible_records k₁ k₂ l₁ l₂
  = rtype_meet_compatible_records k₁ k₂ l₁' l₂.

Lemma rtype_meet_compatible_records_domain_eq_r {A B C}
      (k₁ k₂:record_kind) (l₁:list (string*A)) (l₂:list (string*B)) (l₂':list (string * C)) :
  domain l₂ = domain l₂' ->
  rtype_meet_compatible_records k₁ k₂ l₁ l₂
  = rtype_meet_compatible_records k₁ k₂ l₁ l₂'.


Lemma record_kind_rtype_meet_associative k k0 k1 :
  record_kind_rtype_meet (record_kind_rtype_meet k k0) k1
  = record_kind_rtype_meet k (record_kind_rtype_meet k0 k1).

Section mj.
  Context {ftype:foreign_type}.
  Context {br:brand_relation}.

  Fixpoint rtype_join₀ (τ₁ τ₂:rtype₀) : rtype₀
  := match τ₁, τ₂ with
       | ⊥₀, τ => τ
       | τ, ⊥₀ => τ
       | Unit₀, Unit₀ => Unit₀
       | Nat₀, Nat₀ => Nat₀
       | Float₀, Float₀ => Float₀
       | Bool₀, Bool₀ => Bool₀
       | String₀, String₀ => String₀
       | Coll₀ τ₁', Coll₀ τ₂' => Coll₀ (rtype_join₀ τ₁' τ₂')
       | Rec₀ k₁ srl, Rec₀ k₂ srl' => Rec₀ (record_kind_rtype_join k₁ k₂ srl srl')
                                ((fix map_rtype_join₀ l1 l2 :=
                                match l1 with
                                  | nil => nil
                                  | (s,r)::srs => match lookup string_dec l2 s with
                                                      | None => map_rtype_join₀ srs l2
                                                      | Some r' => (s,rtype_join₀ r r')::(map_rtype_join₀ srs l2)
                                                  end
                                end) srl srl')
       | Either₀ τl₁ τr₁, Either₀ τl₂ τr₂ => Either₀ (rtype_join₀ τl₁ τl₂) (rtype_join₀ τr₁ τr₂)
       | Arrow₀ τl₁ τr₁, Arrow₀ τl₂ τr₂ => Arrow₀ (rtype_meet₀ τl₁ τl₂) (rtype_join₀ τr₁ τr₂)
       | Brand₀ b₁, Brand₀ b₂ => Brand₀ (brand_join brand_relation_brands b₁ b₂)
       | Foreign₀ ft₁, Foreign₀ ft₂ => Foreign₀ (join ft₁ ft₂)
       | _, _ => ⊤₀
     end
  with rtype_meet₀ (τ₁ τ₂:rtype₀) : rtype₀
  := match τ₁, τ₂ with
       | ⊤₀, τ => τ
       | τ, ⊤₀ => τ
       | Unit₀, Unit₀ => Unit₀
       | Nat₀, Nat₀ => Nat₀
       | Float₀, Float₀ => Float₀
       | Bool₀, Bool₀ => Bool₀
       | String₀, String₀ => String₀
       | Coll₀ τ₁', Coll₀ τ₂' => Coll₀ (rtype_meet₀ τ₁' τ₂')
       | Rec₀ k₁ srl, Rec₀ k₂ srl' =>
         if rtype_meet_compatible_records_dec k₁ k₂ srl srl'
         then Rec₀ (record_kind_rtype_meet k₁ k₂)
                  (rec_concat_sort ((fix map_rtype_meet₀ l1 l2 :=
                     match l1 with
                       | nil => nil
                       | (s,r)::srs => match lookup string_dec l2 s with
                                         | None => (s,r)::map_rtype_meet₀ srs l2
                                         | Some r' => (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
                                       end
                     end) srl srl')
                                   (lookup_diff string_dec srl' srl))
         else ⊥₀
       | Either₀ τl₁ τr₁, Either₀ τl₂ τr₂ =>
         Either₀ (rtype_meet₀ τl₁ τl₂) (rtype_meet₀ τr₁ τr₂)
       | Arrow₀ τl₁ τr₁, Arrow₀ τl₂ τr₂ => Arrow₀ (rtype_join₀ τl₁ τl₂) (rtype_meet₀ τr₁ τr₂)
       | Brand₀ τ₁, Brand₀ τ₂ => Brand₀ (brand_meet brand_relation_brands τ₁ τ₂)
       | Foreign₀ ft₁, Foreign₀ ft₂ => Foreign₀ (meet ft₁ ft₂)
       | _, _ => ⊥₀
     end.

Lemma map_rtype_join₀_domain_subset r srl x:
  In x (domain (((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s0, r1) :: srs =>
               match lookup string_dec l2 s0 with
               | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) r srl))) -> In x (domain r) /\ In x (domain srl).

Lemma map_rtype_join₀_domain_subset_inv r srl x:
 In x (domain r) /\ In x (domain srl) ->
  In x (domain (((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s0, r1) :: srs =>
               match lookup string_dec l2 s0 with
               | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) r srl))).

Lemma map_rtype_join₀_rtype_joins {r₁ r₂ s τ₁ τ₂} :
  lookup string_dec r₁ s = Some τ₁ ->
    lookup string_dec r₂ s = Some τ₂ ->
    lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
                | None => map_rtype_join₀ srs l2
                end
            end) r₁ r₂)) s = Some (rtype_join₀ τ₁ τ₂).

Lemma NoDup_map_rtype_join₀ {r₁ r₂} :
      NoDup (domain r₁) -> NoDup (domain
      ((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
          list (string * rtype₀) :=
          match l1 with
          | nil => nil
          | (s0, r1) :: srs =>
              match lookup string_dec l2 s0 with
              | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
              | None => map_rtype_join₀ srs l2
              end
          end) r₁ r₂)).

Lemma map_rtype_meet₀_domain r srl:
  (domain (((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s,r)::srs => match lookup string_dec l2 s with
                             | None => (s,r)::map_rtype_meet₀ srs l2
                             | Some r' => (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
                           end
           end)
             r srl))) = domain r.

Lemma map_rtype_meet₀_rtype_meets {r₁ r₂ s τ₁ τ₂} :
  lookup string_dec r₁ s = Some τ₁ ->
    lookup string_dec r₂ s = Some τ₂ ->
    lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
                | None => (s, r)::map_rtype_meet₀ srs l2
                end
            end) r₁ r₂)) s = Some (rtype_meet₀ τ₁ τ₂).

Lemma map_rtype_meet₀_some_none {r₁ r₂ s τ₁} :
  lookup string_dec r₁ s = Some τ₁ ->
    lookup string_dec r₂ s = None ->
    lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
                | None => (s, r)::map_rtype_meet₀ srs l2
                end
            end) r₁ r₂)) s = Some τ₁.

Lemma map_rtype_meet₀_none {r₁ r₂ s} :
  lookup string_dec r₁ s = None ->
    lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
                | None => (s, r)::map_rtype_meet₀ srs l2
                end
            end) r₁ r₂)) s = None.
  
Ltac perm_tac :=
        try match goal with
          | [H1:In ?x ?l, H3:Permutation ?l2 ?l |- _ ] =>
            extend (Permutation_in _ (symmetry H3) H1)
          | [H1:In ?x ?l, H3:Permutation ?l ?l2 |- _ ] =>
            extend (Permutation_in _ H3 H1)
            end.

Lemma map_rtype_meet₀_disjoint r₁ r₂ :
  disjoint (domain ((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
          list (string * rtype₀) :=
          match l1 with
          | nil => nil
          | (s,r)::srs => match lookup string_dec l2 s with
                            | None => (s,r)::map_rtype_meet₀ srs l2
                            | Some r' => (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
                          end
          end) r₁ r₂)) (domain (lookup_diff string_dec r₂ r₁)).

Lemma NoDup_map_rtype_meet₀_lookup_diff {r₁ r₂} :
      NoDup (domain r₁) ->
      NoDup (domain r₂) ->
      NoDup (domain
               (((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
          list (string * rtype₀) :=
          match l1 with
          | nil => nil
          | (s,r)::srs => match lookup string_dec l2 s with
                             | None => (s,r)::map_rtype_meet₀ srs l2
                             | Some r' => (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
                           end
          end) r₁ r₂) ++ (lookup_diff string_dec r₂ r₁))).

Lemma map_rtype_meet₀_cons2_nin a b l1 l2 :
                  ~ In a (domain l1) ->
                  ((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
         list (string * rtype₀) :=
         match l1 with
         | nil => nil
         | (s, r2) :: srs =>
             match lookup string_dec l2 s with
             | Some r' => (s, rtype_meet₀ r2 r') :: map_rtype_meet₀ srs l2
             | None => (s, r2) :: map_rtype_meet₀ srs l2
             end
         end) l1 ((a,b) :: l2))
                     =
                  ((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
             list (string * rtype₀) :=
             match l1 with
             | nil => nil
             | (s, r) :: srs =>
                 match lookup string_dec l2 s with
                 | Some r' => (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
                 | None => (s, r) :: map_rtype_meet₀ srs l2
                 end
             end) l1 l2).

Lemma rtype_join₀_meet₀_wf {τ₁ τ₂} :
  wf_rtype₀ τ₁ = true ->
  wf_rtype₀ τ₂ = true ->
  wf_rtype₀ (rtype_join₀ τ₁ τ₂) = true
/\ wf_rtype₀ (rtype_meet₀ τ₁ τ₂) = true.

Corollary rtype_join₀_wf {τ₁ τ₂} :
  wf_rtype₀ τ₁ = true ->
  wf_rtype₀ τ₂ = true ->
  wf_rtype₀ (rtype_join₀ τ₁ τ₂) = true.

Corollary rtype_meet₀_wf {τ₁ τ₂} :
  wf_rtype₀ τ₁ = true ->
  wf_rtype₀ τ₂ = true ->
  wf_rtype₀ (rtype_meet₀ τ₁ τ₂) = true.

Program Definition rtype_join (τ₁ τ₂:rtype) : rtype
  := exist _ (rtype_join₀ τ₁ τ₂) (rtype_join₀_wf (proj2_sig τ₁) (proj2_sig τ₂)).

Program Definition rtype_meet (τ₁ τ₂:rtype) : rtype
  := exist _ (rtype_meet₀ τ₁ τ₂) (rtype_meet₀_wf (proj2_sig τ₁) (proj2_sig τ₂)).

Lemma map_rtype_join₀_lookup_none1 {l₁ l₂ s r} :
lookup string_dec l₂ s = None ->
(fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
          | None => map_rtype_join₀ srs l2
          end
      end) ((s, r)::l₁) l₂ =
(fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
          | None => map_rtype_join₀ srs l2
          end
      end) l₁ l₂.

Lemma map_rtype_join₀_lookup_none2 {l₁ l₂ s r} :
lookup string_dec l₁ s = None ->
(fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
          | None => map_rtype_join₀ srs l2
          end
      end) l₁ ((s, r) :: l₂) =
(fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
          | None => map_rtype_join₀ srs l2
          end
      end) l₁ l₂.

Lemma map_rtype_join₀_lookup_some2 {l₁ l₂ s τ₁ τ₂} :
  lookup string_dec l₁ s = Some τ₁ ->
  is_list_sorted ODT_lt_dec (domain l₁) = true ->
  is_list_sorted ODT_lt_dec (domain ((s,τ₂)::l₂)) = true ->
   (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
          | None => map_rtype_join₀ srs l2
          end
      end) l₁ ((s, τ₂) :: l₂) =
 (s, rtype_join₀ τ₁ τ₂)
   :: (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
         list (string * rtype₀) :=
         match l1 with
         | nil => nil
         | (s0, r1) :: srs =>
             match lookup string_dec l2 s0 with
             | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
             | None => map_rtype_join₀ srs l2
             end
         end) l₁ l₂.

Lemma map_rtype_join₀_idempotent' k {rl1} :
  forall (wf1 : wf_rtype₀ (Rec₀ k rl1) = true)
         (subH : Forall
                   (fun ab : string * rtype₀ =>
                      wf_rtype₀ (snd ab) = true ->
                      rtype_join₀ (snd ab) (snd ab) = (snd ab)) rl1),
       (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s, r) :: srs =>
               match lookup string_dec l2 s with
               | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) rl1 rl1
       = rl1.

Lemma rtype_join₀_meet₀_idempotent a :
  wf_rtype₀ a = true ->
  rtype_join₀ a a = a
  /\ rtype_meet₀ a a = a.

Corollary rtype_join₀_idempotent a:
  forall (awf:wf_rtype₀ a = true),
    rtype_join₀ a a = a.

Corollary rtype_meet₀_idempotent a:
  forall (awf:wf_rtype₀ a = true),
    rtype_meet₀ a a = a.

Theorem rtype_join_idempotent: forall a, rtype_join a a = a.

Theorem rtype_meet_idempotent a : rtype_meet a a = a.

Local Hint Resolve rtype_join₀_idempotent : qcert.
Local Hint Constructors Forallt : qcert.

  Lemma map_rtype_join₀_idempotent k {rl1} :
  forall (wf1 : wf_rtype₀ (Rec₀ k rl1) = true),
       (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s, r) :: srs =>
               match lookup string_dec l2 s with
               | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) rl1 rl1
       = rl1.
  
 Lemma map_rtype_join₀_commutative' k₁ k₂ {rl1 rl2} :
  forall (wf1 : wf_rtype₀ (Rec₀ k₁ rl1) = true)
           (wf2 : wf_rtype₀ (Rec₀ k₂ rl2) = true)
           (subH : Forall
                  (fun ab : string * rtype₀ =>
                     forall b : rtype₀,
                     wf_rtype₀ (snd ab) = true ->
                       wf_rtype₀ b = true -> rtype_join₀ (snd ab) b = rtype_join₀ b (snd ab)) rl1),
       (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s, r) :: srs =>
               match lookup string_dec l2 s with
               | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) rl1 rl2
       = (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s, r) :: srs =>
               match lookup string_dec l2 s with
               | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) rl2 rl1.

Lemma map_rtype_meet₀_lookup_none1 {l₁ l₂ s r} :
lookup string_dec l₂ s = None ->
(fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
          | None => map_rtype_meet₀ srs l2
          end
      end) ((s, r)::l₁) l₂ =
(fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
          | None => map_rtype_meet₀ srs l2
          end
      end) l₁ l₂.

Lemma map_rtype_meet₀_lookup_none2 {l₁ l₂ s r} :
lookup string_dec l₁ s = None ->
(fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
          | None => map_rtype_meet₀ srs l2
          end
      end) l₁ ((s, r) :: l₂) =
(fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
          | None => map_rtype_meet₀ srs l2
          end
      end) l₁ l₂.

Lemma map_rtype_meet₀_lookup_some2 {l₁ l₂ s τ₁ τ₂} :
  lookup string_dec l₁ s = Some τ₁ ->
  is_list_sorted ODT_lt_dec (domain l₁) = true ->
  is_list_sorted ODT_lt_dec (domain ((s,τ₂)::l₂)) = true ->
   (fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s0, r1) :: srs =>
          match lookup string_dec l2 s0 with
          | Some r' => (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
          | None => map_rtype_meet₀ srs l2
          end
      end) l₁ ((s, τ₂) :: l₂) =
 (s, rtype_meet₀ τ₁ τ₂)
   :: (fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
         list (string * rtype₀) :=
         match l1 with
         | nil => nil
         | (s0, r1) :: srs =>
             match lookup string_dec l2 s0 with
             | Some r' => (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
             | None => map_rtype_meet₀ srs l2
             end
         end) l₁ l₂.

Lemma rtype_join₀_meet₀_commutative a b:
  forall (awf : wf_rtype₀ a = true)
         (bwf : wf_rtype₀ b = true),
    rtype_join₀ a b = rtype_join₀ b a
    /\ rtype_meet₀ a b = rtype_meet₀ b a.

Corollary rtype_join₀_commutative a b:
  forall (awf : wf_rtype₀ a = true)
         (bwf : wf_rtype₀ b = true),
         rtype_join₀ a b = rtype_join₀ b a.

Corollary rtype_meet₀_commutative a b:
  forall (awf : wf_rtype₀ a = true)
         (bwf : wf_rtype₀ b = true),
         rtype_meet₀ a b = rtype_meet₀ b a.

Theorem rtype_join_commutative: forall a b, rtype_join a b = rtype_join b a.

Theorem rtype_meet_commutative: forall a b, rtype_meet a b = rtype_meet b a.

 Lemma map_rtype_join₀_commutative k₁ k₂ {rl1 rl2} :
  forall (wf1 : wf_rtype₀ (Rec₀ k₁ rl1) = true)
           (wf2 : wf_rtype₀ (Rec₀ k₂ rl2) = true),
       (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s, r) :: srs =>
               match lookup string_dec l2 s with
               | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) rl1 rl2
       = (fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s, r) :: srs =>
               match lookup string_dec l2 s with
               | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) rl2 rl1.


Lemma map_rtype_join₀_lookup_rtype_join {l₁ l₂ s τ₁ τ₂} :
   lookup string_dec l₁ s = Some τ₁ ->
   lookup string_dec l₂ s = Some τ₂ ->
   lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s0, r1) :: srs =>
               match lookup string_dec l2 s0 with
               | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) l₁ l₂)) s = Some (rtype_join₀ τ₁ τ₂).

Lemma map_rtype_join₀_lookup_none1_rtype_join {l₁ l₂ s} :
   lookup string_dec l₁ s = None ->
   lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s0, r1) :: srs =>
               match lookup string_dec l2 s0 with
               | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) l₁ l₂)) s = None.

Lemma map_rtype_join₀_lookup_none2_rtype_join {l₁ l₂ s} :
   lookup string_dec l₂ s = None ->
   lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
           list (string * rtype₀) :=
           match l1 with
           | nil => nil
           | (s0, r1) :: srs =>
               match lookup string_dec l2 s0 with
               | Some r' => (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
               | None => map_rtype_join₀ srs l2
               end
           end) l₁ l₂)) s = None.

Lemma map_rtype_join₀_domain_sublist a b :
  sublist (domain ((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} : list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
                | None => map_rtype_join₀ srs l2
                end
            end) a b)) (domain a).

Lemma map_rtype_join₀_domain_is_list_sorted {a b} :
  is_list_sorted ODT_lt_dec (domain a) = true ->
  is_list_sorted ODT_lt_dec (domain ((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
                | None => map_rtype_join₀ srs l2
                end
            end) a b)) = true.

Lemma map_rtype_join₀_domain {a b}:
  is_list_sorted ODT_lt_dec (domain a) = true ->
  is_list_sorted ODT_lt_dec (domain b) = true ->
  domain a = domain b ->
  domain ((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
                | None => map_rtype_join₀ srs l2
                end
            end) a b) = domain a.

Lemma record_kind_rtype_join_associative {k k0 k1 a b c}:
    wf_rtype₀ (Rec₀ k a) = true ->
   wf_rtype₀ (Rec₀ k0 b) = true ->
   wf_rtype₀ (Rec₀ k1 c) = true ->
   (record_kind_rtype_join (record_kind_rtype_join k k0 a b) k1
        ((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
                | None => map_rtype_join₀ srs l2
                end
            end) a b) c) =
 (record_kind_rtype_join k (record_kind_rtype_join k0 k1 b c) a
        ((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s, r) :: srs =>
                match lookup string_dec l2 s with
                | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
                | None => map_rtype_join₀ srs l2
                end
            end) b c)).


Lemma domain_map_rtype_meet₀_diff r srl :
      domain (rec_concat_sort
            ((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
                list (string * rtype₀) :=
                match l1 with
                | nil => nil
                | (s, r) :: srs =>
                    match lookup string_dec l2 s with
                    | Some r' => (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
                    | None => (s, r) :: map_rtype_meet₀ srs l2
                    end
                end) r srl) (lookup_diff string_dec srl r)) =
      domain (rec_concat_sort r srl).


Lemma NoDup_domain_lookups_Permutation {A B : Type} dec (l l' : list (A*B)) :
       NoDup (domain l) ->
       NoDup (domain l') ->
       (forall x : A, lookup dec l x = lookup dec l' x) ->
       Permutation l l'.

Lemma lookup_nodup_perm {A B : Type}
      (dec : forall a a' : A, {a = a'} + {a <> a'})
         (l l' : list (A * B)) (a : A) :
       NoDup (domain l) ->
       Permutation l l' ->
       lookup dec l a = lookup dec l' a.

Lemma map_rtype_meet₀_domain_rec_concat_sort r srl s :
              NoDup (domain r) ->
              NoDup (domain srl) ->
        lookup string_dec (rec_concat_sort ((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s0, r0) :: srs =>
                match lookup string_dec l2 s0 with
                | Some r' => (s0, rtype_meet₀ r0 r') :: map_rtype_meet₀ srs l2
                | None => (s0, r0) :: map_rtype_meet₀ srs l2
                end
            end) r srl) (lookup_diff string_dec srl r)) s
              = lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
            list (string * rtype₀) :=
            match l1 with
            | nil => nil
            | (s0, r0) :: srs =>
                match lookup string_dec l2 s0 with
                | Some r' => (s0, rtype_meet₀ r0 r') :: map_rtype_meet₀ srs l2
                | None => (s0, r0) :: map_rtype_meet₀ srs l2
                end
            end) r srl) ++ (lookup_diff string_dec srl r)) s.

Lemma map_rtype_join₀_associative' {k k0 k1 a b c}:
     Forall
     (fun ab : string * rtype₀ =>
      forall b c : rtype₀,
      wf_rtype₀ (snd ab) = true ->
      wf_rtype₀ b = true ->
      wf_rtype₀ c = true ->
      rtype_join₀ (rtype_join₀ (snd ab) b) c = rtype_join₀ (snd ab) (rtype_join₀ b c)) a ->
    wf_rtype₀ (Rec₀ k a) = true ->
   wf_rtype₀ (Rec₀ k0 b) = true ->
   wf_rtype₀ (Rec₀ k1 c) = true ->
     rtype_join₀ (rtype_join₀ (Rec₀ k a) (Rec₀ k0 b)) (Rec₀ k1 c) =
     rtype_join₀ (Rec₀ k a) (rtype_join₀ (Rec₀ k0 b) (Rec₀ k1 c)).

Lemma rtype_join₀_meet₀_associative {a b c : rtype₀} :
   wf_rtype₀ a = true ->
   wf_rtype₀ b = true ->
   wf_rtype₀ c = true ->
   rtype_join₀ (rtype_join₀ a b) c = rtype_join₀ a (rtype_join₀ b c)
   /\ rtype_meet₀ (rtype_meet₀ a b) c = rtype_meet₀ a (rtype_meet₀ b c).

Corollary rtype_join₀_associative {a b c : rtype₀} :
   wf_rtype₀ a = true ->
   wf_rtype₀ b = true ->
   wf_rtype₀ c = true ->
   rtype_join₀ (rtype_join₀ a b) c = rtype_join₀ a (rtype_join₀ b c).

Corollary rtype_meet₀_associative {a b c : rtype₀} :
   wf_rtype₀ a = true ->
   wf_rtype₀ b = true ->
   wf_rtype₀ c = true ->
   rtype_meet₀ (rtype_meet₀ a b) c = rtype_meet₀ a (rtype_meet₀ b c).

Theorem rtype_join_associative : forall a b c,
    rtype_join (rtype_join a b) c = rtype_join a (rtype_join b c).

Theorem rtype_meet_associative : forall a b c,
    rtype_meet (rtype_meet a b) c = rtype_meet a (rtype_meet b c).

Lemma map_rtype_join₀_nil_r l₁ :
      ((fix map_rtype_join₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
         list (string * rtype₀) :=
         match l1 with
         | nil => nil
         | (s, r) :: srs =>
             match lookup string_dec l2 s with
             | Some r' => (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
             | None => map_rtype_join₀ srs l2
             end
         end) l₁ nil) = nil.

End mj.
End RTypeMeetJoin.

Section rtype_join_re.


Lemma rtype_nequal {ftype:foreign_type} {br:brand_relation} {τ₁ τ₂:rtype} : τ₁ <> τ₂ -> proj1_sig τ₁ <> proj1_sig τ₂.

Ltac prover_simpler
  := repeat
       match goal with
         | [H: not (@eq rtype ?A ?B) |- _ ] => apply rtype_nequal in H; simpl in H
         | [H: (@eq rtype ?A ?B) -> False |- _ ] => apply rtype_nequal in H; simpl in H
         | [H: not (eq ?x ?x) |- _ ] => elim H; trivial
         | [H: (eq ?x ?x) -> False |- _ ] => elim H; trivial
       end.

Ltac prover0 := apply rtype_fequal; unfold rtype_join; simpl; trivial.
Ltac prover1 τ := intros; apply rtype_fequal; unfold rtype_join; simpl;
                  let tt := fresh "τ'" in
                  let tpf := fresh "pf'" in
                  destruct τ as [tt tpf]; destruct tt; simpl;
                  prover_simpler; trivial.

Context {ftype:foreign_type}.
Context {m:brand_relation}.
Lemma rtype_join_Top_l τ :
  rtype_join ⊤ τ = ⊤.

Lemma rtype_join_Top_r τ : rtype_join τ ⊤ = ⊤.

Lemma rtype_join_Bottom_r τ : rtype_join τ ⊥ = τ.

Lemma rtype_join_Bottom_l τ : rtype_join ⊥ τ = τ.

Lemma rtype_join_Unit_eq : rtype_join Unit Unit = Unit.

Lemma rtype_join_Unit_neq_l τ: τ <> ⊥ -> τ <> Unit -> rtype_join Unit τ = ⊤.

Lemma rtype_join_Unit_neq_r τ: τ <> ⊥ -> τ <> Unit -> rtype_join τ Unit = ⊤.

Lemma rtype_join_Nat_eq : rtype_join Nat Nat = Nat.

Lemma rtype_join_Nat_neq_l τ: τ <> ⊥ -> τ <> Nat -> rtype_join Nat τ = ⊤.

Lemma rtype_join_Nat_neq_r τ: τ <> ⊥ -> τ <> Nat -> rtype_join τ Nat = ⊤.

Lemma rtype_join_Float_eq : rtype_join Float Float = Float.

Lemma rtype_join_Float_neq_l τ: τ <> ⊥ -> τ <> Float -> rtype_join Float τ = ⊤.

Lemma rtype_join_Float_neq_r τ: τ <> ⊥ -> τ <> Float -> rtype_join τ Float = ⊤.

Lemma rtype_join_Bool_eq : rtype_join Bool Bool = Bool.

Lemma rtype_join_Bool_neq_l τ: τ <> ⊥ -> τ <> Bool -> rtype_join Bool τ = ⊤.

Lemma rtype_join_Bool_neq_r τ: τ <> ⊥ -> τ <> Bool -> rtype_join τ Bool = ⊤.

Lemma rtype_join_String_eq : rtype_join String String = String.

Lemma rtype_join_String_neq_l τ: τ <> ⊥ -> τ <> String -> rtype_join String τ = ⊤.

Lemma rtype_join_String_neq_r τ: τ <> ⊥ -> τ <> String -> rtype_join τ String = ⊤.

Lemma rtype_join_Coll_eq τ₁ τ₂ : rtype_join (Coll τ₁) (Coll τ₂) = Coll (rtype_join τ₁ τ₂).

Lemma rtype_join_Coll_neq_l τ τ₃: τ <> ⊥ -> (forall τ₂, τ <> Coll τ₂) -> rtype_join (Coll τ₃) τ = ⊤.

Lemma rtype_join_Coll_neq_r τ τ₃: τ <> ⊥ -> (forall τ₂, τ <> Coll τ₂) -> rtype_join τ (Coll τ₃) = ⊤.

Fixpoint map_rtype_join l1 l2 :=
  match l1 with
    | nil => nil
    | (s,r)::srs => match lookup string_dec l2 s with
                      | None => map_rtype_join srs l2
                      | Some r' => (s,rtype_join r r')::(map_rtype_join srs l2)
                    end
  end.


Lemma map_rtype_join_sublist_l l₁ l₂ : sublist (domain (map_rtype_join l₁ l₂)) (domain l₁).

Lemma map_rtype_join_is_sorted l₁ l₂ :
  is_list_sorted ODT_lt_dec (domain l₁) = true
  -> is_list_sorted ODT_lt_dec (domain (map_rtype_join l₁ l₂)) = true.
                              
Lemma rtype_join_Rec_eq k₁ rl₁ pf₁ k₂ rl₂ pf₂ :
  rtype_join (Rec k₁ rl₁ pf₁) (Rec k₂ rl₂ pf₂) =
  Rec (record_kind_rtype_join k₁ k₂ rl₁ rl₂)
        (map_rtype_join rl₁ rl₂) (map_rtype_join_is_sorted rl₁ rl₂ pf₁).

Lemma rtype_join_Rec_neq_l τ k rl pf :
  τ <> ⊥ -> (forall k₂ rl₂ pf₂, τ <> Rec k₂ rl₂ pf₂) -> rtype_join (Rec k rl pf) τ = ⊤.

Lemma rtype_join_Rec_neq_r τ k rl pf :
  τ <> ⊥ -> (forall k₂ rl₂ pf₂, τ <> Rec k₂ rl₂ pf₂) -> rtype_join τ (Rec k rl pf) = ⊤.

Lemma rtype_join_Either_eq τl₁ τr₁ τl₂ τr₂ : rtype_join (Either τl₁ τr₁) (Either τl₂ τr₂) = Either (rtype_join τl₁ τl₂) (rtype_join τr₁ τr₂).

Lemma rtype_join_Either_neq_l τ τl τr: τ <> ⊥ -> (forall τl₂ τr₂, τ <> Either τl₂ τr₂) -> rtype_join (Either τl τr) τ = ⊤.

Lemma rtype_join_Either_neq_r τ τl τr: τ <> ⊥ -> (forall τl₂ τr₂, τ <> Either τl₂ τr₂) -> rtype_join τ (Either τl τr) = ⊤.

Lemma rtype_join_Brand_eq x y : rtype_join (Brand x) (Brand y) = Brand (brand_join brand_relation_brands x y).

Lemma rtype_join_Brand_neq_l τ y: τ <> ⊥ -> (forall x, τ <> Brand x) -> rtype_join (Brand y) τ = ⊤.

Lemma rtype_join_Brand_neq_r τ y: τ <> ⊥ -> (forall x, τ <> Brand x) -> rtype_join τ (Brand y) = ⊤.

 Lemma rtype_join_Foreign_eq x y : rtype_join (Foreign x) (Foreign y) = Foreign (join x y).

Lemma rtype_join_Foreign_neq_l τ y: τ <> ⊥ -> (forall x, τ <> Foreign x) -> rtype_join (Foreign y) τ = ⊤.

Lemma rtype_join_Foreign_neq_r τ y: τ <> ⊥ -> (forall x, τ <> Foreign x) -> rtype_join τ (Foreign y) = ⊤.
End rtype_join_re.

Section rtype_meet_re.


Ltac prover_simpler
  := repeat
       match goal with
         | [H: not (@eq rtype ?A ?B) |- _ ] => apply rtype_nequal in H; simpl in H
         | [H: (@eq rtype ?A ?B) -> False |- _ ] => apply rtype_nequal in H; simpl in H
         | [H: not (eq ?x ?x) |- _ ] => elim H; trivial
         | [H: (eq ?x ?x) -> False |- _ ] => elim H; trivial
       end.

Ltac prover0 := apply rtype_fequal; unfold rtype_meet; simpl; trivial.
Ltac prover1 τ := intros; apply rtype_fequal; unfold rtype_meet; simpl;
                  let tt := fresh "τ'" in
                  let tpf := fresh "pf'" in
                  destruct τ as [tt tpf]; destruct tt; simpl;
                  prover_simpler; trivial.

Context {ftype:foreign_type}.
Context {m:brand_relation}.

Lemma rtype_meet_Top_l τ :
  rtype_meet ⊤ τ = τ.

Lemma rtype_meet_Top_r τ : rtype_meet τ ⊤ = τ.

Lemma rtype_meet_Bottom_r τ : rtype_meet τ ⊥ = ⊥.

Lemma rtype_meet_Bottom_l τ : rtype_meet ⊥ τ = ⊥.

Lemma rtype_meet_Unit_eq : rtype_meet Unit Unit = Unit.

Lemma rtype_meet_Unit_neq_l τ: τ <> ⊤ -> τ <> Unit -> rtype_meet Unit τ = ⊥.

Lemma rtype_meet_Unit_neq_r τ: τ <> ⊤ -> τ <> Unit -> rtype_meet τ Unit = ⊥.

Lemma rtype_meet_Nat_eq : rtype_meet Nat Nat = Nat.

Lemma rtype_meet_Nat_neq_l τ: τ <> ⊤ -> τ <> Nat -> rtype_meet Nat τ = ⊥.

Lemma rtype_meet_Nat_neq_r τ: τ <> ⊤ -> τ <> Nat -> rtype_meet τ Nat = ⊥.

Lemma rtype_meet_Float_eq : rtype_meet Float Float = Float.

Lemma rtype_meet_Float_neq_l τ: τ <> ⊤ -> τ <> Float -> rtype_meet Float τ = ⊥.

Lemma rtype_meet_Float_neq_r τ: τ <> ⊤ -> τ <> Float -> rtype_meet τ Float = ⊥.

Lemma rtype_meet_Bool_eq : rtype_meet Bool Bool = Bool.

Lemma rtype_meet_Bool_neq_l τ: τ <> ⊤ -> τ <> Bool -> rtype_meet Bool τ = ⊥.

Lemma rtype_meet_Bool_neq_r τ: τ <> ⊤ -> τ <> Bool -> rtype_meet τ Bool = ⊥.

Lemma rtype_meet_String_eq : rtype_meet String String = String.

Lemma rtype_meet_String_neq_l τ: τ <> ⊤ -> τ <> String -> rtype_meet String τ = ⊥.

Lemma rtype_meet_String_neq_r τ: τ <> ⊤ -> τ <> String -> rtype_meet τ String = ⊥.

Lemma rtype_meet_Coll_eq τ₁ τ₂ : rtype_meet (Coll τ₁) (Coll τ₂) = Coll (rtype_meet τ₁ τ₂).

Lemma rtype_meet_Coll_neq_l τ τ₃: τ <> ⊤ -> (forall τ₂, τ <> Coll τ₂) -> rtype_meet (Coll τ₃) τ = ⊥.

Lemma rtype_meet_Coll_neq_r τ τ₃: τ <> ⊤ -> (forall τ₂, τ <> Coll τ₂) -> rtype_meet τ (Coll τ₃) = ⊥.

Fixpoint map_rtype_meet l1 l2 :=
  match l1 with
    | nil => nil
    | (s,r)::srs => match lookup string_dec l2 s with
                      | None => (s,r)::map_rtype_meet srs l2
                      | Some r' => (s,rtype_meet r r')::(map_rtype_meet srs l2)
                    end
  end.

Lemma map_rtype_meet_domain r srl:
  domain (map_rtype_meet r srl) = domain r.

  Lemma NoDup_map_rtype_meet_lookup_diff {r₁ r₂} :
      NoDup (domain r₁) ->
      NoDup (domain r₂) ->
      NoDup (domain
               ((map_rtype_meet r₁ r₂) ++ (lookup_diff string_dec r₂ r₁))).

  Lemma map_rtype_meet_sublist_l l₁ l₂ : sublist (domain (map_rtype_meet l₁ l₂)) (domain l₁).

Lemma map_rtype_meet_eq
      (rl₁ rl₂ : list (string * rtype)) :
   (fix map_rtype_meet₀ (l1 l2 : list (string * rtype₀)) {struct l1} :
      list (string * rtype₀) :=
      match l1 with
      | nil => nil
      | (s, r) :: srs =>
          match lookup string_dec l2 s with
          | Some r' => (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
          | None => (s, r) :: map_rtype_meet₀ srs l2
          end
      end)
     (map
        (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
         (fst x, proj1_sig (snd x))) rl₁)
     (map
        (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
         (fst x, proj1_sig (snd x))) rl₂) =
   map
     (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
        (fst x, proj1_sig (snd x))) (map_rtype_meet rl₁ rl₂).

  
Lemma rtype_meet_Rec_eq k₁ rl₁ pf₁ k₂ rl₂ pf₂ :
  rtype_meet (Rec k₁ rl₁ pf₁) (Rec k₂ rl₂ pf₂) =
  if rtype_meet_compatible_records_dec k₁ k₂ rl₁ rl₂
    then
      Rec (record_kind_rtype_meet k₁ k₂)
          (rec_concat_sort (map_rtype_meet rl₁ rl₂) (lookup_diff string_dec rl₂ rl₁)) (drec_concat_sort_sorted _ _)
   else ⊥.

Lemma rtype_meet_Rec_neq_l τ k rl pf :
  τ <> ⊤ -> (forall k₂ rl₂ pf₂, τ <> Rec k₂ rl₂ pf₂) -> rtype_meet (Rec k rl pf) τ = ⊥.

Lemma rtype_meet_Rec_neq_r τ k rl pf :
  τ <> ⊤ -> (forall k₂ rl₂ pf₂, τ <> Rec k₂ rl₂ pf₂) -> rtype_meet τ (Rec k rl pf) = ⊥.

Lemma rtype_meet_Either_eq τl₁ τr₁ τl₂ τr₂ : rtype_meet (Either τl₁ τr₁) (Either τl₂ τr₂) = Either (rtype_meet τl₁ τl₂) (rtype_meet τr₁ τr₂).

Lemma rtype_meet_Either_neq_l τ τl τr: τ <> ⊤ -> (forall τl₂ τr₂, τ <> Either τl₂ τr₂) -> rtype_meet (Either τl τr) τ = ⊥.

Lemma rtype_meet_Either_neq_r τ τl τr: τ <> ⊤ -> (forall τl₂ τr₂, τ <> Either τl₂ τr₂) -> rtype_meet τ (Either τl τr) = ⊥.

Lemma rtype_meet_Brand_eq x y : rtype_meet (Brand x) (Brand y) = Brand (brand_meet brand_relation_brands x y).

Lemma rtype_meet_Brand_neq_l τ y: τ <> ⊤ -> (forall x, τ <> Brand x) -> rtype_meet (Brand y) τ = ⊥.

Lemma rtype_meet_Brand_neq_r τ y: τ <> ⊤ -> (forall x, τ <> Brand x) -> rtype_meet τ (Brand y) = ⊥.

 Lemma rtype_meet_Foreign_eq x y : rtype_meet (Foreign x) (Foreign y) = Foreign (meet x y).

Lemma rtype_meet_Foreign_neq_l τ y: τ <> ⊤ -> (forall x, τ <> Foreign x) -> rtype_meet (Foreign y) τ = ⊥.

Lemma rtype_meet_Foreign_neq_r τ y: τ <> ⊤ -> (forall x, τ <> Foreign x) -> rtype_meet τ (Foreign y) = ⊥.

End rtype_meet_re.

Global Hint Rewrite @rtype_join_Top_l @rtype_join_Top_r: rtype_join.
Global Hint Rewrite @rtype_join_Bottom_l @rtype_join_Bottom_r: rtype_join.
Global Hint Rewrite @rtype_join_Unit_eq : rtype_join.
Global Hint Rewrite @rtype_join_Unit_neq_l @rtype_join_Unit_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Nat_eq : rtype_join.
Global Hint Rewrite @rtype_join_Nat_neq_l @rtype_join_Nat_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Float_eq : rtype_join.
Global Hint Rewrite @rtype_join_Float_neq_l @rtype_join_Float_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Bool_eq : rtype_join.
Global Hint Rewrite @rtype_join_Bool_neq_l @rtype_join_Bool_neq_r using discriminate: rattype_join.
Global Hint Rewrite @rtype_join_String_eq : rtype_join.
Global Hint Rewrite @rtype_join_String_neq_l @rtype_join_String_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Coll_eq : rtype_join.
Global Hint Rewrite @rtype_join_Coll_neq_l @rtype_join_Coll_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Rec_eq : rtype_join.
Global Hint Rewrite @rtype_join_Rec_neq_l @rtype_join_Rec_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Either_eq : rtype_join.
Global Hint Rewrite @rtype_join_Either_neq_l @rtype_join_Either_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Brand_eq : rtype_join.
Global Hint Rewrite @rtype_join_Brand_neq_l @rtype_join_Brand_neq_r using discriminate: rtype_join.
Global Hint Rewrite @rtype_join_Foreign_eq : rtype_join.
Global Hint Rewrite @rtype_join_Foreign_neq_l @rtype_join_Foreign_neq_r using discriminate: rtype_join.


Global Hint Rewrite @rtype_meet_Top_l @rtype_meet_Top_r: rtype_meet.
Global Hint Rewrite @rtype_meet_Bottom_l @rtype_meet_Bottom_r: rtype_meet.
Global Hint Rewrite @rtype_meet_Unit_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Unit_neq_l @rtype_meet_Unit_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Nat_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Nat_neq_l @rtype_meet_Nat_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Float_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Float_neq_l @rtype_meet_Float_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Bool_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Bool_neq_l @rtype_meet_Bool_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_String_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_String_neq_l @rtype_meet_String_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Coll_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Coll_neq_l @rtype_meet_Coll_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Rec_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Rec_neq_l @rtype_meet_Rec_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Either_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Either_neq_l @rtype_meet_Either_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Brand_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Brand_neq_l @rtype_meet_Brand_neq_r using discriminate: rtype_meet.
Global Hint Rewrite @rtype_meet_Foreign_eq : rtype_meet.
Global Hint Rewrite @rtype_meet_Foreign_neq_l @rtype_meet_Foreign_neq_r using discriminate: rtype_meet.