text:
(*
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 * http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 *)

Require Import String.
Require Import List.
Require Import Bool.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Permutation.
Require Import Eqdep_dec.
Require Import Program.
Require Import Utils.
Require Import DataSystem.
Require Import NNRSSystem.
Require Import NNRSimpSystem.
Require Import NNRStoNNRSimp.

Section TNNRStoNNRSimp.

  Context {m:basic_model}.
  Context (τconstants:tbindings).

  Definition lift_pdtype (τo:option rtype) : rtype
    := match τo with
       | Some τ => τ
       | Noneu => ⊥
       end.

  Definition pd_tbindings_lift (Γ:TNNRS.pd_tbindings) : TNNRSimp.pd_tbindings
    := map_codomain lift_pdtype Γ.

  Lemma lookup_pd_tbindings_lift Γ v :
    lookup equiv_dec (pd_tbindings_lift Γ) v = lift lift_pdtype (lookup equiv_dec Γ v).
  Proof.
    apply lookup_map_codomain.
  Qed.

  Lemma tnnrs_expr_to_nnrs_expr_correct_f:
    forall Γc Γ (e:nnrs_expr) (τ:rtype),
      ([ Γc ; Γ  ⊢ e ▷ τ ])%nnrs -> [ Γc ; pd_tbindings_lift Γ  ⊢ (nnrs_expr_to_nnrs_imp_expr e) ▷ τ ]%nnrs_imp.
  Proof.
    Hint Constructors nnrs_imp_expr_type : qcert.
    intros Γc Γ e.
    revert Γ.
    induction e
    ; simpl
    ; intros Γ τ typ
    ; invcs typ
    ; econstructor; eauto.
    - rewrite lookup_pd_tbindings_lift.
      rewrite H1.
      simpl; trivial.
  Qed.

  Lemma tnnrs_expr_to_nnrs_expr_correct_b:
    forall Γc Γ (e:nnrs_expr) (τ:rtype),
      (forall x, In x (nnrs_expr_free_vars e) -> lookup equiv_dec Γ x <> Some None) ->
      [ Γc ; pd_tbindings_lift Γ  ⊢ (nnrs_expr_to_nnrs_imp_expr e) ▷ τ ]%nnrs_imp -> ([ Γc ; Γ  ⊢ e ▷ τ ])%nnrs.
  Proof.
    Hint Constructors nnrs_expr_type : qcert.
    intros Γc Γ e.
    revert Γ.
    induction e
    ; simpl
    ; intros Γ τ fns typ
    ; invcs typ
    ; econstructor; eauto.
    - rewrite lookup_pd_tbindings_lift in H1.
      apply some_lift in H1.
      destruct H1 as [???]; subst.
      specialize (fns v); unfold var in *.
      rewrite e in *.
      destruct x; simpl; intuition.
    - eapply IHe1; trivial.
      intros; apply fns.
      rewrite in_app_iff; intuition.
    - eapply IHe2; trivial.
      intros; apply fns.
      rewrite in_app_iff; intuition.
  Qed.

  Definition concat_tenvs
             (Γ :TNNRS.pd_tbindings)
             (Δc :TNNRS.mc_tbindings)
             (Δd :TNNRS.md_tbindings)
    : TNNRSimp.pd_tbindings
    := pd_tbindings_lift Γ ++ map_codomain Coll Δc ++ Δd.

  Lemma concat_tenvs_cons (Γ :TNNRS.pd_tbindings)
        (Δc :TNNRS.mc_tbindings)
        (Δd :TNNRS.md_tbindings) s τ :
    (s,lift_pdtype τ)::concat_tenvs Γ Δc Δd = concat_tenvs ((s,τ)::Γ) Δc Δd.
  Proof.
    reflexivity.
  Qed.

  Lemma concat_tenvs_cons_some (Γ :TNNRS.pd_tbindings)
        (Δc :TNNRS.mc_tbindings)
        (Δd :TNNRS.md_tbindings) s τ :
    (s, τ)::concat_tenvs Γ Δc Δd = concat_tenvs ((s,Some τ)::Γ) Δc Δd.
  Proof.
    reflexivity.
  Qed.

  (* Move this to TNNRS *)
  Lemma nnrs_expr_type_lookup_on_equiv {Γc Γ₁ e τ} :
    ([ Γc ; Γ₁  ⊢ e ▷ τ ])%nnrs ->
    forall Γ₂,
      lookup_equiv_on (nnrs_expr_free_vars e) Γ₁ Γ₂ ->
      ([ Γc ; Γ₂  ⊢ e ▷ τ ])%nnrs.
  Proof.
    revert Γ₁ τ.
    induction e; intros Γ₁ τ typ Γ₂ leo
    ; invcs typ; simpl in *; subst; econstructor; eauto 3.
    - rewrite <- leo; simpl; tauto.
    - eapply IHe1; eauto.
      unfold lookup_equiv_on in *; intuition.
    - eapply IHe2; eauto.
      unfold lookup_equiv_on in *; intuition.
  Qed.

  Lemma nnrs_expr_to_nnrs_imp_expr_free_vars (e:nnrs_expr) :
    nnrs_imp_expr_free_vars (nnrs_expr_to_nnrs_imp_expr e) = nnrs_expr_free_vars e.
  Proof.
    induction e; simpl; congruence.
  Qed.

  Lemma nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment s v:
    ~ In v (nnrs_stmt_free_env_vars s) ->
    ~ In v (nnrs_stmt_free_mcenv_vars s) ->
    nnrs_imp_stmt_var_usage (nnrs_stmt_to_nnrs_imp_stmt s) v <> VarMayBeUsedWithoutAssignment.
  Proof.
    nnrs_stmt_cases (induction s) Case
    ; simpl
    ; repeat rewrite in_app_iff
    ; intros nin1 nin2.
    - Case "NNRSSeq"%string.
      match_destr; intuition.
    - Case "NNRSLet"%string.
      match_case; intros eqq.
      + rewrite nnrs_imp_expr_may_use_free_vars in eqq.
        rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq.
        tauto.
      + unfold equiv_decb. destruct (v0 == v); try congruence.
        apply IHs; try tauto.
        rewrite remove_in_neq by eauto.
        tauto.
    - Case "NNRSLetMut"%string.
      unfold equiv_decb.
      destruct (v0 == v); try congruence.
      match_destr; try tauto.
      apply IHs2; try tauto.
      rewrite remove_in_neq by eauto.
      tauto.
    - Case "NNRSLetMutColl"%string.
      unfold equiv_decb.
      destruct (v0 == v); try congruence.
      match_destr; try tauto.
      + elim IHs1; try tauto.
        rewrite remove_in_neq by eauto.
        tauto.
      + apply IHs2; try tauto.
        rewrite remove_in_neq by eauto.
        tauto.
    - Case "NNRSAssign"%string.
      match_case; intros eqq.
      + rewrite nnrs_imp_expr_may_use_free_vars in eqq.
        rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq.
        tauto.
      + match_destr.
    - Case "NNRSPush"%string.
      unfold equiv_decb.
      destruct (v == v0); destruct (v0 == v); try congruence; simpl.
      + tauto.
      + match_case; intros eqq.
        rewrite nnrs_imp_expr_may_use_free_vars in eqq.
        rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq.
        tauto.
    - Case "NNRSFor"%string.
      match_case; intros eqq.
      + rewrite nnrs_imp_expr_may_use_free_vars in eqq.
        rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq.
        tauto.
      + unfold equiv_decb. destruct (v0 == v); try congruence.
        match_case; intros eqq2.
        elim IHs; try tauto.
        rewrite remove_in_neq by eauto.
        tauto.
    - Case "NNRSIf"%string.
      match_case; intros eqq.
      + rewrite nnrs_imp_expr_may_use_free_vars in eqq.
        rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq.
        tauto.
      + match_case; intros eqq2
        ; try (match_case; intros eqq3).
        * elim IHs2; try tauto.
        * elim IHs1; try tauto.
        * elim IHs2; try tauto.
    - Case "NNRSEither"%string.
      match_case; intros eqq.
      + rewrite nnrs_imp_expr_may_use_free_vars in eqq.
        rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq.
        tauto.
      + destruct (v0 == v).
        * destruct (v1 == v); try congruence.
          match_case; intros eqq2.
          elim IHs2; try tauto.
          rewrite remove_in_neq by eauto.
          tauto.
        * { match_case; intros eqq2.
            - destruct (v1 == v); try congruence.
              match_case; intros eqq3.
              elim IHs2; try tauto.
              rewrite remove_in_neq by eauto.
              tauto.
            - elim IHs1; try tauto.
              rewrite remove_in_neq by eauto.
              tauto.
            - destruct (v1 == v); try congruence.
              match_case; intros eqq3.
              elim IHs2; try tauto.
              rewrite remove_in_neq by eauto.
              tauto.
          }
  Qed.

  Lemma nnrs_stmt_to_nnrs_imp_stmt_must_assign_assigned {s dΓ dΔc dΔd} :
    nnrs_stmt_cross_shadow_free_under s dΓ dΔc dΔd ->
    forall v,
      In v (dΔd) ->
      nnrs_stmt_must_assign s v ->
      nnrs_imp_stmt_var_usage (nnrs_stmt_to_nnrs_imp_stmt s) v = VarMustBeAssigned.
  Proof.
    revert dΓ dΔc dΔd.
    nnrs_stmt_cases (induction s) Case
    ; simpl
    ; repeat rewrite in_app_iff
    ; intros dΓ dΔc dΔd cs vv inn ma.
    - Case "NNRSSeq"%string.
      specialize (IHs1 dΓ dΔc dΔd).
      specialize (IHs2 dΓ dΔc dΔd).
      (match_case; intro); intuition
      ; try solve[(eelim (nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment)
                   ; [| | eauto]; eauto)]
      ; try congruence.
      + rewrite H3 in H; intuition.
      + eelim nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment; [| | eauto]; eauto.
        * apply nnrs_stmt_cross_shadow_free_under_free_env_mdenv in H0.
          specialize (H0 vv); tauto.
        * apply nnrs_stmt_cross_shadow_free_under_free_mcenv_mdenv in H0.
          specialize (H0 vv); tauto.
      + rewrite H3 in H; congruence.
    - Case "NNRSLet"%string.
      match_case; intros eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars in eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars_neg in eqq
      ; try rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq
      ; intuition.
      + specialize (H1 vv); intuition.
      + unfold equiv_decb; destruct (v == vv); unfold equiv, complement in *
        ; subst
        ; intuition; eauto.
    - Case "NNRSLetMut"%string.
      unfold equiv_decb; destruct (v == vv); unfold equiv, complement in *
      ; subst
      ; intuition.
      + rewrite (IHs1 _ _ _  H2 vv); simpl; tauto.
      + match_case; intros eqq.
        * { eelim nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment; [| | eauto]; eauto.
            - apply nnrs_stmt_cross_shadow_free_under_free_env_mdenv in H2.
              specialize (H2 vv); simpl in H2; tauto.
            - apply nnrs_stmt_cross_shadow_free_under_free_mcenv_mdenv in H2.
              specialize (H2 vv); simpl in H2; tauto.
          }
        * eauto.
    - Case "NNRSLetMutColl"%string.
      unfold equiv_decb; destruct (v == vv); unfold equiv, complement in *
      ; subst
      ; intuition.
      + rewrite (IHs1 _ _ _  H2 vv); simpl; tauto.
      + match_case; intros eqq.
        * { eelim nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment; [| | eauto]; eauto.
            - apply nnrs_stmt_cross_shadow_free_under_free_env_mdenv in H2.
              specialize (H2 vv); simpl in H2; tauto.
            - apply nnrs_stmt_cross_shadow_free_under_free_mcenv_mdenv in H2.
              specialize (H2 vv); simpl in H2; tauto.
          }
        * eauto.
    - Case "NNRSAssign"%string.
      subst.
      match_case; intros eqq.
      + rewrite nnrs_imp_expr_may_use_free_vars in eqq.
        rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq.
        subst; intuition.
        specialize (H1 vv); tauto.
      + unfold equiv_decb; destruct (vv == vv); try congruence.
    - Case "NNRSPush"%string.
      contradiction.
    - Case "NNRSFor"%string.
      match_case; intros eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars in eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars_neg in eqq
      ; try rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq
      ; intuition.
    - Case "NNRSIf"%string.
      match_case; intros eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars in eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars_neg in eqq
      ; try rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq
      ; intuition.
      + specialize (H3 vv); tauto.
      + rewrite (IHs1 _ _ _ H0); trivial.
        rewrite (IHs2 _ _ _ H5); trivial.
    - Case "NNRSEither"%string.
      match_case; intros eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars in eqq
      ; try rewrite nnrs_imp_expr_may_use_free_vars_neg in eqq
      ; try rewrite nnrs_expr_to_nnrs_imp_expr_free_vars in eqq
      ; intuition.
      + specialize (H3 vv); tauto.
      + specialize (IHs1 _ _ _ H7 _ inn H1).
        specialize (IHs2 _ _ _ H9 _ inn H2).
        rewrite IHs1, IHs2.
        destruct (v == vv); try congruence.
        destruct (v0 == vv); try congruence.
  Qed.

  Lemma concat_tenvs_lookup_equiv_env_mc_cons Γ Δc Δd v τ :
    ~ In v (domain Γ) ->
    lookup_equiv (concat_tenvs ((v,Some (Coll τ))::Γ) Δc Δd)
                 (concat_tenvs Γ ((v,τ)::Δc) Δd).
  Proof.
    unfold concat_tenvs, lookup_equiv.
    intros nin x.
    repeat rewrite lookup_app; simpl.
    destruct (string_eqdec x v); unfold equiv, complement in *.
    + subst. rewrite lookup_nin_none; trivial.
      unfold pd_tbindings_lift.
      rewrite domain_map_codomain; trivial.
    + trivial.
  Qed.

  Lemma concat_tenvs_lookup_equiv_mc_md  Γ Δc Δd v τ :
    ~ In v (domain Δc) ->
    lookup_equiv (concat_tenvs Γ ((v,τ)::Δc) Δd)
                 (concat_tenvs Γ Δc ((v,Coll τ)::Δd)).
  Proof.
    unfold concat_tenvs, lookup_equiv.
    intros nin x.
    repeat rewrite lookup_app.
    match_destr; simpl.
    destruct (string_eqdec x v); unfold equiv, complement in *.
    + subst.
      rewrite lookup_nin_none; trivial.
      rewrite domain_map_codomain; trivial.
    + match_destr.
  Qed.

  Lemma concat_tenvs_lookup_equiv_env_md Γ Δc Δd v τ :
    ~ In v (domain Γ) ->
    ~ In v (domain Δc) ->
    lookup_equiv (concat_tenvs ((v,τ)::Γ) Δc Δd)
                 (concat_tenvs Γ Δc ((v,lift_pdtype τ)::Δd)).
  Proof.
    intros nin1 nin2 x.
    unfold concat_tenvs, lookup_equiv.
    repeat rewrite lookup_app; simpl.
    destruct (string_eqdec x v); unfold equiv, complement in *.
    + subst.
      repeat rewrite lookup_nin_none; trivial
      ; unfold pd_tbindings_lift; rewrite domain_map_codomain; trivial.
    + trivial.
  Qed.

  Lemma nnrs_stmt_unused_tenv_free_env {Γc Γ Δc Δd s} :
    [ Γc ; Γ , Δc , Δd ⊢ s ]%nnrs ->
    forall x,
      lookup equiv_dec Γ x = Some None ->
      ~ In x (nnrs_stmt_free_env_vars s).
  Proof.
    revert Γ Δc Δd.
    nnrs_stmt_cases (induction s) Case
    ; simpl; intros Γ Δc Δd typ x eqq
    ; invcs typ
    ; repeat rewrite in_app_iff.
    - Case "NNRSSeq"%string.
      intuition eauto.
    - Case "NNRSLet"%string.
      intuition eauto.
      + eapply nnrs_expr_unused_tenv_free_env; eauto.
      + apply remove_inv in H0.
        intuition.
        eapply IHs; eauto; simpl.
        match_destr; congruence.
    - Case "NNRSLetMut"%string.
      intuition.
      + eapply IHs1; eauto.
      + apply remove_inv in H0; intuition.
        eapply IHs2; eauto.
        simpl; match_destr; congruence.
    - Case "NNRSLetMut"%string.
      intuition.
      + eapply IHs1; eauto.
      + apply remove_inv in H0; intuition.
        eapply IHs2; eauto.
        simpl; match_destr; congruence.
    - Case "NNRSLetMutColl"%string.
      intuition.
      + eapply IHs1; eauto.
      + apply remove_inv in H0; intuition.
        eapply IHs2; eauto.
        simpl; match_destr; congruence.
    - Case "NNRSAssign"%string.
      eapply nnrs_expr_unused_tenv_free_env; eauto.
    - Case "NNRSPush"%string.
      eapply nnrs_expr_unused_tenv_free_env; eauto.
    - Case "NNRSFor"%string.
      intuition eauto.
      + apply (nnrs_expr_unused_tenv_free_env H4) in eqq; tauto.
      + apply remove_inv in H0.
        intuition.
        eapply IHs; eauto; simpl.
        match_destr; congruence.
    - Case "NNRSIf"%string.
      intuition eauto.
      eapply nnrs_expr_unused_tenv_free_env; eauto.
    - Case "NNRSEither"%string.
      intuition eauto.
      + eapply nnrs_expr_unused_tenv_free_env; eauto.
      + apply remove_inv in H.
        intuition.
        eapply IHs1; eauto; simpl.
        match_destr; congruence.
      + apply remove_inv in H.
        intuition.
        eapply IHs2; eauto; simpl.
        match_destr; congruence.
  Qed.

  Lemma tnnrs_stmt_to_nnrs_imp_correct_f
        {Γc:tbindings} {Γ:TNNRS.pd_tbindings}
        (Δc:TNNRS.mc_tbindings) (Δd:TNNRS.md_tbindings) s :
    [ Γc ; Γ , Δc , Δd ⊢ s ]%nnrs ->
    nnrs_stmt_cross_shadow_free_under s (domain Γ) (domain Δc) (domain Δd)->
    [ Γc ; concat_tenvs Γ Δc Δd ⊢  nnrs_stmt_to_nnrs_imp_stmt s ]%nnrs_imp.
  Proof.

    Ltac prove_expr_f_t
         := match goal with
            | [H: [ _ ; _ ⊢ ?e ▷ _ ]%nnrs |-
               [ _ ; _ ⊢ nnrs_expr_to_nnrs_imp_expr ?e ▷ _ ] %nnrs_imp ] =>
              apply tnnrs_expr_to_nnrs_expr_correct_f in H
              ; apply (nnrs_imp_expr_type_lookup_equiv_on H)
              ; rewrite nnrs_expr_to_nnrs_imp_expr_free_vars
              ; unfold lookup_equiv_on; intros ? inn
              ; unfold concat_tenvs; repeat rewrite lookup_app
              ; match_destr
              ; repeat rewrite lookup_nin_none; trivial
              ; try rewrite domain_map_codomain; trivial
              ; match goal with
                | [H1:disjoint ?l1 ?l2,
                      H2: In ?x ?l1 |- ~ In ?x ?l2 ] =>
                  exact (H1 x inn)
                end
            end.

    Hint Constructors nnrs_imp_stmt_type : qcert.
    revert Γ Δc Δd.
    nnrs_stmt_cases (induction s) Case
    ; simpl; intros Γ Δc Δd typ sf
    ; invcs typ.
    - Case "NNRSSeq"%string.
      econstructor; intuition eauto.
    - Case "NNRSLet"%string.
      destruct sf as [disj1 [disj2 [nin1 [nin2 sf]]]].
      econstructor.
      + prove_expr_f_t.
      + specialize (IHs ((v, Some τ) :: Γ)); unfold concat_tenvs in *.
        simpl in IHs; eauto.
    - Case "NNRSLetMut"%string.
      destruct sf as [ninΓ [ninΔc [ninΔd [sf1 sf2]]]].
      apply (nnrs_stmt_to_nnrs_imp_stmt_must_assign_assigned sf1) in H5
      ; simpl; try tauto.
      eapply (type_NNRSimpLetNone _ _ τ); simpl.
      + rewrite H5; congruence.
      + specialize (IHs1 _ _ _ H6 sf1).
        specialize (IHs2 _ _ _ H7 sf2).
        econstructor.
        * eapply nnrs_imp_stmt_type_lookup_equiv_prop; eauto.
          rewrite concat_tenvs_cons_some.
          apply concat_tenvs_lookup_equiv_env_md; eauto.
        * eauto.
    - Case "NNRSLetMut"%string.
      destruct sf as [ninΓ [ninΔc [ninΔd [sf1 sf2]]]].
      eapply (type_NNRSimpLetNone _ _ τ); simpl.
      + match_case; intros eqq; try congruence.
        * { apply nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment in eqq.
            - contradiction.
            - apply nnrs_stmt_cross_shadow_free_under_free_env_mdenv in sf1.
              specialize (sf1 v); simpl in sf1; tauto.
            - apply nnrs_stmt_cross_shadow_free_under_free_mcenv_mdenv in sf1.
              specialize (sf1 v); simpl in sf1; tauto.
          }
        * { apply nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment.
            - apply (nnrs_stmt_unused_tenv_free_env H6 v); simpl.
              match_destr; try congruence.
            - apply nnrs_stmt_cross_shadow_free_under_free_mcenv_env in sf2.
              eapply disjoint_cons_inv2 in sf2; tauto.
          }
      + rewrite concat_tenvs_cons_some.
        econstructor.
        * eapply nnrs_imp_stmt_type_lookup_equiv_prop; eauto.
          apply concat_tenvs_lookup_equiv_env_md; eauto.
        * eapply IHs2; eauto.
          apply nnrs_stmt_type_env_cons_none_some; eauto.
    - Case "NNRSLetMutColl"%string.
      destruct sf as [ninΓ [ninΔc [ninΔd [sf1 sf2]]]].
      eapply (type_NNRSimpLetDef _ _ (Coll τ)); simpl.
      + repeat (econstructor; simpl).
      + rewrite concat_tenvs_cons_some.
        econstructor; eauto.
        eapply nnrs_imp_stmt_type_lookup_equiv_prop; eauto.
        apply concat_tenvs_lookup_equiv_env_mc_cons; eauto.
    - Case "NNRSAssign"%string.
      destruct sf as [disjc [disjd [ninΓ ninΔc]]].
      econstructor; eauto.
      + prove_expr_f_t.
      + unfold concat_tenvs; repeat rewrite lookup_app.
        rewrite H5.
        repeat rewrite lookup_nin_none; trivial
        ; unfold pd_tbindings_lift
        ; try rewrite domain_map_codomain; trivial.
    - Case "NNRSPush"%string.
      destruct sf as [disjc [disjd [ninΓ ninΔc]]].
      assert (lo:lookup equiv_dec (concat_tenvs Γ Δc Δd) v = Some (Coll τ)).
      {
        unfold concat_tenvs; repeat rewrite lookup_app.
        rewrite lookup_map_codomain.
        unfold equiv_dec, string_eqdec.
        rewrite H5.
        repeat rewrite lookup_nin_none; trivial
        ; unfold pd_tbindings_lift
        ; try rewrite domain_map_codomain; trivial.
      }
      econstructor; qeauto.
      econstructor; qeauto.
      + econstructor.
      + econstructor; [econstructor | ].
         prove_expr_f_t.
    - Case "NNRSFor"%string.
      destruct sf as [disjc [disjd [ninΔc [ninΔd sf]]]].
      econstructor.
      + prove_expr_f_t.
      + specialize (IHs ((v, Some τ) :: Γ)); unfold concat_tenvs in *.
         simpl in IHs; eauto.
    - Case "NNRSIf"%string.
      destruct sf as [disjc [disjd [sf1 sf2]]].
      econstructor; eauto.
      prove_expr_f_t.
    - Case "NNRSEither"%string.
      destruct sf as [disjc [disjd [nin1Δc [nin1Δd [nin2Δc [nin2Δd [sf1 sf2]]]]]]].
      econstructor.
      + prove_expr_f_t.
      + specialize (IHs1 ((v, Some τl) :: Γ)); unfold concat_tenvs in *.
         simpl in IHs1; eauto.
      + specialize (IHs2 ((v0, Some τr) :: Γ)); unfold concat_tenvs in *.
         simpl in IHs2; eauto.
  Qed.

  Theorem tnnrs_to_nnrs_imp_correct_f {Γc} {si:nnrs} {τ} :
    [ Γc ⊢ si ▷ τ ]%nnrs ->
    nnrs_cross_shadow_free si ->
    [ Γc ⊢ nnrs_to_nnrs_imp si ▷ τ ]%nnrs_imp.
  Proof.
    destruct si; simpl.
    intros typ sf.
    apply tnnrs_stmt_to_nnrs_imp_correct_f in typ; eauto.
    split.
    - unfold nnrs_cross_shadow_free in sf; simpl in sf.
      apply nnrs_stmt_to_nnrs_imp_stmt_not_used_without_assignment.
      + apply nnrs_stmt_cross_shadow_free_under_free_env_mdenv in sf.
         apply disjoint_cons_inv2 in sf; tauto.
      + apply nnrs_stmt_cross_shadow_free_under_free_mcenv_mdenv in sf.
        apply disjoint_cons_inv2 in sf; tauto.
    - unfold concat_tenvs in typ; simpl in typ; trivial.
  Qed.

  Theorem tnnrs_to_nnrs_imp_top_correct_f {Γc} {si:nnrs} {τ} :
    [ Γc ⊢ si ▷ τ ]%nnrs ->
    forall sep,
      [ Γc ⊢ nnrs_to_nnrs_imp_top sep si ▷ τ ]%nnrs_imp.
  Proof.
    intros typ sep.
    apply tnnrs_to_nnrs_imp_correct_f.
    - apply nnrs_uncross_shadow_type; trivial.
    - apply nnrs_uncross_shadow_free.
  Qed.

  Lemma nnrs_stmt_to_nnrs_imp_stmt_assigned_must_assign {s v} :
    nnrs_imp_stmt_var_usage (nnrs_stmt_to_nnrs_imp_stmt s) v = VarMustBeAssigned ->
    nnrs_stmt_must_assign s v.
  Proof.
    nnrs_stmt_cases (induction s) Case
    ; simpl; intros eqq
    ; try solve [repeat match_destr_in eqq; try tauto].
    - Case "NNRSLetMut"%string.
      unfold equiv_decb in *.
      destruct (v0 == v); try discriminate.
      match_destr_in eqq; auto.
    - Case "NNRSAssign"%string.
      unfold equiv_decb in *.
      destruct (v0 == v); try discriminate.
      match_destr_in eqq; tauto.
      match_destr_in eqq; tauto.
    - Case "NNRSPush"%string.
      unfold equiv_decb in eqq.
      destruct (v0 == v)
      ; destruct (v == v0)
      ; simpl in eqq
      ; try congruence.
      match_destr_in eqq.
  Qed.

    Lemma nnrs_imp_stmt_must_free {s v} :
      nnrs_imp_stmt_var_usage s v = VarMustBeAssigned ->
      In v (nnrs_imp_stmt_free_vars s).
    Proof.
      induction s; simpl
      ; try (match_case; intros eqq; intuition)
      ; unfold equiv_decb in *
      ; try (destruct (v0 == v); try intuition congruence).
      - congruence.
      - rewrite in_app_iff.
        right.
         apply remove_in_neq; intuition.
      - match_destr_in H.
      - repeat rewrite in_app_iff.
        match_case_in H; intros eqq1; rewrite eqq1 in H; try congruence
        ; match_case_in H; intros eqq2; rewrite eqq2 in H; try congruence.
        intuition.
      - destruct (v1 == v); try congruence.
        repeat rewrite in_app_iff.
        match_case_in H; intros eqq1; rewrite eqq1 in H; try congruence.
      -  repeat rewrite in_app_iff.
         match_case_in H; intros eqq1; rewrite eqq1 in H; try congruence
         ; destruct (v1 == v); try congruence
        ; match_case_in H; intros eqq2; rewrite eqq2 in H; try congruence.
         intuition.
         right; left.
         apply remove_in_neq; intuition.
    Qed.

    Lemma nnrs_stmt_to_nnrs_imp_free_md_free {Γc Γ Δc Δd s} :
    [ Γc ; Γ , Δc , Δd ⊢ s ]%nnrs -> forall v,
    ~ In v (nnrs_stmt_free_mdenv_vars s) ->
    nnrs_imp_stmt_var_usage (nnrs_stmt_to_nnrs_imp_stmt s) v <>
    VarMayBeUsedWithoutAssignment ->
    ~ In v (nnrs_imp_stmt_free_vars (nnrs_stmt_to_nnrs_imp_stmt s)).
  Proof.
    revert Γ Δc Δd.
    nnrs_stmt_cases (induction s) Case
    ; simpl
    ; intros  Γ Δc Δd typ vv
    ; repeat rewrite in_app_iff
    ; intros nin neq.
    - Case "NNRSSeq"%string.
      invcs typ.
      specialize (IHs1 _ _ _  H4 vv).
      specialize (IHs2 _ _ _  H5 vv).
      match_case_in neq; intros eqq1; rewrite eqq1 in neq; try congruence.
      + elim IHs1; eauto; try congruence.
        apply nnrs_imp_stmt_must_free; trivial.
      + intuition congruence.
    - Case "NNRSLet"%string.
      match_case_in neq; intros eqq1; rewrite eqq1 in neq; try congruence.
      apply nnrs_imp_expr_may_use_free_vars_neg in eqq1.
      intros [inn|inn]; auto.
      apply remove_inv in inn.
      destruct inn as [inn ?].
      unfold equiv_decb in *.
      destruct (v == vv); try congruence.
      revert inn.
      invcs typ.
      eapply IHs; eauto.
    - Case "NNRSLetMut"%string.
      unfold equiv_decb in *.
      destruct (v == vv); [rewrite e; apply remove_In | ].
      rewrite <- remove_in_neq; try eauto.
      rewrite in_app_iff.
      match_case_in neq; intros eqq1; rewrite eqq1 in neq; try congruence.
      + apply nnrs_stmt_to_nnrs_imp_stmt_assigned_must_assign in eqq1.
         apply nnrs_stmt_must_assign_is_free in eqq1.
         eapply remove_in_neq in eqq1; eauto.
      +  intros [inn|inn].
         * invcs typ; eapply IHs1; eauto; intuition; try congruence
           ; rewrite <- remove_in_neq in H0 by eauto
           ; tauto.
         * revert inn. invcs typ; eapply IHs2; eauto.
    - Case "NNRSLetMutColl"%string.
      invcs typ.
      unfold equiv_decb in *.
      destruct (v == vv); [rewrite e; apply remove_In | ].
      match_case_in neq; intros eqq1; rewrite eqq1 in neq; try congruence.
      + apply nnrs_stmt_to_nnrs_imp_stmt_assigned_must_assign in eqq1.
         apply nnrs_stmt_must_assign_is_free in eqq1.
         intuition.
      + rewrite <- remove_in_neq by eauto.
         rewrite in_app_iff.
         intros [inn|inn].
         * eapply IHs1; eauto; intuition; try congruence.
         * revert inn. eapply IHs2; eauto.
    - Case "NNRSAssign"%string.
      match_case_in neq; intros eqq; rewrite eqq in neq; try congruence.
      unfold equiv_decb in *.
      destruct (v == vv); [intuition | ].
      apply nnrs_imp_expr_may_use_free_vars_neg in eqq.
      intuition.
    - Case "NNRSPush"%string.
      unfold equiv_decb in *.
      destruct (vv == v); simpl in neq; try congruence.
      match_case_in neq; intros eqq; rewrite eqq in neq; try congruence.
      apply nnrs_imp_expr_may_use_free_vars_neg in eqq.
      intuition.
    - Case "NNRSFor"%string.
      match_case_in neq; intros eqq1; rewrite eqq1 in neq; try congruence.
      apply nnrs_imp_expr_may_use_free_vars_neg in eqq1.
      intros [inn|inn]; auto.
      apply remove_inv in inn.
      destruct inn as [inn ?].
      unfold equiv_decb in *.
      destruct (v == vv); try congruence.
      revert inn.
      invcs typ.
      eapply IHs; eauto.
      intros e; rewrite e in neq; congruence.
    - Case "NNRSIf"%string.
      match_case_in neq; intros eqq1; rewrite eqq1 in neq; try congruence.
      apply nnrs_imp_expr_may_use_free_vars_neg in eqq1.
      invcs typ.
      intros [inn|inn]; auto; revert inn.
      match_case_in neq; intros eqq2; rewrite eqq2 in neq; try congruence
      ; match_case_in neq; intros eqq3; rewrite eqq3 in neq; try congruence
      ; (intros [inn|inn]; revert inn
        ; [eapply IHs1|eapply IHs2]; eauto; congruence).
    - Case "NNRSEither"%string.
      match_case_in neq; intros eqq1; rewrite eqq1 in neq; try congruence.
      apply nnrs_imp_expr_may_use_free_vars_neg in eqq1.
      invcs typ.
      intros [inn|inn]; auto; revert inn.
      destruct (v == vv)
      ; destruct (v0 == vv)
      ; unfold equiv, complement in *
      ; subst.
      + intros [inn|inn]
        ; apply remove_inv in inn; intuition congruence.
      + intros [inn|inn].
        * apply remove_inv in inn; intuition congruence.
        * revert inn.
          match_case_in neq; intros eqq2; rewrite eqq2 in neq; try congruence
          ; rewrite <- remove_in_neq by eauto
          ; eapply IHs2; eauto; congruence.
      + intros [inn|inn].
        * revert inn.
          match_case_in neq; intros eqq2; rewrite eqq2 in neq; try congruence
          ; rewrite <- remove_in_neq by eauto
          ; eapply IHs1; eauto; congruence.
        * apply remove_inv in inn; intuition congruence.
      + intros [inn|inn].
        * revert inn.
          match_case_in neq; intros eqq2; rewrite eqq2 in neq; try congruence
          ; rewrite <- remove_in_neq by eauto
          ; eapply IHs1; eauto; congruence.
        * revert inn.
          match_case_in neq; intros eqq2; rewrite eqq2 in neq; try congruence
          ; rewrite <- remove_in_neq by eauto
          ; match_case_in neq; intros eqq3; rewrite eqq3 in neq; try congruence
          ; try rewrite <- remove_in_neq by eauto
          ; eapply IHs2; eauto; congruence.
  Qed.

  Lemma nnrs_stmt_to_nnrs_imp_preserves_free_env {s  dΓ dΔc dΔd} :
    nnrs_stmt_cross_shadow_free_under s dΓ dΔc dΔd ->
    forall v,
    In v (nnrs_stmt_free_env_vars s) \/  In v (nnrs_stmt_free_mcenv_vars s) \/  In v (nnrs_stmt_free_mdenv_vars s) ->
    In v (nnrs_imp_stmt_free_vars (nnrs_stmt_to_nnrs_imp_stmt s)).
  Proof.
    Ltac  pfe_tac
      := repeat match goal with
               | [ H: In _ (remove _ _ _) |- _ ] => apply remove_inv in H; destruct H
               | [|- context [In _ (remove _ _ _) ]] => rewrite <- remove_in_neq by
                     (eauto
                      ; repeat match goal with
                                 [H:  nnrs_stmt_cross_shadow_free_under _ _ _ _ |- _ ] =>
                                 apply nnrs_stmt_cross_shadow_free_under_free_cons in H
                                 ; destruct H; congruence
                               end)
             end; intuition eauto.
    revert dΓ dΔc dΔd.
    nnrs_stmt_cases (induction s) Case
    ; simpl
    ; repeat rewrite in_app_iff in *
    ; intros  dΓ dΔc dΔd sf vv inn
    ; repeat progress (
               repeat rewrite in_app_iff in *
               ; repeat rewrite nnrs_expr_to_nnrs_imp_expr_free_vars
               ; intuition
               ; pfe_tac
             ).
    - Case "NNRSEither"%string.
      right; right.
      pfe_tac.
    - Case "NNRSEither"%string.
      right; right.
      pfe_tac.
    - Case "NNRSEither"%string.
      right; right.
      pfe_tac.
  Qed.

  Lemma nnrs_stmt_to_nnrs_imp_preserves_nfree_env {s  dΓ dΔc dΔd} :
    nnrs_stmt_cross_shadow_free_under s dΓ dΔc dΔd ->
    forall v,
      ~ In v (nnrs_imp_stmt_free_vars (nnrs_stmt_to_nnrs_imp_stmt s)) ->
          ~ In v (nnrs_stmt_free_env_vars s)
          /\  ~ In v (nnrs_stmt_free_mcenv_vars s)
          /\ ~ In v (nnrs_stmt_free_mdenv_vars s).
  Proof.
    intros sf v nin.
    generalize (nnrs_stmt_to_nnrs_imp_preserves_free_env sf); intros HH.
    repeat split; intros inn; apply nin; eauto.
  Qed.

  Lemma tnnrs_stmt_to_nnrs_imp_correct_b
        (Γc:tbindings) (Γ:TNNRS.pd_tbindings)
        (Δc:TNNRS.mc_tbindings) (Δd:TNNRS.md_tbindings) s :
    [ Γc ; concat_tenvs Γ Δc Δd ⊢  nnrs_stmt_to_nnrs_imp_stmt s ]%nnrs_imp ->
    nnrs_stmt_cross_shadow_free_under s (domain Γ) (domain Δc) (domain Δd) ->
    (forall x : var, In x (nnrs_stmt_free_env_vars s) -> lookup equiv_dec Γ x <> Some None) ->
    [ Γc ; Γ , Δc , Δd ⊢ s ]%nnrs.
  Proof.

    Ltac prove_expr_b_t notnone
      := match goal with
        | [H: [ _ ; _ ⊢ nnrs_expr_to_nnrs_imp_expr ?e ▷ _ ] %nnrs_imp |-
           [ _ ; _ ⊢ ?e ▷ _ ]%nnrs ] =>
        apply tnnrs_expr_to_nnrs_expr_correct_b
        ; [ eauto; try (intros; apply notnone; rewrite in_app_iff; tauto)
          | apply (nnrs_imp_expr_type_lookup_equiv_on H)
            ; rewrite nnrs_expr_to_nnrs_imp_expr_free_vars
            ; unfold lookup_equiv_on; intros ? inn
            ; unfold concat_tenvs; repeat rewrite lookup_app
            ; match_destr
            ; repeat rewrite lookup_nin_none; trivial
            ; try rewrite domain_map_codomain; trivial
            ; match goal with
              | [H1:disjoint ?l1 ?l2,
                      H2: In ?x ?l1 |- ~ In ?x ?l2 ] =>
                exact (H1 x inn)
              end]
        end.

    Hint Constructors nnrs_stmt_type : qcert.
    revert Γ Δc Δd.
    nnrs_stmt_cases (induction s) Case
    ; simpl
    ; intros Γ Δc Δd typ sf notnone
    ; invcs typ.
    - Case "NNRSSeq"%string.
      destruct sf as [sf1 sf2].
      econstructor.
      + eapply IHs1; eauto; intros
        ; apply notnone; rewrite in_app_iff; tauto.
      + eapply IHs2; eauto; intros
        ; apply notnone; rewrite in_app_iff; tauto.
    - Case "NNRSLet"%string.
      destruct sf as [disj1 [disj2 [nin1 [nin2 sf]]]].
      econstructor.
      + prove_expr_b_t notnone.
      + eapply IHs; eauto; intros; simpl.
        match_destr.
        apply notnone; rewrite in_app_iff.
        right.
        apply remove_in_neq; auto.
    - Case "NNRSLetMut"%string.
      destruct sf as [ninΓ [ninΔc [ninΔd [sf1 sf2]]]].
      invcs H3.
      simpl in H2.
      match_case_in H2; intros eqq; rewrite eqq in H2; try congruence.
      + { econstructor.
          + eapply nnrs_stmt_to_nnrs_imp_stmt_assigned_must_assign; eauto.
          + eapply IHs1; eauto.
            * eapply nnrs_imp_stmt_type_lookup_equiv_prop; try eapply H4; trivial.
              rewrite concat_tenvs_cons_some.
              rewrite <- concat_tenvs_lookup_equiv_env_md
              ; try reflexivity; eauto.
            * intros; apply notnone; rewrite in_app_iff; tauto.
          + simpl. eapply IHs2; eauto.
            intros; simpl.
            match_destr.
            apply notnone; rewrite in_app_iff.
            right.
            apply remove_in_neq; auto.
        }
      + { eapply type_NNRSLetMutNotUsed.
          + eapply IHs1; eauto.
            *  eapply nnrs_imp_stmt_type_lookup_equiv_prop; try eapply H4; trivial.
              rewrite concat_tenvs_cons_some.
              rewrite <- concat_tenvs_lookup_equiv_env_md; eauto.
              reflexivity.
            * intros; apply notnone; rewrite in_app_iff; tauto.
          + assert (nin:~ In v (nnrs_stmt_free_mdenv_vars s2)).
            {
              apply nnrs_stmt_cross_shadow_free_under_free_mdenv_env in sf2.
              eapply disjoint_cons_inv2; eauto.
            }
            rewrite concat_tenvs_cons_some in H5.
            specialize (IHs2 _ _ _ H5 sf2).
            cut_to IHs2
            ; [ |
              simpl; intros
              ; match_destr
              ; apply notnone; rewrite in_app_iff
              ; right; apply remove_in_neq; eauto].
            assert (nin2:~ In v (nnrs_imp_stmt_free_vars (nnrs_stmt_to_nnrs_imp_stmt s2))) by (eapply nnrs_stmt_to_nnrs_imp_free_md_free; eauto).
            apply (nnrs_stmt_to_nnrs_imp_preserves_nfree_env sf2) in nin2.
            destruct nin2 as [nin1 [nin2 nin3]].
            eapply (nnrs_stmt_type_unused_add_env Γc nil); simpl
            ; try tauto.
            eapply (nnrs_stmt_type_unused_remove_env Γc nil); simpl
            ; eauto.
        }
    - Case "NNRSLetMutColl"%string.
      destruct sf as [ninΓ [ninΔc [ninΔd [sf1 sf2]]]].
      invcs H4.
      invcs H2.
      invcs H4.
      rewrite concat_tenvs_cons_some in H3.
      rewrite concat_tenvs_cons_some in H5.
      econstructor.
      + eapply IHs1; eauto.
        * eapply nnrs_imp_stmt_type_lookup_equiv_prop; eauto.
          rewrite <- concat_tenvs_lookup_equiv_env_mc_cons
          ; trivial.
          reflexivity.
        * intros; apply notnone; rewrite in_app_iff; tauto.
      + eapply IHs2; eauto.
         simpl; intros
              ; match_destr
              ; apply notnone; rewrite in_app_iff
              ; right; apply remove_in_neq; eauto.
    - Case "NNRSAssign"%string.
      destruct sf as [disjc [disjd [ninΓ ninΔc]]].
      econstructor; eauto.
      + prove_expr_b_t notnone.
      + unfold concat_tenvs in H3; repeat rewrite lookup_app in H3.
        do 2 (rewrite lookup_nin_none in H3; trivial
        ; unfold pd_tbindings_lift
        ; try rewrite domain_map_codomain; trivial).
    - Case "NNRSPush"%string.
      destruct sf as [disjc [disjd [ninΓ ninΔc]]].
      invcs H2.
      invcs H5.
      invcs H7.
      invcs H8.
      invcs H4.
      rtype_equalizer; subst.
      unfold equiv_dec, string_eqdec in *.
      rewrite H1 in H3.
      invcs H3.
      econstructor.
      + prove_expr_b_t notnone.
      + unfold concat_tenvs in H1; repeat rewrite lookup_app in H1.
        rewrite lookup_map_codomain in H1.
        rewrite lookup_nin_none in H1; trivial
        ; unfold pd_tbindings_lift
        ; try rewrite domain_map_codomain; trivial.
        destruct (lookup string_dec Δc v); simpl in *.
        * invcs H1; rtype_equalizer; congruence.
        * rewrite lookup_nin_none in H1; trivial
        ; unfold pd_tbindings_lift
        ; try rewrite domain_map_codomain; trivial.
          discriminate.
    - Case "NNRSFor"%string.
      destruct sf as [disjc [disjd [ninΔc [ninΔd sf]]]].
      econstructor.
      + prove_expr_b_t notnone.
      + eapply IHs; eauto; intros; simpl.
        match_destr.
        apply notnone; rewrite in_app_iff.
        right.
        apply remove_in_neq; auto.
    - Case "NNRSIf"%string.
      destruct sf as [disjc [disjd [sf1 sf2]]].
      econstructor.
      + prove_expr_b_t notnone.
      + eapply IHs1; eauto.
        intros; apply notnone; rewrite in_app_iff; intuition.
      + eapply IHs2; eauto.
        intros; apply notnone; rewrite in_app_iff; intuition.
    - Case "NNRSEither"%string.
      destruct sf as [disjc [disjd [nin1Δc [nin1Δd [nin2Δc [nin2Δd [sf1 sf2]]]]]]].
      econstructor.
      + prove_expr_b_t notnone.
      + eapply IHs1; eauto; intros; simpl.
        match_destr.
        apply notnone; repeat rewrite in_app_iff.
        right; left.
        apply remove_in_neq; auto.
      + eapply IHs2; eauto; intros; simpl.
        match_destr.
        apply notnone; repeat rewrite in_app_iff.
        right; right.
        apply remove_in_neq; auto.
  Qed.

  Theorem tnnrs_to_nnrs_imp_correct_b {Γc} {si:nnrs} {τ} :
    [ Γc ⊢ nnrs_to_nnrs_imp si ▷ τ ]%nnrs_imp ->
    nnrs_cross_shadow_free si ->
    [ Γc ⊢ si ▷ τ ]%nnrs.
  Proof.
    destruct si; simpl.
    intros [neq typ] sf.
    apply (tnnrs_stmt_to_nnrs_imp_correct_b Γc nil nil ((v, τ)::nil))
    ; unfold concat_tenvs; simpl; intuition congruence.
  Qed.

  Theorem tnnrs_to_nnrs_imp_top_correct_b {Γc} {si:nnrs} {τ} {sep}:
    [ Γc ⊢ nnrs_to_nnrs_imp_top sep si ▷ τ ]%nnrs_imp ->
    [ Γc ⊢ si ▷ τ ]%nnrs.
  Proof.
    unfold nnrs_to_nnrs_imp_top.
    intros typ.
    apply tnnrs_to_nnrs_imp_correct_b in typ.
    - eapply nnrs_uncross_shadow_type; eauto.
    - apply nnrs_uncross_shadow_free.
  Qed.

  Theorem tnnrs_to_nnrs_imp_top_correct Γc (si:nnrs) τ sep:
    [ Γc ⊢ si ▷ τ ]%nnrs <->
    [ Γc ⊢ nnrs_to_nnrs_imp_top sep si ▷ τ ]%nnrs_imp.
  Proof.
    split; intros.
    - eapply tnnrs_to_nnrs_imp_top_correct_f; eauto.
    - eapply tnnrs_to_nnrs_imp_top_correct_b; eauto.
  Qed.

  Section core.

    Program Lemma tnnrs_core_to_nnrs_imp_core_top_correct_f {Γc} {si:nnrs_core} {τ} :
      [ Γc ⊢ si ▷ τ ]%nnrs ->
      forall sep,
        [ Γc ⊢ nnrs_core_to_nnrs_imp_core_top sep si ▷ τ ]%nnrs_imp.
    Proof.
      intros typ sep.
      apply tnnrs_to_nnrs_imp_top_correct_f; trivial.
    Qed.

    Program Lemma tnnrs_core_to_nnrs_imp_core_top_correct_b {Γc} {si:nnrs_core} {τ} {sep} :
      [ Γc ⊢ nnrs_core_to_nnrs_imp_core_top sep si ▷ τ ]%nnrs_imp ->
      [ Γc ⊢ si ▷ τ ]%nnrs.
    Proof.
      intros typ.
      apply tnnrs_to_nnrs_imp_top_correct_b in typ; eauto.
    Qed.

    Program Theorem tnnrs_core_to_nnrs_imp_core_top_correct Γc (si:nnrs_core) τ sep :
      [ Γc ⊢ si ▷ τ ]%nnrs <->
        [ Γc ⊢ nnrs_core_to_nnrs_imp_core_top sep si ▷ τ ]%nnrs_imp.
    Proof.
      split; intros.
      - eapply tnnrs_core_to_nnrs_imp_core_top_correct_f; eauto.
      - eapply tnnrs_core_to_nnrs_imp_core_top_correct_b; eauto.
    Qed.

  End core.

