Module Qcert.TypeSystem.RSubtypeProp


Require Import String.
Require Import List.
Require Import RelationClasses.
Require Import Utils.
Require Import ForeignType.
Require Import RType.
Require Import BrandRelation.
Require Export RSubtype.

Section RSubtypeProp.

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

  Lemma top_subtype z : ⊤ <: z -> z = ⊤.
Proof.
    inversion 1; subst; eauto.
  Qed.

  Lemma subtype_bottom z : z <: ⊥ -> z = ⊥.
Proof.
    inversion 1; subst; eauto.
  Qed.

  Ltac simpl_type :=
    repeat match goal with
           | [H: ?z <: ⊥ |- _] => apply subtype_bottom in H; subst
           | [H: ⊤ <: ?z |- _] => apply top_subtype in H; subst
           end.

  Local Hint Constructors subtype : qcert.
  Instance subtype_trans : Transitive subtype.
Proof.
    red.
    intros x y.
    revert x.
    induction y using rtype_rect; intros x z sub1 sub2; inversion sub1; subst; simpl_type; eauto with qcert.
    - inversion sub2; subst; eauto with qcert.
      rtype_equalizer. subst; eauto with qcert.
    - inversion sub2; subst; qeauto.
      rtype_equalizer. subst.
      constructor.
      + intros s' r' lsr'.
        destruct (H5 _ _ lsr') as [?[look3 sub3]].
        destruct (H3 _ _ look3) as [?[??]].
        exists x0; intuition.
        generalize (Forallt_In H (s',x)).
        simpl; intros P; eapply P; eauto.
        apply (lookup_in string_dec); trivial.
      + intuition.
    - inversion sub2; subst; qeauto.
      rtype_equalizer. subst. qeauto.
    - rtype_equalizer. subst.
      inversion sub2; subst; trivial with qcert.
      rtype_equalizer. subst.
      econstructor; qeauto.
    - inversion sub2; subst; trivial with qcert.
      apply canon_equiv in H; apply canon_equiv in H0.
      rewrite H in H1.
      rewrite H0 in H2.
      constructor; etransitivity; eassumption.
    - invcs sub2; qtrivial.
      econstructor.
      transitivity ft; trivial.
  Qed.

  Global Instance subtype_pre : PreOrder subtype.
Proof.
    constructor; qeauto.
    apply subtype_trans.
  Qed.

  Lemma Rec_subtype_cons_weaken k s r lpf pf2:
    Rec k ((s, r) :: l₁) pf <: Rec Open lpf2.
Proof.
    apply SRec_open; intros.
    simpl.
    case_eq (string_dec s0 s); [intros ? ?; subst | qeauto].
    assert False; [|intuition].
    rewrite domain_cons in pf.
    apply is_list_sorted_NoDup in pf; [|apply StringOrder.lt_strorder].
    inversion pf; subst. elim H3.
    eapply in_dom; eapply lookup_in; eauto.
  Qed.

  Lemma Rec_subtype_cons_inv2 {k1 k2 s r llpf pf2}:
    Rec k1 lpf <: Rec k2 ((s, r) :: l₂) pf2 ->
                    exists pf',
                      Rec k1 lpf <: Rec Open lpf'.
Proof.
    intros sub.
    generalize pf2.
    rewrite domain_cons, is_list_sorted_cons.
    intros [pf' _].
    rewrite (Rec_subtype_cons_weaken k2 s r lpf2 pf') in sub.
    eauto.
  Qed.

  Lemma Rec_subtype_cons_inv1_open {k1 k2 s r llpf pf2}:
    Rec k1 ((s, r) :: l₁) pf <: Rec k2 lpf2 ->
                                lookup string_dec ls = None ->
                                k2 = Open.
Proof.
    intro rt.
    destruct k2; trivial.
    intros lo.
    apply lookup_none_nin in lo.
    elim lo.
    generalize (SRec_closed_equiv_domain rt); intros inns.
    simpl in inns.
    destruct (inns s).
    apply H; intuition.
  Qed.

  Lemma Rec_subtype_cons_inv1 {k1 k2 s r llpf pf2}:
    Rec k1 ((s, r) :: l₁) pf <: Rec k2 lpf2 ->
                                lookup string_dec ls = None ->
                                exists pf',
                                  Rec k1 lpf' <: Rec Open lpf2.
Proof.
    intros rt lo.
    generalize (Rec_subtype_cons_inv1_open rt lo); intros; subst.
    inversion rt; subst; rtype_equalizer.
    - destruct l₂; simpl in H2; try discriminate.
      inversion H2; subst. rtype_equalizer.
      subst. destruct p; simpl in *.
      destruct (string_dec s s); intuition congruence.
    - subst. destruct rl1; simpl in H0; try discriminate.
      inversion H0; rtype_equalizer. subst.
      destruct p; simpl in lo |- *.
      generalize pf.
      rewrite domain_cons, is_list_sorted_cons; simpl.
      intros [pf' _].
      exists pf'.
      apply SRec_open; intros s0 r0 ls0.
      specialize (H2 _ _ ls0); simpl in H2.
      destruct (string_dec s0 s); eauto.
      destruct H2 as [? [inv _]].
      inversion inv; subst. congruence.
  Qed.

Note that unlike the biased inverses, since we are removing an element from both sides, it is possible for k2 to be Closed
  Lemma Rec_subtype_cons_inv {k1 k2 s r1 r2 llpf pf2}:
    Rec k1 ((s, r1) :: l₁) pf <: Rec k2 ((s, r2) :: l₂) pf2 ->
                                 exists pf' pf2',
                                   Rec k1 lpf' <: Rec k2 lpf2'.
Proof.
    intros rt.
    inversion rt; subst; rtype_equalizer; subst.
    - repeat (exists (is_list_sorted_cons_inv _ pf)). reflexivity.
    - destruct rl1; simpl in H0; try discriminate.
      destruct rl2; simpl in H3; try discriminate.
      inversion H0; inversion H3; clear H0; clear H3.
      rtype_equalizer. subst.
      exists (is_list_sorted_cons_inv _ pf).
      exists (is_list_sorted_cons_inv _ pf2).
      generalize (is_list_sorted_NoDup ODT_lt_dec _ pf).
      generalize (is_list_sorted_NoDup ODT_lt_dec _ pf2).
      intros.
      constructor.
      + intros.
        specialize (H2 s r').
        simpl in H2.
        destruct p; destruct p0; simpl in *; subst.
        destruct (string_dec s s0).
        * inversion H; subst.
          apply lookup_in in H1.
          apply in_dom in H1.
          intuition.
        * auto.
      + intuition; subst.
        destruct p; destruct p0; simpl in *; subst.
        specialize (H5 s). intuition.
        inversion H0; subst.
        intuition.
  Qed.

  Global Instance subtype_part : PartialOrder eq subtype.
Proof.
    unfold PartialOrder, relation_equivalence, predicate_equivalence,
    relation_conjunction, predicate_intersection, Basics.flip; simpl.
    split; intros; subst; intuition.
    revert x0 H0 H1.
    induction x using rtype_rect; intros y sub1 sub2;
      simpl_type; trivial;
        inversion sub1; subst; simpl_type; trivial.
    - f_equal. inversion sub2; subst;
                 rtype_equalizer.
      + subst; eauto.
      + subst; eauto.
    - rtype_equalizer; subst.
      intros.
      apply rtype_fequal; simpl.
      inversion sub2; rtype_equalizer; subst; try apply Rec_pr_irrel; auto 1.
      f_equal; [ destruct k; destruct k2; intuition | ].
      f_equal.
      apply Forall2_eq.
      assert (deq:domain srl = domain rl2) by
          (eapply (@Sorted_incl_both_eq _ StringOrder.lt);
           [ apply string_eqdec
           | apply StringOrder.lt_strorder
           | eapply is_list_sorted_Sorted_iff; eauto
           | eapply is_list_sorted_Sorted_iff; eauto
           | apply (SRec_closed_in_domain sub2)
           | apply (SRec_closed_in_domain sub1)]).
      revert k k2 rl2 pf2 H sub1 sub2 H2 H4 H5 H7 deq.
      induction srl; destruct rl2; trivial; intros.
      + destruct p.
        generalize (H2 s r); simpl.
        destruct (string_dec s s); intuition.
        destruct H1; intuition; discriminate.
      + destruct a.
        generalize (H5 s r); simpl.
        destruct (string_dec s s); intuition.
        destruct H1; intuition; discriminate.
      + inversion H; subst. destruct a; destruct p.
        simpl in deq. inversion deq; subst; clear deq.
        simpl in H3.
        specialize (H3 r0).
        specialize (H5 s0 r); specialize (H2 s0 r0).
        simpl in H2, H5.
        destruct (string_dec s0 s0); intuition.
        destruct H0 as [? [eq1 su1]].
        destruct H1 as [? [eq2 su2]].
        inversion eq1; inversion eq2; subst.
        intuition; subst.
        
        constructor; trivial.
        destruct (Rec_subtype_cons_inv sub1) as [pf'11 [pf'12 sub'1]].
        destruct (Rec_subtype_cons_inv sub2) as [pf'21 [pf'22 sub'2]].
        eapply (IHsrl (is_list_sorted_cons_inv _ pf) k k2); trivial.
        * erewrite (Rec_pr_irrel); eauto.
        * erewrite (Rec_pr_irrel _ _ pf'12).
          erewrite (Rec_pr_irrel _ _ (is_list_sorted_cons_inv ODT_lt_dec pf)).
          eauto.
        * inversion sub'1; rtype_equalizer; subst; qeauto.
        * inversion sub'1; rtype_equalizer; subst; qeauto.
        * inversion sub'2; rtype_equalizer; subst; qeauto.
        * inversion sub'2; rtype_equalizer; subst; qeauto.
    - inversion sub2; subst; trivial;
        rtype_equalizer; subst; trivial.
      subst. f_equal; eauto.
    - inversion sub2; subst; trivial;
        rtype_equalizer; subst; trivial.
      subst. f_equal; eauto.
    - apply canon_equiv in H. rewrite H in H0.
      apply rtype_fequal; simpl.
      f_equal. apply canon_equiv. split; trivial.
      inversion sub2; subst; trivial.
      + apply canon_equiv in H3. destruct H3; trivial.
      + apply canon_equiv in H1. apply canon_equiv in H2.
        rewrite <- H1, <- H2; trivial.
    - invcs sub2; trivial.
      f_equal.
      apply foreign_type_sub_part; split; trivial.
  Qed.

  Lemma wf_rtype_subtype_refl τ pf1 pf2:
    exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) τ pf1 <:
    exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) τ pf2.
Proof.
    generalize (wf_rtype_ext pf1 pf2); intros s.
    subst. reflexivity.
  Qed.

  Lemma Rec_subtype_cons_eq {kks rrrlrlpf1 pf2} :
    Rec k₁ ((s, r₁) :: rl₁) pf1 <: Rec k₂ ((s, r₂) :: rl₂) pf2 ->
                                   r₁ <: r₂.
Proof.
    inversion 1; subst; rtype_equalizer.
    subst; intros. reflexivity.
    destruct rl1; try discriminate.
    destruct rl2; try discriminate.
    destruct p; destruct p0.
    simpl in H1, H4.
    inversion H1; subst.
    inversion H4; subst.
    rtype_equalizer. subst.
    specialize (H3 s r₂).
    simpl in H3.
    destruct (string_dec s s); intuition.
    destruct H0 as [? [inv sub]].
    inversion inv; subst.
    auto.
  Qed.

  Lemma SToppf τ : τ <: exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) ⊤₀ pf.
Proof.
    generalize (STop τ).
    destruct τ; unfold Top; intros.
    eapply subtype_ext; eauto.
  Qed.

  Lemma SBottompf τ : exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) ⊥₀ pf <: τ.
Proof.
    generalize (SBottom τ).
    destruct τ; unfold Top; intros.
    eapply subtype_ext; eauto.
  Qed.

  Lemma SRefl₀ τ₀ pf : exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) τ₀ pf <: exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) τ₀ pf.
Proof.
    apply SRefl.
  Qed.

  Lemma SColl₀ τ₁ pf₁ τ₂ pf₂ :
    exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) τ₁ pf₁ <: exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) τ₂ pf₂ ->
                                                             exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) (Coll₀ τ₁) pf₁ <: exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) (Coll₀ τ₂) pf₂.