End TNNRStoNNRSimp.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable wd_ : Universe -> Universe -> Prop.
Variable col_ : Universe -> Universe -> Universe -> Prop.

Variable col_swap1_1 : (forall A B C : Universe, (col_ A B C -> col_ B A C)).
Variable col_swap2_2 : (forall A B C : Universe, (col_ A B C -> col_ B C A)).
Variable col_triv_3 : (forall A B : Universe, col_ A B B).
Variable wd_swap_4 : (forall A B : Universe, (wd_ A B -> wd_ B A)).
Variable col_trans_5 : (forall P Q A B C : Universe, ((wd_ P Q /\ (col_ P Q A /\ (col_ P Q B /\ col_ P Q C))) -> col_ A B C)).

Theorem pipo_6 : (forall H O Hprime Oprime Lprime SH SHprime : Universe, ((wd_ H O /\ (wd_ O SH /\ (wd_ H SH /\ (wd_ Hprime Oprime /\ (wd_ Oprime SHprime /\ (wd_ Hprime SHprime /\ (col_ H O SH /\ (col_ Hprime Oprime SHprime /\ col_ SHprime Oprime Lprime)))))))) -> col_ Hprime Oprime Lprime)).
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus


text:
From cap_machine Require Export logrel.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import weakestpre adequacy lifting.
From stdpp Require Import base.
From cap_machine Require Import ftlr_base monotone.
From cap_machine.rules Require Import rules_base rules_Mov.

Section fundamental.
  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
          {stsg : STSG Addr region_type Σ} {heapg : heapG Σ}
          {nainv: logrel_na_invs Σ}
          `{MachineParameters}.

  Notation STS := (leibnizO (STS_states * STS_rels)).
  Notation STS_STD := (leibnizO (STS_std_states Addr region_type)).
  Notation WORLD := (prodO STS_STD STS).
  Implicit Types W : WORLD.

  Notation D := (WORLD -n> (leibnizO Word) -n> iPropO Σ).
  Notation R := (WORLD -n> (leibnizO Reg) -n> iPropO Σ).
  Implicit Types w : (leibnizO Word).
  Implicit Types interp : (D).

  Lemma mov_case (W : WORLD) (r : leibnizO Reg) (p : Perm)
        (g : Locality) (b e a : Addr) (w : Word) (ρ : region_type) (dst : RegName) (src : Z + RegName) (P:D):
    ftlr_instr W r p g b e a w (Mov dst src) ρ P.
  Proof.
    intros Hp Hsome i Hbae Hpers Hpwl Hregion Hnotrevoked Hnotmonostatic Hnotuninitialized Hi.
    iIntros "#IH #Hinv #Hreg #Hinva #Hrcond #Hwcond Hmono Hw Hsts Hown".
    iIntros "Hr Hstate Ha HPC Hmap".
    rewrite delete_insert_delete.
    iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /=";
      [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl.
    iApply (wp_Mov with "[$Ha $Hmap]"); eauto.
    { simplify_map_eq; auto. }
    { rewrite /subseteq /map_subseteq /set_subseteq. intros rr _.
      apply elem_of_gmap_dom. apply lookup_insert_is_Some'; eauto. }

    iIntros "!>" (regs' retv). iDestruct 1 as (HSpec) "[Ha Hmap]".
    destruct HSpec; cycle 1.
    { iApply wp_pure_step_later; auto. iNext.
      iApply wp_value; auto. iIntros; discriminate. }
    { (* TODO: it might be possible to refactor the proof below by using more simplify_map_eq *)
      (* TODO: use incrementPC_inv *)
      match goal with
      | H: incrementPC _ = Some _ |- _ => apply incrementPC_Some_inv in H as (p''&g''&b''&e''&a''& ? & HPC & Z & Hregs' & XX)
      end. simplify_map_eq.
      iApply wp_pure_step_later; auto. iNext.
      destruct (reg_eq_dec dst PC).
      { subst dst. rewrite lookup_insert in HPC. inv HPC.
        repeat rewrite insert_insert.
        destruct src; simpl in *; try discriminate.
        iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto.
        { destruct ρ;auto;[|specialize (Hnotmonostatic g0)|specialize (Hnotuninitialized w0)];contradiction. }
        destruct (reg_eq_dec PC r0).
        { subst r0. simplify_map_eq.
          iApply ("IH" $! _ r with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); try iClear "IH"; eauto. }
        { simplify_map_eq.
          rewrite /RegLocate. iDestruct ("Hreg" $! r0 ltac:(auto)) as "Hr0". rewrite H0.
          destruct (PermFlowsTo RX p'') eqn:Hpft.
          - iApply ("IH" $! _ r with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); try iClear "IH"; eauto.
            + destruct p''; simpl in Hpft; auto.
              repeat rewrite fixpoint_interp1_eq. simpl.
              destruct g''; auto.
            + iModIntro. rewrite /region_conditions.
              destruct p''; simpl in Hpft; try discriminate; repeat (rewrite fixpoint_interp1_eq); simpl; auto.
              iApply (big_sepL_mono with "Hr0").
              intros. iIntros "H". iDestruct "H" as (P') "(?&?&?)".
              iApply bi.and_exist_r. iExists _. iFrame.
              destruct g''; auto.
          - iApply (wp_bind (fill [SeqCtx])).
            iDestruct ((big_sepM_delete _ _ PC) with "Hmap") as "[HPC Hmap]"; [apply lookup_insert|].
            iApply (wp_notCorrectPC with "HPC"); [eapply not_isCorrectPC_perm; destruct p''; simpl in Hpft; try discriminate; eauto|].
            iNext. iIntros "HPC /=".
            iApply wp_pure_step_later; auto.
            iApply wp_value.
            iNext. iIntros. discriminate. } }
      { rewrite lookup_insert_ne in HPC; auto.
        rewrite lookup_insert in HPC. inv HPC.
        iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto.
        { destruct ρ;auto;[|specialize (Hnotmonostatic g)|specialize (Hnotuninitialized w1)];contradiction. }
        iApply ("IH" $! _ (<[dst:=w0]> _) with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); eauto.
        - intros; simpl.
          rewrite lookup_insert_is_Some.
          destruct (reg_eq_dec dst x0); auto; right; split; auto.
          rewrite lookup_insert_is_Some.
          destruct (reg_eq_dec PC x0); auto; right; split; auto.
        - iIntros (ri Hri).
          destruct (reg_eq_dec ri dst).
          + subst ri. rewrite /RegLocate lookup_insert.
            destruct src; simplify_map_eq.
            * repeat rewrite fixpoint_interp1_eq; auto.
            * destruct (reg_eq_dec PC r0).
              { subst r0.
                - simplify_map_eq.
                  rewrite (fixpoint_interp1_eq _ (inr (_, g'', b'', e'', a''))) /=.
                destruct Hp as [Hp | [Hp | [Hp Hg] ] ]; subst p''; try subst g'';
                  try (iFrame "Hexec"); try (iFrame "Hinv").
                iApply (big_sepL_mono with "Hinv").
                intros. iIntros "(H & ?)".
                simpl. iDestruct "H" as (P') "(?&?&?)".
                iExists _. iFrame.
              }
              simplify_map_eq.
              iDestruct ("Hreg" $! r0 ltac:(auto)) as "Hr0". rewrite H0. auto.
          + repeat rewrite /RegLocate lookup_insert_ne; auto.
            iApply "Hreg"; auto.
      }
    }
    Unshelve. all: auto.
  Qed.

End fundamental.

author: logsem

repo: cerise-stack-monotone


text:
From ITree Require Import ITree.
From compcert Require Coqlib.
From Paco Require Import paco.

Require Import sflib.
Require Import Axioms StdlibExt IntegersExt.

Require Import SysSem.
Require Import IPModel DiscreteTimeModel.
Require Import RTSysEnv.
Require Import SyncSysModel.

Require Import List.
Require Import Arith ZArith Lia.

Module SyncSysNB.
  Section SYS.
    Context {sysE: Type -> Type}.
    Context {msgT: Set}.
    Variable is_nb_step: list (@SNode.state sysE msgT) -> list (@SNode.state sysE msgT) -> bool.

    Record t: Type :=
      mk { period: nat ;
           nodes: list (@SNode.t sysE msgT) ;
           mcasts: list (list Tid) ;

           sanitize_msg: msgT -> msgT? ;
         }.

    Inductive wf: t -> Prop :=
      Wf prd nds mcs sntz (* imcasts *)
         (PERIOD_POS: 0 < prd)
      : wf (mk prd nds mcs sntz).

    Record state: Type :=
      State { time: nat ;
              node_states: list (@SNode.state sysE msgT) ;
            }.

    Inductive state_wf (num_tasks: nat)
      : state -> Prop :=
      StateWf
        tm nsts
        (WF_NSTS: iForall (SNode.state_wf num_tasks) 0 nsts)
        (NUM_TASKS: length nsts = num_tasks)
      : state_wf num_tasks (State tm nsts).

    Definition init_state (tm_init: nat) (sys: t): state :=
      let nds := nodes sys in
      let nsts := imap (SNode.init_state (length nds)) 0 nds in
      State tm_init nsts.

    Lemma wf_init_state
          tm sys
          (* (WF_SYS: wf sys) *)
      : state_wf (length (nodes sys))
                 (init_state tm sys).
    Proof.
      econs; eauto.
      2: { rewrite imap_length. ss. }
      (* inv WF_SYS. ss. *)
      destruct sys as [period nodes mcasts]. ss.
      apply iForall_nth. ss.
      i. rewrite imap_nth_error_iff.
      destruct (nth_error nodes n); ss.
      econs. rewrite repeat_length; ss.
    Qed.

    Inductive step
              (mcasts: list (list Tid)) (period: nat)
              (sntz: msgT -> msgT?)
      : state -> list (tsp * events (nbE +' sysE)) ->
        state -> Prop :=
    | Step_Wait
        tm nsts tes
        (WAIT: ~ Nat.divide period tm)
        (EMPTY_EVTS: tes = List.repeat (Z.of_nat tm, []) (length nsts))
      : step mcasts period sntz
             (State tm nsts) tes (State (S tm) nsts)

    | Step_Run
        tm nsts ess tes outs nsts1 nsts'
        (WAIT: Nat.divide period tm)
        (STEPS: Forall4 (SNode.step sntz (length nsts) mcasts tm) nsts ess outs nsts1)
        (ACCEPT_MSGS: List.map (SNode.accept_msgs outs) nsts1 = nsts')
        (ATTACH_TIMESTAMP:
           tes = if is_nb_step nsts nsts'
                 then map (fun es => (Z.of_nat tm, [embed (Event NobehEvent tt)])) ess
                 else map (fun es => (Z.of_nat tm, es)) ess)
      : step mcasts period sntz
             (State tm nsts) tes (State (S tm) nsts')
    .

    Lemma wf_prsv
          nt mcs sntz prd
          st es st'
          (STEP: step mcs prd sntz
                      st es st')
          (WF_STATE: state_wf nt st)
      : state_wf nt st'.
    Proof.
      inv WF_STATE. inv STEP.
      - econs; eauto.
      - econs; eauto.
        2: { rewrite map_length.
             hexploit Forall4_length; eauto.
             i. des. eauto. }
        apply iForall_nth. i.
        rewrite iForall_nth in WF_NSTS.
        specialize (WF_NSTS n). ss.

        rewrite Coqlib.list_map_nth.
        destruct (nth_error nsts n) as [nst_n|] eqn: NST_N.
        2: {
          rewrite nth_error_None2.
          { econs. }
          apply Forall4_length in STEPS.
          des.
          rewrite <- LEN14.
          apply nth_error_None. ss.
        }

        hexploit Forall4_nth1; eauto. i. des.
        rewrite NTH4. ss.
        eapply SNode.wf_accept_msgs_prsv; eauto.
        { hexploit Forall4_length; eauto. i. des. ss. }
        eapply SNode.wf_prsv; eauto.
    Qed.

    Lemma wf_progress
          mcs prd sntz
          nt st
          (WF_STATE: state_wf nt st)
      : exists es st',
        step mcs prd sntz st es st'.
    Proof.
      destruct st as [tm nsts].

      destruct (Nat_divide_dec prd tm).
      2: { esplits. econs 1; eauto. }

      assert (exists l2 l3 l4,
                 Forall4 (SNode.step sntz (length nsts) mcs tm)
                         nsts l2 l3 l4).
      { eapply Forall4_exists_list.
        i. apply SNode.step_progress. }
      des. esplits. econs 2; eauto.
    Qed.

    Definition num_sites (st: state): nat :=
      length st.(node_states).

    Program Definition as_dsys (sys: t) (tm_init: nat): DSys.t :=
      DSys.mk state num_sites
              (step (mcasts sys) (period sys) (sanitize_msg sys))
              (fun st => st = init_state tm_init sys) _.
    Next Obligation.
      splits.
      - unfold num_sites.
        inv STEP; ss.
        + rewrite repeat_length. ss.
        + hexploit Forall4_length; eauto. i. des.
          des_ifs; rewrite map_length; ss.
      - unfold num_sites.
        inv STEP; ss.
        rewrite map_length.
        hexploit Forall4_length; eauto. i. des. ss.
    Qed.

    Lemma safe
          tm
          (sys: t)
          (WF: wf sys)
      : DSys.safe (as_dsys sys tm).
    Proof.
      econs.
      { esplits; ss. }
      i.
      pose (num_tasks := length (nodes sys)).

      assert (WF_STATE: state_wf num_tasks st_i).
      { subst num_tasks.
        inv INIT.
        apply wf_init_state. }
      rename st_i into st.
      clear INIT.
      depgen st.

      pcofix CIH. i.
      pfold. econs.
      { eapply wf_progress. eauto. }
      i. right. ss.
      hexploit wf_prsv; eauto.
    Qed.

  End SYS.
End SyncSysNB.

author: kim-yoonseung

repo: pals-thesis-dev


text:
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(** * Subtyping *)

(** A subtype extends another type by adding
    a property. The new type has a richer theory.
    The new type should inherit all the original
    theory. *)

(* Let's define the type of homogeneous tuples *)

(** ** Standard [sig] type *)

Print sig.
(**
  Inductive sig (A : Type) (P : A -> Prop) : Type :=
    | exist : forall x:A, P x -> sig P.

  Notation "{ x : A  |  P }" :=
    (sig (A:=A) (fun x => P)) : type_scope.
*)

(** [sig] type is almost the same as the [ex] type encoding
    existential quantifier *)
Print ex.
(**
  Inductive ex (A : Type) (P : A -> Prop) : Prop :=
    | ex_intro : forall x:A, P x -> ex P.
 *)

(** simple definition relying on the existing [pred] function *)
Definition predecessor (x : {n | 0 < n}) : nat :=
  let: (exist m prf_m_gt_0) := x in
  m.-1.

About False_rect.
Check notF.

Lemma not_false_is_true' : not false.
Proof.
  Unset Printing Notations.
  rewrite /is_true.
  move=> x.
  by case: x.
  Set Printing Notations.
Qed.

Variable x : 0 < 0.
Check (False_rect _ (notF x)) : nat.

(** The _convoy pattern_ : *)
Definition pred_dep (x : {n | 0 < n}) : nat :=
  let: (exist n prf_n_gt_0) := x in
  match n as n return (0 < n -> nat) with
  | 0 =>
      fun prf : 0 < 0 => False_rect _ (notF prf)
  | n'.+1 =>
      fun _ => n'
  end prf_n_gt_0.

(** ** Some issues *)

(** Proof irrelevance *)

Lemma eq_sig T (P : T -> Prop) x (px : P x) (px' : P x) :
  (exist P x px) = (exist P x px').
Proof.
Fail by done.
(** we are stuck: we need proof irrelevance here *)
Abort.

Axiom proof_irrelevance :
  forall (P : Prop) (pf1 pf2 : P), pf1 = pf2.

Lemma eq_sig T (P : T -> Prop) x (px : P x) (px' : P x) :
  (exist P x px) = (exist P x px').
Proof.
rewrite [px]proof_irrelevance.
done.
Qed.

(** Decidable propositions _are_ proof irrelevant *)

Check eq_irrelevance.
(**
eq_irrelevance
     : forall (T : eqType) (x y : T)
         (e1 e2 : x = y),
         e1 = e2

This special case of proof irrelevance is called
_Unicity of Identity Proofs_ principle (UIP).
*)

(** [sval] projection is injective for decidable propositions : *)
Lemma eq_n_gt0 (m n : {n | 0 < n}) :
  sval m = sval n ->
  m = n.
Proof.
case: m=> [m pfm]; case: n=> [n pfn] /=.
Fail move=> ->.  (* because of the dependencies *)
move=> eq_mn; move: eq_mn pfm pfn.
move=> -> *.
congr exist.
exact: eq_irrelevance.
Qed.

(** We cannot define [proj1_sig] as a coercion *)

(**
This is because we cannot specify the target
class of this tentative coercion:
  Coercion proj1_sig : sig >-> ???.
 *)

(** ** Mathcomp's [subType]
       (defined in [eqtype] library) *)

Print subType.
(**
  Structure subType (T : Type) (P : pred T) : Type :=
    SubType {
      (* new type *)
      sub_sort : Type;

      (* projection, like proj_sig1 *)
      val : sub_sort -> T;

      (* constructor *)
      Sub : forall x : T, P x -> sub_sort;

      (* elimination principle *)
      _ : forall K : sub_sort -> Type,
          (forall (x : T) (Px : P x), K (Sub x Px)) ->
          forall u : sub_sort, K u;

      (* projection is injective *)
      _ : forall (x : T) (Px : P x),
          val (Sub x Px) = x
    }.
*)

(** An example of a [subType] *)
Section PosSubtype.

Inductive pos := Positive m of 0 < m.

Coercion nat_of_pos p :=
  let: Positive n _ := p in n.

Variables p1 p2 : pos.

(** This is something not possible with
    {n | 0 < n} type *)
Check p1.-1 + p2.
Set Printing Coercions.
Check p1.-1 + p2.
Unset Printing Coercions.

(** Register [pos] as a [subType] *)
Canonical pos_subType :=
  [subType for nat_of_pos].

(** Given that propositions are expressed as
    booleans, we can use the fact that proofs of
    these properties are irrelevant. *)

(** Hence we can build subtypes and prove that
    the projection to the supertype is injective,
    which lets us inherit all of the theory of
    the supertype. *)

(** E.g. we can make [pos] inherit [eqType]
    from [nat] type with a bit of boilerplate *)

Definition pos_eqMixin :=
  Eval hnf in [eqMixin of pos by <:].

Canonical pos_eqType :=
  Eval hnf in EqType pos pos_eqMixin.

Check p1 == p2.

End PosSubtype.

(** * Some standard [subType]s *)

(** ** [ordinal]: type of finite ordinals *)

(**
[ordinal n] = {0, 1, ... , n-1}

Inductive ordinal : predArgType :=
  | Ordinal m of m < n.

Notation "''I_' n" := (ordinal n)

 *)

From mathcomp Require Import fintype.

Definition i1 : 'I_2 :=
  Ordinal (erefl : 0 < 2).

Definition i2 : 'I_2 :=
  Ordinal (erefl : 1 < 2).

Compute i1 == i2.

(** Note: [ordinal] is also a [finType] *)

(** ** [tuple] type *)

From mathcomp Require Import tuple.

Definition t : 3.-tuple nat :=
  [tuple 5; 6; 7].

(** It's not possible to take an out-of-bounds
    element of a tuple, so there is no need
    of a default element as for [nth] on [seq]s *)
About tnth.

Compute [tnth t 0].
Compute [tnth t 1].
Compute [tnth t 2].
Fail Compute [tnth t 3].

About thead.
(**
thead :
  forall (n : nat) (T : Type),
    (n.+1).-tuple T -> T
*)

Compute thead t.  (** = 5 *)
(** [thead] of empty tuple
    does not even typecheck *)
Fail Check thead [tuple].

(**
  Structure tuple_of (n : nat) (T : Type) : Type :=
    Tuple {
    (* [:>] means "is a coercion" *)
      tval :> seq T;
      _ : size tval == n;
    }.
*)

Section TupleExample.
Variables (m n : nat) (T : Type).
Variable t1 : m.-tuple T.
Variable t2 : n.-tuple T.

Check [tuple of t1 ++ t2] : (m + n).-tuple T.
Fail Check [tuple of t1 ++ t2] : (n + m).-tuple T.
End TupleExample.

Example seq_on_tuple (n : nat) (t : n .-tuple nat) :
  size (rev [seq 2 * x | x <- rev t]) = size t.
Proof.

Set Printing Coercions.
by rewrite map_rev revK size_map.
Unset Printing Coercions.

Restart.

rewrite size_tuple.  (** this should work *)
Check size_tuple.
(**
  size_tuple : forall (n : nat) (T : Type)
               (t : n.-tuple T), size t = n
*)

(** Why does this not fail? *)
(** rev [seq 2 * x | x <- rev t] is a list,
    not a tuple *)
rewrite size_tuple.
Abort.

Print Canonical Projections.
(**
  ...
  map <- tval ( map_tuple )
  ...
  rev <- tval ( rev_tuple )
  ...
*)

(**
This works because Coq is instrumented
to automatically promote sequences to tuples
using the mechanism of Canonical Structures.

Lemma rev_tupleP n A (t : n .-tuple A) :
  size (rev t) == n.
Proof. by rewrite size_rev size_tuple. Qed.

Canonical rev_tuple n A (t : n .-tuple A) :=
  Tuple (rev_tupleP t).

Lemma map_tupleP n A B (f:A -> B) (t: n.-tuple A) :
   size (map f t) == n.
Proof. by rewrite size_map size_tuple. Qed.

Canonical
  map_tuple n A B (f:A -> B) (t: n.-tuple A) :=
    Tuple (map_tupleP f t).
 *)

(** Exercise: show in detail how
    [rewrite size_tuple] from above works *)

(**
Since tuples are a subtype of lists, we
can reuse the theory of lists over equality types.
*)

Example test_eqtype (x y : 3.-tuple nat) :
  x == y -> True.
Proof.
move=> /eqP.
Abort.

(** * Finite types *)

From mathcomp Require Import choice fintype finfun.

(**
Fig. 3 of "Packaging Mathematical Structures"
by F. Garillot, G. Gonthier, A. Mahboubi,
L. Rideau(2009)
*)

(** A [finType] structure is composed of
    a list of elements of an [eqType] structure,
    each element of the type being uniquely
    represented in the list:

(* simplified definition of [finType] *)
  Structure finType : Type :=
    FinType {
        sort :> countType;
        enum : seq sort;
        enumP : forall x,
                  count (pred1 x) enum = 1;
    }.
*)

(**
Finite sets are then sets taken in a [finType]
domain. In the library, the basic operations
are provided.
For example, given [A] a finite set,
[card A] (or #|A|) represents the cardinality
of A. All these operations come with their
basic properties. For example, we have:

  Lemma cardUI : ∀ (d: finType) (A B: {pred T}),
    #|A ∪ B| + #|A ∩ B| = #|A| + #|B|.

  Lemma card_image :
    ∀ (T T': finType) (f : T -> T')
      injective f -> forall A : {pred T},
      #|image f A| = #|A|.
*)

(** ** How [finType] is actually organized *)

Print Finite.type.
(**
  Structure type : Type :=
    Pack {
      sort : Type;
      _ : Finite.class_of sort
    }.
*)

(** [finType] extends [choiceType] with a mixin *)
Print Finite.class_of.
(**
  Structure class_of (T : Type) : Type :=
    Class {
      base : Choice.class_of T;
      mixin : Finite.mixin_of (EqType T base)
    }
*)

Print Finite.mixin_of.
(** we mix in countable and two specific fields:
    an enumeration and an axiom

  Structure mixin_of (T : eqType) : Type :=
    Mixin {
      mixin_base : Countable.mixin_of T;
      mixin_enum : seq T;
      _ : Finite.axiom mixin_enum
    }.
*)

Print Finite.axiom.
(**
  Finite.axiom =
    fun (T : eqType) (e : seq T) =>
      forall x : T, count_mem x e = 1

where
  Notation count_mem x := (count (pred1 x)).
*)

Eval cbv in count_mem 5 [:: 1; 5; 2; 5; 3; 5; 4].

Section FinTypeExample.

Variable T : finType.

(** Cardinality of a finite type *)
Check #| T |.

(** "bounded" quantification *)
Check [forall x : T, x == x] && false.
Fail Check (forall x : T, x == x) && false.

(** We recover classical reasoning for
    the bounded quantifiers: *)
Check negb_forall:
  forall (T : finType) (P : pred T),
    ~~ [forall x, P x] = [exists x, ~~ P x].

Check negb_exists:
  forall (T : finType) (P : pred T),
    ~~ [exists x, P x] = [forall x, ~~ P x].

(** [negb_forall] does not hold
    in intuitionistic setting *)

End FinTypeExample.

(** * Examples of interfaces *)

From mathcomp Require Import finset.

Section Interfaces.

Variable chT : choiceType.

Check (@sigW chT).

Check [eqType of chT].

Variable coT : countType.

Check [countType of nat].
Check [choiceType of coT].
Check [choiceType of nat * nat].
Check [choiceType of seq coT].

Variable fT : finType.

Check [finType of bool].
Check [finType of 'I_10].
Check [finType of {ffun 'I_10 -> fT}].
Check [finType of bool * bool].
Check [finType of 3.-tuple bool].
Fail Check [finType of 3.-tuple nat].

Check {set 'I_4} : Type.
Check forall a : {set 'I_4},
        (a == set0) || (1 < #|a| < 4).
Print set_type.
Check {ffun 'I_4 -> bool} : Type.
Print finfun_eqType.
Check [eqType of #| 'I_4 |.-tuple bool].
Check [finType of #| 'I_4 |.-tuple bool].

Check {ffun 'I_4 * 'I_6 -> nat} : Type.
Check [eqType of {ffun 'I_4 * 'I_6 -> nat}] : Type.

End Interfaces.

(** * Bonus *)

(* The following requires
   the coq-mathcomp-algebra package
   from opam package manager *)
From mathcomp Require Import all_algebra.
Open Scope ring_scope.

Print matrix.

Section Rings.

Variable R : ringType.

Check forall x : R, x * 1 == x.

(** Matrices of size 4x4 over an arbitrary ring [R] *)
Check forall m : 'M[R]_(4,4), m == m * m.

End Rings.

author: vyorkin

repo: coq-fv

save_path: github-repos/coq/vyorkin-coq-fv


text:
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Typeclass-based setoids. Definitions on [Equivalence].

   Author: Matthieu Sozeau
   Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)

(* $Id: Equivalence.v 14641 2011-11-06 11:59:10Z herbelin $ *)

Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.

Require Import Coq.Classes.Init.
Require Import Relation_Definitions.
Require Export Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable Variables A R eqA B S eqB.
Local Obligation Tactic := simpl_relation.

Open Local Scope signature_scope.

Definition equiv `{Equivalence A R} : relation A := R.