Proof.
    apply SColl.
  Qed.

  Lemma SReck1 rl1 rl2 k2 pf1 pf2 : (forall s r' pf',
                                          lookup string_dec rl2 s = Some r' ->
                                          exists r pf, lookup string_dec rl1 s = Some r /\
                                                       subtype (exist _ r pf) (exist _ r' pf')) ->
                                      (k2 = Closed -> k1 = Closed /\
                                                      (forall s, In s (domain rl1) -> In s (domain rl2))) ->
                                      exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) (Reck1 rl1) pf1 <:
    exist (fun τ₀ : rtype₀ => wf_rtype₀ τ₀ = true) (Reck2 rl2) pf2.
Proof.
    intros.
    destruct (from_Recrl1 pf1) as [l1' [pf1' [eq11 eq12]]].
    destruct (from_Recrl2 pf2) as [l2' [pf2' [eq21 eq22]]].
    subst.
    rewrite <- eq12, <- eq22.
    apply SRec.
    intros.
    apply lookup_map_some in H1.
    destruct (H s _ (proj2_sig r') H1) as [r [rpf [l1 s1]]].
    exists (exist _ r rpf).
    split.
    apply lookup_map_some; simpl. auto.
    destruct r'; simpl in *; auto.

    intuition.
    specialize (H3 s).
    unfold domain in H3; repeat rewrite map_map in H3.
    simpl in H3.
    auto.
  Qed.

  Lemma subtype_Rec_sublist {klpfklpf₂} :
    Rec klpf₁ <: Rec klpf₂ -> sublist (domain l₂) (domain l₁).
Proof.
    inversion 1; subst; rtype_equalizer; subst; try reflexivity.
    generalize pfpf₂.
    repeat rewrite is_list_sorted_StronglySorted by eapply StrictOrder_Transitive.
    intros.
    eapply StronglySorted_incl_sublist; eauto.
    eapply SRec_closed_in_domain; eauto.
  Qed.


  Lemma subtype_Rec_closed_domain {klpflpf₂} :
    Rec klpf₁ <: Rec Closed lpf₂ -> (domain l₂) = (domain l₁).
Proof.
    intros sub.
    apply Sorted_incl_both_eq; try eapply is_list_sorted_Sorted_iff; eauto
    ; intros; eapply (SRec_closed_equiv_domain sub); trivial.
  Qed.

  Lemma subtype_Rec_closed2_closed1 {k1 l1 pf1 l2 pf2}:
    Rec k1 l1 pf1 <: Rec Closed l2 pf2 ->
                     k1 = Closed.
Proof.
    inversion 1; subst; intuition.
  Qed.

  Lemma is_list_sorted_in_cons_lookup_none {B} {b τ₃ s} (τ₁:B) {rl0 rl1 τ₀} (τ₂:B)
        (pf1 : @is_list_sorted string _ ODT_lt_dec (domain ((b, τ₃) :: rl1)) = true)
        (x : @is_list_sorted string _ ODT_lt_dec (domain ((s, τ₁) :: rl0)) = true)
        (inn:In (b, τ₀) rl0) :
    lookup string_dec ((b, τ₂) :: rl1) s = None.
Proof.
    apply (sorted_cons_in _ _ _ x) in inn.
    simpl in inn.
    assert (isl:is_list_sorted ODT_lt_dec (s::domain ((b, τ₃) :: rl1)) = true) by (apply is_list_sorted_cons; intuition).
    apply is_list_sorted_NoDup in isl; try eapply StringOrder.lt_strorder.
    inversion isl; subst.
    apply lookup_nin_none.
    rewrite domain_cons; trivial.
  Qed.
  
  Lemma Rec_subtype_In {rl0 pf0 rl1 pf1 b τ₁ τ₂} :
    Rec Open rl0 pf0 <:
    Rec Open rl1 pf1 ->
    In (b, τ₁) rl0 -> In (b, τ₂) rl1 -> τ₁ <: τ₂.
Proof.
    revert rl0 pf0 pf1 b τ₁ τ₂. induction rl1; [simpl; intuition| ].
    intros.
    destruct rl0; simpl in H1; [intuition |].
    destruct a; destruct p.
    simpl in H0.
    destruct H0.
    - inversion H0; subst; clear H0.
      destruct H1.
      + inversion H0; subst; clear H0.
        eapply Rec_subtype_cons_eq; eauto.
      + apply Rec_subtype_cons_inv2 in H.
        destruct H. eapply (IHrl1 _ _ _ _ _ _ H); simpl; eauto.
    - destruct H1.
      + inversion H1; subst; clear H1.
        apply Rec_subtype_cons_inv1 in H.
        * destruct H as [??].
          revert H0 H. clear.
          revert rl1 b τ₁ τ₂ pf1 x. induction rl0; [simpl; intuition | ].
          intros. simpl in H0. destruct H0; subst.
          apply Rec_subtype_cons_eq in H; trivial.
          destruct a.
          apply Rec_subtype_cons_inv1 in H.
          destruct H as [??].
          eauto.
          eapply is_list_sorted_in_cons_lookup_none; eauto.
        * eapply is_list_sorted_in_cons_lookup_none; eauto.
      + rewrite (Rec_subtype_cons_weaken Open s r rl1
                                          pf1 (is_list_sorted_cons_inv _ pf1)) in H.
        apply (IHrl1 _ _ _ b τ₁ τ₂ H); simpl; auto.
  Qed.
  
End RSubtypeProp.