(** Overloaded notations for setoid equivalence and inequivalence.
    Not to be confused with [eq] and [=]. *)

Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.

Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.

Open Local Scope equiv_scope.

(** Overloading for [PER]. *)

Definition pequiv `{PER A R} : relation A := R.

(** Overloaded notation for partial equivalence. *)

Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.

(** Shortcuts to make proof search easier. *)

Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.

Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.

Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.

  Next Obligation.
  Proof.
    transitivity y ; auto.
  Qed.

(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)

Ltac setoid_subst H :=
  match type of H with
    ?x === ?y => substitute H ; clear H x
  end.

Ltac setoid_subst_nofail :=
  match goal with
    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
    | _ => idtac
  end.

(** [subst*] will try its best at substituting every equality in the goal. *)

Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.

(** Simplify the goal w.r.t. equivalence. *)

Ltac equiv_simplify_one :=
  match goal with
    | [ H : ?x === ?x |- _ ] => clear H
    | [ H : ?x === ?y |- _ ] => setoid_subst H
    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
    | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
  end.

Ltac equiv_simplify := repeat equiv_simplify_one.

(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
   for easy recognition in tactics. *)

Ltac equivify_tac :=
  match goal with
    | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
    | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
  end.

Ltac equivify := repeat equivify_tac.

Section Respecting.

  (** Here we build an equivalence instance for functions which relates respectful ones only,
     we do not export it. *)

  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type :=
    { morph : A -> B | respectful R R' morph morph }.

  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
    Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).

  Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.

  Next Obligation.
  Proof.
    unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
  Qed.

End Respecting.

(** The default equivalence on function spaces, with higher-priority than [eq]. *)

Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
  Equivalence (pointwise_relation A eqB) | 9.

  Next Obligation.
  Proof.
    transitivity (y a) ; auto.
  Qed.

author: JasonGross

repo: category-coq-experience-tests


text:
Load LFindLoad.
From lfind Require Import LFind.
From QuickChick Require Import QuickChick.
From adtind Require Import goal33.

Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.

Lemma conj33synthconj4 : forall  (lv0 : natural) (lv1 : natural), (@eq natural (plus (plus (mult lv0 lv1) lv1) (Succ lv0)) (plus lv1 (Succ (mult (Succ lv1) lv0)))).
Admitted.
QuickChick conj33synthconj4.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Inductive day : Type :=
  | monday : day
  | tuesday : day
  | wednesday : day
  | thursday : day
  | friday : day
  | saturday : day
  | sunday : day.
Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.
Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.

author: georgydunaev

repo: TRASH

save_path: github-repos/coq/georgydunaev-TRASH


text:
Require Import List.
Import ListNotations.

Set Implicit Arguments.

Fixpoint fin (n : nat) : Type :=
  match n with
    | 0 => False
    | S n' => option (fin n')
  end.

Fixpoint fin_eq_dec (n : nat) : forall (a b : fin n), {a = b} + {a <> b}.
  refine
   (match n with
      | 0 => fun a b : fin 0 => right (match b with end)
      | S n' => fun a b : fin (S n') =>
                 match a, b with
                   | Some a', Some b' =>
                     match fin_eq_dec n' a' b' with
                       | left _ _ => left _
                       | right _ _ => right _
                     end
                   | Some a', None => right _
                   | None, Some b' => right _
                   | None, None => left eq_refl
                 end
    end); congruence.
Defined.

Fixpoint all_fin (n : nat) : list (fin n) :=
  match n with
    | 0 => []
    | S n' => None :: map (fun x => Some x) (all_fin n')
  end.

Lemma all_fin_all :
  forall n (x : fin n),
    In x (all_fin n).
Proof.
  induction n; intros.
  - inversion x.
  - simpl in *. destruct x; auto using in_map.
Qed.

Lemma NoDup_map_injective : forall A B (f : A -> B) xs,
    (forall x y, In x xs -> In y xs ->
            f x = f y -> x = y) ->
    NoDup xs -> NoDup (map f xs).
Proof using.
  induction xs; intros.
  - constructor.
  - simpl. inversion H0. subst. constructor.
    + intro.
      apply in_map_iff in H1.
      destruct H1.
      destruct H1.
      assert (x = a) by intuition.
      subst.
      congruence.
    + intuition.
Qed.

Lemma all_fin_NoDup :
  forall n, NoDup (all_fin n).
Proof.
  induction n; intros; simpl; constructor.
  - intro. apply in_map_iff in H. firstorder. discriminate.
  - apply NoDup_map_injective; auto. congruence.
Qed.

author: proofengineering

repo: serapi-tests