text:
Require Import OrderedType.
Require Import String.
Require Import Utf8_core.
Require Import FunInd.
Require Import NArith Lia.

Module VarsString <: OrderedType with Definition t := String.string.
  Definition t:= String.string.
  Definition eq := @eq t.

  Module M.  (* Just to bypass sort of a bug in rewrite *)
    Function lt (s1 s2:string) {struct s1} : Prop :=
      match s1,s2 with
        | EmptyString,EmptyString => False
        | EmptyString, _ => True
        | _,EmptyString => False
        | String c1 s1, String c2 s2 =>
          ((Ascii.nat_of_ascii c1) < (Ascii.nat_of_ascii c2)) \/
          ((c1=c2) /\ lt s1 s2)
      end.

    Function compare_digits (l1 l2:list bool) {struct l1} : comparison :=
      match l1,l2 with
        | nil,nil => Eq
        | _,nil => Gt
        | nil,_ => Lt
        | b1::l1,b2::l2 =>
          match compare_digits l1 l2 with
            | Eq => match b1,b2 with
                      | true,true | false,false => Eq
                      | false,true => Lt
                      | true,false => Gt
                    end
            | v => v
          end
      end.

    Definition ascii_compare c1 c2 :=
      match c1,c2 with
        Ascii.Ascii b1 b2 b3 b4 b5 b6 b7 b8,
        Ascii.Ascii b1' b2' b3' b4' b5' b6' b7' b8' =>
        compare_digits
        (b1::b2::b3::b4::b5::b6::b7::b8::nil)
        (b1'::b2'::b3'::b4'::b5'::b6'::b7'::b8'::nil)
      end.

    Lemma compare_digits_eq_correct : forall l1 l2,
      compare_digits l1 l2 = Eq -> l1 = l2.
    Proof.
      intros l1 l2.
      functional induction (compare_digits l1 l2);try discriminate;intros;f_equal;auto.
      rewrite H in y;tauto.
    Qed.

    Lemma ascii_compare_eq_correct :
      forall c1 c2, ascii_compare c1 c2 = Eq -> c1 = c2.
    Proof.
      destruct c1 as [b1 b2 b3 b4 b5 b6 b7 b8];
        destruct c2 as [b1' b2' b3' b4' b5' b6' b7' b8'].
      unfold ascii_compare.
      intros H.
      apply compare_digits_eq_correct in H.
      injection H;intros;subst;reflexivity.
    Qed.

    Lemma compare_digits_lt_correct :
      forall (l1 l2:list bool),
        List.length l1 = List.length l2 ->
        compare_digits l1 l2 = Lt ->
        N.lt (Ascii.N_of_digits l1) (Ascii.N_of_digits l2).
    Proof.
      intros l1 l2;functional induction (compare_digits l1 l2);try discriminate.

      destruct l2;tauto||(simpl;discriminate).

      intros Hlength;injection Hlength;clear Hlength;intro Hlength.
      rewrite (compare_digits_eq_correct _ _ e1).
      simpl.
      destruct ( Ascii.N_of_digits l3).
      vm_compute;reflexivity.
      intros _.
      unfold N.lt.
      cbn.
      apply BinPos.Pcompare_refl_id.

      intros Hlength;injection Hlength;clear Hlength;intro Hlength.
      intros Heq;rewrite Heq in *.
      simpl.
      generalize (IHc Hlength (refl_equal _)).
      destruct b1;destruct b2;
      destruct (Ascii.N_of_digits l0);
        destruct (Ascii.N_of_digits l3);
          try (vm_compute;tauto).
      vm_compute;discriminate.
      lia.
      lia.
    Qed.

    Lemma compare_digits_gt_correct :
      forall (l1 l2:list bool),
        List.length l1 = List.length l2 ->
        compare_digits l1 l2 = Gt ->
        N.lt (Ascii.N_of_digits l2) (Ascii.N_of_digits l1).
    Proof.
      intros l1 l2;functional induction (compare_digits l1 l2);try discriminate.

      destruct l1;tauto||(simpl;discriminate).

      intros Hlength;injection Hlength;clear Hlength;intro Hlength.
      rewrite (compare_digits_eq_correct _ _ e1).
      simpl.
      destruct ( Ascii.N_of_digits l3).
      vm_compute;reflexivity.
      lia.

      intros Hlength;injection Hlength;clear Hlength;intro Hlength.
      intros Heq;rewrite Heq in *.
      simpl.
      generalize (IHc Hlength (refl_equal _)).
      destruct b1;destruct b2;
      destruct (Ascii.N_of_digits l0);
        destruct (Ascii.N_of_digits l3);
          try (vm_compute;tauto).
      lia.
      lia.
      lia.
    Qed.

    Lemma ascii_compare_lt_correct : forall c1 c2, ascii_compare c1 c2 = Lt -> (Ascii.nat_of_ascii c1) < (Ascii.nat_of_ascii c2).
    Proof.
      unfold ascii_compare.
      destruct c1;destruct c2.
      intros Heq.
      apply compare_digits_lt_correct in Heq;[|vm_compute;reflexivity].
      unfold Ascii.nat_of_ascii.
      assert (forall p q, (p < q)%N -> (BinNat.nat_of_N p) < (BinNat.nat_of_N q)).
      clear .
      intros p q.
      lia.
      apply H;assumption.
    Qed.

    Lemma ascii_compare_gt_correct : forall c1 c2, ascii_compare c1 c2 = Gt -> (Ascii.nat_of_ascii c2) < (Ascii.nat_of_ascii c1).
    Proof.
      unfold ascii_compare.
      destruct c1;destruct c2.
      intros Heq.
      apply compare_digits_gt_correct in Heq;[|vm_compute;reflexivity].
      unfold Ascii.nat_of_ascii.
      assert (forall p q, (p < q)%N -> (BinNat.nat_of_N p) < (BinNat.nat_of_N q)).
      clear .
      intros p q.
      lia.
      apply H;assumption.
    Qed.

    Function compare' (s1 s2 : string) {struct s1} : comparison :=
      match s1,s2 with
        | EmptyString,EmptyString => Eq
        | EmptyString,_ => Lt
        | _,EmptyString => Gt
        | String c1 s1,String c2 s2 =>
          match ascii_compare c1 c2 with
            | Eq => compare' s1 s2
            | v => v
          end
      end.

    Lemma compare'_eq_correct : forall s1 s2, compare' s1 s2 = Eq -> s1=s2.
    Proof.
      intros s1 s2;functional induction (compare' s1 s2);
        reflexivity || (try discriminate).

      intros Heq;rewrite (IHc Heq).
      rewrite (ascii_compare_eq_correct _ _ e1).
      reflexivity.

      intros Heq;rewrite Heq in y;tauto.
    Qed.

    Lemma compare'_lt_correct :
      forall s1 s2, compare' s1 s2 = Lt -> lt s1 s2.
    Proof.
      intros s1 s2;functional induction (compare' s1 s2);
        reflexivity || (try discriminate).

      destruct s2;try tauto.

      intros Heq;assert (IHc':=IHc Heq);clear IHc Heq.
      simpl.
      right;rewrite (ascii_compare_eq_correct _ _ e1);tauto.

      intros Heq;clear y.
      simpl;left;apply ascii_compare_lt_correct;assumption.
    Qed.

    Lemma compare'_gt_correct :
      forall s1 s2, compare' s1 s2 = Gt -> lt s2 s1.
    Proof.
      intros s1 s2;functional induction (compare' s1 s2);
        reflexivity || (try discriminate).

      destruct s1;try tauto.

      intros Heq;assert (IHc':=IHc Heq);clear IHc Heq.
      simpl.
      right;rewrite (ascii_compare_eq_correct _ _ e1);tauto.

      intros Heq;clear y.
      simpl;left;apply ascii_compare_gt_correct;assumption.
    Qed.

  End M.
  Import M.
  Definition eq_sym := @Logic.eq_sym t.
  Definition eq_refl := @Logic.eq_refl t.
  Definition eq_trans := @Logic.eq_trans t.

  Definition lt := M.lt.

  Ltac clear_goal :=
    repeat match goal with
      | h: ?t = ?t  |- _ => clear h
      | h: Compare_dec.lt_eq_lt_dec _ _ = _  |- _ => clear h
    end.

  Lemma lt_trans : forall s1 s2 s3, lt s1 s2 -> lt s2 s3 -> lt s1 s3.
  Proof.
    unfold lt.
    intros s1 s2.
    functional induction (M.lt s1 s2);try tauto.
    intros s3. revert y;functional induction (M.lt s2 s3);simpl;try tauto.
    destruct s1;simpl;try tauto.
    intuition (subst).
    left;eauto with arith .
    left;eauto with arith .
    left;eauto with arith .
    right;eauto.
  Qed.

  Lemma lt_not_eq : ∀ x y, lt x y -> not (eq x y).
  Proof.
    unfold lt.
    intros s1 s2; functional induction (M.lt s1 s2);try tauto.

    unfold eq;intros _ abs;subst;tauto.

    intuition.
    unfold eq in H0;simpl in H0;injection H0;clear H0;intros;subst;lia.
    subst.
    injection H0;clear H0;intros;subst;unfold eq in *;auto.
  Qed.

  Lemma compare : ∀ x y, Compare lt eq x y.
  Proof.
    intros x y.
    case_eq (compare' x y);intros Heq.
    constructor 2.
    apply compare'_eq_correct;assumption.
    constructor 1.
    apply compare'_lt_correct;assumption.
    constructor 3.
    apply compare'_gt_correct;assumption.
  Defined.

  Function eq_bool (s1 s2: string) {struct s1} : bool :=
    match s1,s2 with
      | EmptyString,EmptyString => true
      | String c1 s1,String c2 s2 =>
        if Peano_dec.eq_nat_dec (Ascii.nat_of_ascii c1) (Ascii.nat_of_ascii c2)
          then eq_bool s1 s2
          else false
      | _,_ => false
    end.

  Lemma eq_bool_correct : forall s1 s2, eq_bool s1 s2 = true -> eq s1 s2.
  Proof.
    intros s1 s2;functional induction (eq_bool s1 s2);try discriminate.

    reflexivity.

    intros H;assert (IHb':=IHb H);clear IHb H.
    red. f_equal.
    rewrite <- (Ascii.ascii_nat_embedding c1);
    rewrite <- (Ascii.ascii_nat_embedding c2);
    rewrite _x. reflexivity.
    exact IHb'.
  Qed.

  Lemma eq_bool_correct_2 : forall s1 s2, eq_bool s1 s2 = false -> ~ eq s1 s2.
  Proof.
    intros s1 s2;functional induction (eq_bool s1 s2);try discriminate.

    intros H;assert (IHb':= IHb H);clear e1 IHb H;intro abs;red in abs;injection abs;clear abs;intros;elim IHb';assumption.

    intros _;clear e1;intro abs;red in abs;injection abs;clear abs;intros;elim _x;subst;reflexivity.

    intros _ abs;destruct s1;destruct s2;simpl in y;try tauto;
    discriminate abs.
  Qed.

  Definition eq_dec : forall (s1 s2:string), {eq s1 s2}+{~eq s1 s2}.
  Proof.
    intros s1 s2.
    case_eq (eq_bool s1 s2);intro H.
    left;apply eq_bool_correct;exact H.
    right;apply eq_bool_correct_2;assumption.
  Qed.

End VarsString.

author: ComputerAidedLL


text:
Require Import Coq.Sets.Ensembles.
Require Import Arith.

Definition var := nat.

Definition monomial := Ensemble var.

Definition polynomial := Ensemble monomial.

Inductive SymDiff {U:Type} (B C:Ensemble U) : Ensemble U :=
  | SymDiff_intro : forall x:U, In U B x \/ In U C x -> ~ In U (Intersection U B C) x -> In U (SymDiff B C) x.

Lemma SymDiff_refl:
  forall {U:Type} (B : Ensemble U) (x:U), In U (SymDiff B B) x -> False.
Proof.
  intros U B x H. inversion H. apply H1. destruct H0; apply Intersection_intro; intuition.
Qed.

Definition addPP (p q : polynomial) : polynomial := SymDiff p q.

Definition mulMM (m n : monomial) : monomial := Union var m n.

Lemma Aeq_dec:
  forall (x y : nat),
  {x = y} + {x <> y}.
Proof.
  intros x y. destruct (beq_nat x y) eqn:H.
  - apply beq_nat_true_iff in H. left. apply H.
  - apply beq_nat_false_iff in H. right. apply H.
Qed.

Inductive mulMP (m:monomial) (B:polynomial) : polynomial :=
  | mulMP_intro : forall n:monomial, In monomial B n -> In monomial (mulMP m B) (mulMM m n).

Inductive mulPP (B C:polynomial) : polynomial :=
  | mulPP_intro : forall m:monomial, In monomial B m -> Included monomial (mulMP m C) (mulPP B C).

Definition repl := (prod var polynomial).

Definition subst := list repl.

Definition inDom (x : var) (s : subst) : bool :=
  List.existsb (beq_nat x) (List.map fst s).

Fixpoint appSubst (s : subst) (x : var) : polynomial :=
  match s with
  | nil => Singleton monomial (Singleton var x)
  | cons (y,p) s1 => if (x =? y) then p else (appSubst s1 x)
  end.

Fixpoint substM (s : subst) (m : monomial) : polynomial :=
  match s with
  | nil => Singleton monomial (Empty_set var)
  | cons (y,p) s1 =>
    match (inDom y s) with
    | true => mulPP (appSubst s y) (substM s1 m)
    | false => mulMP (Singleton var y) (substM s1 m)
    end
  end.

Inductive substP (s : subst) (p : polynomial) : polynomial :=
  | substP_intro : forall m:monomial, In monomial p m -> Included monomial (addPP (substM s m) (substP s (Subtract monomial p m))) (substP s p).

author: dandougherty


text:
Require Export RecTypes.SpecTypes.
Require Export RecTypes.InstTy.
Require Export RecTypes.Contraction.
Require Export RecTypes.ValidTy.
Require Export RecTypes.LemmasTypes.

Require Import StlcEqui.SpecSyntax.
Require Import StlcEqui.SpecEvaluation.
Require Import StlcEqui.LemmasEvaluation.
Require Import StlcEqui.SpecTyping.
Require Import StlcEqui.SpecAnnot.
Require Import StlcEqui.LemmasTyping.
Require Import StlcEqui.Inst.
Require Import StlcEqui.InstAnnot.
Require Import Db.Lemmas.
Require Import Db.WellScoping.

Require Import Coq.Bool.Bool.

Local Ltac crush :=
  intros; cbn in * |-;
  repeat
    (cbn;
     repeat crushRecTypesMatchH;
     repeat crushStlcSyntaxMatchH;
     repeat crushDbSyntaxMatchH;
     repeat crushDbLemmasRewriteH;
     rewrite <- ?ap_liftSub, <- ?up_liftSub
     (* repeat crushStlcEquiScopingMatchH; *)
     (* repeat crushScopingMatchH *)
    );
  auto.

(* Definition ufix₂_annot (f : TmA) (τ1 τ2 : Ty) : TmA := *)
(*   let t : TmA := ia_abs (trec (tarr (tvar 0) (tarr τ1 τ2)[wkm])) *)
(*                        (tarr τ1 τ2) *)
(*                        (ia_app (tarr τ1 τ2) (tarr τ1 τ2) f[wkm] *)
(*                                (ia_abs τ1 τ2 (ia_app τ1 τ2 (ia_app (trec (tarr (tvar 0) (tarr τ1 τ2)[wkm])) (tarr τ1 τ2) (ia_unfold_ (tarr (tvar 0) (tarr τ1 τ2)[wkm]) (ia_var 1)) (ia_var 1)) (ia_var 0)))) *)
(*   in ia_app (trec (tarr (tvar 0) (tarr τ1 τ2)[wkm])) (tarr τ1 τ2) (ia_unfold_ (tarr (tvar 0) (tarr τ1 τ2)[wkm]) (ia_fold_ (tarr (tvar 0) (tarr τ1 τ2)[wkm]) t)) (ia_fold_ (tarr (tvar 0) (tarr τ1 τ2)[wkm]) t). *)

Definition ufix₁_annot (f : TmA) (τ1 τ2 : Ty) : TmA :=
  let t : TmA := ea_abs (trec (tarr (tvar 0) (tarr τ1 τ2)))
                       (tarr τ1 τ2)
                       (ea_app (tarr τ1 τ2) (tarr τ1 τ2) f[wkm]
                               (ea_abs τ1 τ2 (ea_app τ1 τ2 (ea_app (trec (tarr (tvar 0) (tarr τ1 τ2))) (tarr τ1 τ2) (ea_coerce (trec (tarr (tvar 0) (tarr τ1 τ2))) (ea_var 1)) (ea_var 1)) (ea_var 0))))
  in ea_app (trec (tarr (tvar 0) (tarr τ1 τ2))) (tarr τ1 τ2)
            t
            (ea_coerce (tarr (trec (tarr (tvar 0) (tarr τ1 τ2))) (tarr τ1 τ2)) t).

Definition ufix_annot (τ1 τ2 : Ty) : TmA :=
  ea_abs (tarr (tarr τ1 τ2) (tarr τ1 τ2)) (tarr τ1 τ2) (ufix₁_annot (ea_var 0) τ1 τ2).

(* Definition ufix₂ (f : Tm) (τ1 τ2 : Ty) : Tm := *)
(*   let t : Tm := abs (trec (tarr (tvar 0) (tarr τ1 τ2)[wkm])) (app f[wkm] (abs τ1 (app (app (unfold_ (var 1)) (var 1)) (var 0)))) *)
(*   in app (unfold_ (fold_ t)) (fold_ t). *)

(* note that ufix₁ has a unfold-fold redex.
  this is of course unnecessary, but it will appear after evaluation, so it's easier to put it there from the start as well (to reduce the amount of different terms to keep track of).
*)
Definition ufix₁ (f : Tm) (τ1 τ2 : Ty) : Tm :=
  let t : Tm := abs (trec (tarr (tvar 0) (tarr τ1 τ2))) (app f[wkm] (abs τ1 (app (app (var 1) (var 1)) (var 0))))
  in app t t.

Definition ufix (τ1 τ2 : Ty) : Tm :=
  abs (tarr (tarr τ1 τ2) (tarr τ1 τ2)) (ufix₁ (var 0) τ1 τ2).

Lemma eraseAnnot_ufix {τ₁ τ₂} : eraseAnnot (ufix_annot τ₁ τ₂) = ufix τ₁ τ₂.
Proof.
  reflexivity.
Qed.

(* Lemma eraseAnnot_ufix₁ {f τ₁ τ₂} : eraseAnnot (ufix₁_annot f τ₁ τ₂) = ufix₁ (eraseAnnot f) τ₁ τ₂. *)
(* Proof. *)
(*   cbn. *)
(*   unfold ufix₁. *)
(*   admit. *)
(* Admitted. *)

Lemma ufix_eval₁' f (valf: Value f) {τ1 τ2} : (app (ufix τ1 τ2) f) --> (ufix₁ f τ1 τ2).
Proof.
  unfold ufix, ufix₁.
  apply (eval_ctx₀ phole); crush; eapply eval_beta''; crush.
Qed.

Lemma ufix_eval₁ f (valf: Value f) {τ1 τ2} : app (ufix τ1 τ2) f  --> ufix₁ f τ1 τ2.
Proof.
  eauto using ufix_eval₁'.
Qed.

Lemma ufix₁_evaln' {t τ1 τ2 τ} :
  evaln (ufix₁ (abs τ t) τ1 τ2) (t[beta1 (abs τ1 (app (ufix₁ (abs τ t[wkm↑]) τ1 τ2) (var 0)))]) 2.
Proof.
  unfold ufix₁.
  econstructor.
  { eapply eval_eval₀, eval_beta; now cbn. }
  cbn.
  repeat change (apTm ?ξ ?t) with t[ξ].
  rewrite <-?ap_liftSub, <-?up_liftSub, ?liftSub_wkm.
  rewrite apply_wkm_beta1_up_cancel.
  crushDbLemmasRewriteH.
  econstructor.
  { eapply eval_eval₀, eval_beta; now cbn. }
  econstructor.
Qed.

Lemma ufix₁_typing {t τ₁ τ₂ Γ} :
  ValidTy τ₁ -> ValidTy τ₂ ->
  ⟪ Γ e⊢ t : tarr (tarr τ₁ τ₂) (tarr τ₁ τ₂) ⟫ →
  ⟪ Γ e⊢ ufix₁ t τ₁ τ₂ : tarr τ₁ τ₂ ⟫.
Proof.
  intros (cl1 & cr1) (cl2 & cr2) tyt.
  unfold ufix₁.
  crushTypingMatchH.
  crushTypingMatchH.
  crushTypingMatchH.
  crushTyping.
  crushTypingMatchH.
  crushTypingMatchH.
  crushTypingMatchH.
  eapply WtEq with (T := trec (tvar 0 r⇒ τ₁ r⇒ τ₂)).
  eapply EqMuL.
  crush.
  rewrite ?wsClosed_invariant.
  eapply tyeq_refl.
  crush.
  crush.
  crushValidTy.
  crushValidTy.
  crushTyping.
  crushTyping.
  crushTyping.
  crushValidTy.
  crushValidTy.
  crushTypingMatchH.
  eapply EqMuR.
  crush.
  rewrite ?wsClosed_invariant.
  eapply tyeq_refl.
  crush.
  crush.
  crushValidTy.
  crushValidTy.
  crushTypingMatchH.
  crushTypingMatchH.
  crushTyping.
  crushTypingMatchH.
  crushTypingMatchH.
  crushTypingMatchH.
  eapply WtEq with (T := trec (tvar 0 r⇒ τ₁ r⇒ τ₂)).
  eapply EqMuL.
  crush.
  rewrite ?wsClosed_invariant.
  eapply tyeq_refl.
  crush.
  crush.
  crushValidTy.
  crushValidTy.
  crushTyping.
  crushTyping.
  crushTyping.
  crushValidTy.
  crushValidTy.
Qed.

Lemma ufix₁_annot_typing {t τ₁ τ₂ Γ} :
  ValidTy τ₁ -> ValidTy τ₂ ->
  ⟪ (Γ r▻ trec (tvar 0 r⇒ τ₁ r⇒ τ₂)) ea⊢ t [wkm] : tarr (tarr τ₁ τ₂) (tarr τ₁ τ₂) ⟫ →
  ⟪ Γ ea⊢ ufix₁_annot t τ₁ τ₂ : tarr τ₁ τ₂ ⟫.
Proof.
  intros (cl1 & cr1) (cl2 & cr2).
  unfold ufix₁_annot.
  crushTypingEA;
    crushValidTy.
  - eapply EqMuL.
    cbn. crush.
    rewrite ?wsClosed_invariant; try assumption.
    eapply tyeq_refl.
  - eapply EqMuR.
    cbn. crush.
    rewrite ?wsClosed_invariant; try assumption.
    eapply tyeq_refl.
  - eapply EqMuL.
    cbn. crush.
    rewrite ?wsClosed_invariant; try assumption.
    eapply tyeq_refl.
Qed.

Lemma ufix_annot_typing {τ₁ τ₂ Γ} :
  ValidTy τ₁ -> ValidTy τ₂ ->
  ⟪ Γ ea⊢ ufix_annot τ₁ τ₂ : tarr (tarr (tarr τ₁ τ₂) (tarr τ₁ τ₂)) (tarr τ₁ τ₂) ⟫.
Proof.
  intros (cl1 & cr1) (cl2 & cr2).
  constructor; crushValidTy.
  eapply ufix₁_annot_typing; crushValidTy.
  constructor.
  crushTyping.
Qed.

Lemma ufix_typing {τ₁ τ₂ Γ} :
  ValidTy τ₁ -> ValidTy τ₂ ->
  ⟪ Γ e⊢ ufix τ₁ τ₂ : tarr (tarr (tarr τ₁ τ₂) (tarr τ₁ τ₂)) (tarr τ₁ τ₂) ⟫.
Proof.
  intros vτ₁ vτ₂.
  change (ufix τ₁ τ₂) with (eraseAnnot (ufix_annot τ₁ τ₂)).
  now eapply eraseAnnotT, ufix_annot_typing.
Qed.

(* Lemma ufix₁_evaln {t} : evaln (ufix₁ (abs t)) (t[beta1 (abs (app (ufix₁ (abs t[wkm↑])) (var 0)))]) 2. *)
(* Proof. *)
(*   eauto using ufix₁_evaln', ctxevaln_evaln. *)
(* Qed. *)

(* Lemma ufix₁_eval {t} : ufix₁ (abs t) -->+ t[beta1 (abs (app (ufix₁ (abs t[wkm↑])) (var 0)))]. *)
(* Proof. *)
(*   refine (evaln_to_evalPlus _). *)
(*   apply ufix₁_evaln. *)
(* Qed. *)

(* Lemma ufix_ws (γ : Dom) : *)
(*   ⟨ γ ⊢ ufix ⟩. *)
(* Proof. *)
(*   unfold ufix, ufix₁. *)
(*   crush. *)
(* Qed. *)

(* (* TODO: simplify using result about scoping under subst... *) *)
(* Lemma ufix₁_ws {γ t} : *)
(*   ⟨ γ ⊢ t ⟩ → ⟨ γ ⊢ ufix₁ t ⟩. *)
(* Proof. *)
(*   unfold ufix₁. *)
(*   crush. *)
(* Qed. *)

author: dominiquedevriese

repo: fixismu-coq


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.
 *)

(* This includes some rewrites/simplification rules for the Nested relational calculus *)

Require Import String.
Require Import List.
Require Import ListSet.
Require Import BinInt.
Require Import Arith.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import Utils.
Require Import DataSystem.
Require Import cNNRCSystem.
Require Import NNRCSystem.
Require Import NNRCRewriteUtil.
Require Import NNRCRewrite.
Require Import TNNRCRewrite.
Require Import OptimizerLogger.
Require Import OptimizerStep.

Import ListNotations.
Local Open Scope list_scope.

Section NNRCOptimizer.
  Local Open Scope nnrc_scope.
  Local Open Scope string.

  Section engine.
    (** Apply the function f to the direct child of p *)
    Context {fruntime:foreign_runtime}.

    Definition nnrc_map (f: nnrc -> nnrc) (e:nnrc) :=
      match e with
      | NNRCGetConstant v => NNRCGetConstant v
      | NNRCVar v => NNRCVar v
      | NNRCConst d => NNRCConst d
      | NNRCBinop bop e1 e2 => NNRCBinop bop (f e1) (f e2)
      | NNRCUnop uop e1 => NNRCUnop uop (f e1)
      | NNRCLet v e1 e2 => NNRCLet v (f e1) (f e2)
      | NNRCFor v e1 e2 => NNRCFor v (f e1) (f e2)
      | NNRCIf e1 e2 e3 => NNRCIf (f e1) (f e2) (f e3)
      | NNRCEither ed xl el xr er => NNRCEither (f ed) xl (f el) xr (f er)
      | NNRCGroupBy g sl e1 => NNRCGroupBy g sl (f e1)
      end.

    Lemma nnrc_map_correctness:
      forall f: nnrc -> nnrc,
      forall e: nnrc,
        (forall e', nnrc_eq (f e') e') -> nnrc_eq (nnrc_map f e) e.
    Proof.
      intros f e Hf.
      nnrc_cases (induction e) Case;
        try solve [simpl; repeat rewrite Hf; reflexivity].
    Qed.

    (** Apply the function f to all subexpression of e. *)
    Fixpoint nnrc_map_deep (f: nnrc -> nnrc) (e: nnrc) :=
      match e with
      | NNRCGetConstant v => f (NNRCGetConstant v)
      | NNRCVar v => f (NNRCVar v)
      | NNRCConst d => f (NNRCConst d)
      | NNRCBinop bop e1 e2 => f (NNRCBinop bop (nnrc_map_deep f e1) (nnrc_map_deep f e2))
      | NNRCUnop uop e1 => f (NNRCUnop uop (nnrc_map_deep f e1))
      | NNRCLet v e1 e2 => f (NNRCLet v (nnrc_map_deep f e1) (nnrc_map_deep f e2))
      | NNRCFor v e1 e2 => f (NNRCFor v (nnrc_map_deep f e1) (nnrc_map_deep f e2))
      | NNRCIf e1 e2 e3 => f (NNRCIf (nnrc_map_deep f e1) (nnrc_map_deep f e2) (nnrc_map_deep f e3))
      | NNRCEither ed xl el xr er => f (NNRCEither (nnrc_map_deep f ed) xl (nnrc_map_deep f  el) xr (nnrc_map_deep f er))
      | NNRCGroupBy g sl e1 => f (NNRCGroupBy g sl (nnrc_map_deep f e1))
      end.

    Lemma nnrc_map_deep_corretness:
      forall f: nnrc -> nnrc,
      forall e: nnrc,
        (forall e', nnrc_eq (f e') e') -> nnrc_eq (nnrc_map_deep f e) e.
    Proof.
      intros f e Hf.
      nnrc_cases (induction e) Case; simpl;
        try solve [repeat rewrite Hf; reflexivity];
        try solve [repeat rewrite Hf; rewrite IHe; reflexivity ];
        try solve [repeat rewrite Hf; rewrite IHe1; rewrite IHe2; reflexivity ];
        try solve [repeat rewrite Hf; rewrite IHe1; rewrite IHe2; rewrite IHe3; reflexivity ].
    Qed.

    (* Java equivalent: NnrcOptimizer.rew_iter *)
    (*  Definition rew_iter (rew: nnrc -> nnrc) (fuel: nat) (p: nnrc)
    := iter rew fuel p.
     *)
    (* Java equivalent: NnrcOptimizer.rew_size *)
    (* Definition rew_size (rew: nnrc -> nnrc) (p: nnrc) :=
    iter_cost rew NNRCSize.nnrc_size p.
     *)
    (* *************************** *)

    (* unshadowing *)

    Definition nunshadow := unshadow_simpl nil.

    (* *************************** *)
    Definition head_rew (e: nnrc) :=
      (nunshadow e).

    Lemma head_rew_correctness e:
      nnrc_eq (head_rew e) e.
    Proof.
      unfold head_rew.
    apply nnrc_unshadow_preserves.
    Qed.

    Lemma rewriter_simpl_rew_no_free_var :
      forall (op : nnrc) (x : var),
        In x (nnrc_free_vars (head_rew op)) -> In x (nnrc_free_vars op).
    Proof.
      intros.
      unfold head_rew in H.
      eapply unshadow_free_vars; eapply H.
    Qed.
    (* *************************** *)

  End engine.

  Ltac tcorrectness_prover :=
    simpl; repeat progress
                  (try match goal with
                       | [|- context [match ?p with | _ => _ end] ] => destruct p
                       end; try reflexivity; try unfold Equivalence.equiv in *; try subst).

  Ltac tprove_correctness p :=
    destruct p;
    tcorrectness_prover.

  Lemma tnnrc_rewrites_to_trans {model:basic_model} e1 e2 e3:
    tnnrc_rewrites_to e1 e2 -> tnnrc_rewrites_to e2 e3 -> tnnrc_rewrites_to e1 e3.
  Proof.
    apply transitivity.
  Qed.

  Lemma AUX {model:basic_model} f e e' :
    (forall e, tnnrc_rewrites_to e (f e)) -> tnnrc_rewrites_to e e' -> tnnrc_rewrites_to e (f e').
  Proof.
    intros.
    rewrite H0 at 1.
    rewrite (H e') at 1.
    reflexivity.
  Qed.

  Definition tnnrc_map {fruntime:foreign_runtime} := nnrc_map.

  Lemma tnnrc_map_correctness {model:basic_model}:
    forall f: nnrc -> nnrc,
    forall p: nnrc,
      (forall p', tnnrc_rewrites_to p' (f p')) -> tnnrc_rewrites_to p (tnnrc_map f p).
  Proof.
    intros.
    nnrc_cases (induction p) Case; try solve [simpl; apply Hf]; simpl;
    try reflexivity;
    try (rewrite (H p1) at 1; rewrite (H p2) at 1; reflexivity).
    rewrite (H p) at 1; reflexivity.
    simpl.
    rewrite (H p1) at 1; rewrite (H p2) at 1; rewrite (H p3) at 1.
    reflexivity.
    rewrite (H p1) at 1; rewrite (H p2) at 1; rewrite (H p3) at 1.
    reflexivity.
    rewrite (H p) at 1; reflexivity.
  Qed.

  Definition tnnrc_map_deep {fruntime:foreign_runtime} := nnrc_map_deep.
  Lemma tnnrc_map_deep_correctness {model:basic_model}:
    forall f: nnrc -> nnrc,
    forall p: nnrc,
      (forall p', tnnrc_rewrites_to p' (f p')) -> tnnrc_rewrites_to p (tnnrc_map_deep f p).
  Proof.
    intros f p Hf.
    nnrc_cases (induction p) Case; try solve [simpl; apply Hf];
    try reflexivity; simpl;
    try (rewrite IHp1 at 1; rewrite IHp2 at 1; rewrite Hf at 1; reflexivity);
    try (rewrite IHp at 1; rewrite Hf at 1; reflexivity).
    rewrite IHp1 at 1; rewrite IHp2 at 1; rewrite IHp3 at 1; rewrite Hf at 1; reflexivity.
    rewrite IHp1 at 1; rewrite IHp2 at 1; rewrite IHp3 at 1; rewrite Hf at 1; reflexivity.
  Qed.

  (****************)

  (* Java equivalent: NnrcOptimizer.tunshadow_preserves_fun *)
  Definition tunshadow_preserves_fun {fruntime:foreign_runtime} (e:nnrc) :=
    unshadow_simpl nil e.

  Lemma tunshadow_preserves_fun_correctness {model:basic_model} (e:nnrc):
    tnnrc_rewrites_to e (tunshadow_preserves_fun e).
  Proof.
    unfold tunshadow_preserves_fun, unshadow_simpl.
    apply tunshadow_preserves_arrow.
  Qed.

  Definition tunshadow_preserves_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "unshadow" (* name *)
         "Renames variables to avoid shadowing" (* description *)
         "tunshadow_preserves_fun" (* lemma name *)
         tunshadow_preserves_fun (* lemma *).

  Definition tunshadow_preserves_step_correct {model:basic_model}
    := mkOptimizerStepModel tunshadow_preserves_step tunshadow_preserves_fun_correctness.

  Definition tconcat_nil_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
    | NNRCBinop OpRecConcat (NNRCConst (drec nil)) ee => ee
    | NNRCBinop OpRecConcat ee (NNRCConst (drec nil)) => ee
    | _ => e
    end.

  Lemma tconcat_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tconcat_nil_fun e).
  Proof.
    destruct e; simpl; try reflexivity.
    destruct b; simpl; try reflexivity.
    destruct (e1 == (‵[||])).
    - rewrite e.
      apply tconcat_of_nil_l_arrow.
    - destruct (e2 == (‵[||])).
      + repeat rewrite e.
        rewrite tconcat_of_nil_r_arrow.
        repeat (match_destr; try reflexivity).
      + repeat (match_destr; try reflexivity; try congruence).
  Qed.

  Definition tconcat_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "concat/nil" (* name *)
         "Remove record concatenation with an empty bag" (* description *)
         "tconcat_nil_fun" (* lemma name *)
         tconcat_nil_fun (* lemma *).

  Definition tconcat_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tconcat_nil_step tconcat_nil_fun_correctness.

  Definition tmerge_nil_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
    | NNRCBinop OpRecMerge (NNRCConst (drec nil)) ee => NNRCUnop OpBag ee
    | NNRCBinop OpRecMerge ee (NNRCConst (drec nil)) => NNRCUnop OpBag ee
    | _ => e
    end.

  Lemma tmerge_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tmerge_nil_fun e).
  Proof.
    destruct e; simpl; try reflexivity.
    destruct b; simpl; try reflexivity.
    destruct (e1 == (‵[||])).
    - rewrite e.
      apply tmerge_of_nil_l_arrow.
    - destruct (e2 == (‵[||])).
      + repeat rewrite e.
        rewrite tmerge_of_nil_r_arrow.
        repeat (match_destr; try reflexivity).
      + repeat (match_destr; try reflexivity; try congruence).
  Qed.

  Definition tmerge_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "merge/nil" (* name *)
         "Remove record merge with an empty bag" (* description *)
         "tmerge_nil_fun" (* lemma name *)
         tmerge_nil_fun (* lemma *).

  Definition tmerge_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tmerge_nil_step tmerge_nil_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tfor_nil_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
    | NNRCFor x ‵{||} e2 => ‵{||}
    | _ => e
    end.

  Lemma tfor_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tfor_nil_fun e).
  Proof.
    tprove_correctness e.
    apply tfor_nil_arrow.
  Qed.

  Definition tfor_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "for/nil" (* name *)
         "Remove loop comprehensions over empty bags" (* description *)
         "tfor_nil_fun" (* lemma name *)
         tfor_nil_fun (* lemma *).

  Definition tfor_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tfor_nil_step tfor_nil_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tfor_singleton_to_let_fun  {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
    | NNRCFor x (NNRCUnop OpBag e1) e2
      => NNRCUnop OpBag (NNRCLet x e1 e2)
    | _ => e
    end.

  Lemma tfor_singleton_to_let_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tfor_singleton_to_let_fun e).
  Proof.
    tprove_correctness e.
    apply tfor_singleton_to_let_arrow.
  Qed.

  Definition tfor_singleton_to_let_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "for/singleton" (* name *)
         "Lower a loop comprehension over a singleton into a singleton of a let" (* description *)
         "tfor_singleton_to_let_step" (* lemma name *)
         tfor_singleton_to_let_fun (* lemma *).

  Definition tfor_singleton_to_let_step_correct {model:basic_model}
    := mkOptimizerStepModel tfor_singleton_to_let_step tfor_singleton_to_let_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tflatten_singleton_fun  {fruntime:foreign_runtime} (e:nnrc)
    := match e with
       | ♯flatten(‵{| e1 |}) => e1
       | _ => e
       end.

  Lemma tflatten_singleton_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tflatten_singleton_fun e).
  Proof.
    tprove_correctness e.
    apply tflatten_singleton_nnrc_arrow.
  Qed.

  Definition tflatten_singleton_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/singleton" (* name *)
         "Simplify a flatten of a singleton bag" (* description *)
         "tflatten_singleton_fun" (* lemma name *)
         tflatten_singleton_fun (* lemma *).

  Definition tflatten_singleton_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_singleton_step tflatten_singleton_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tflatten_nil_fun  {fruntime:foreign_runtime} (e:nnrc)
    := match e with
       | ♯flatten(‵{||}) => ‵{||}
       | _ => e
       end.

  Lemma tflatten_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tflatten_nil_fun e).
  Proof.
    tprove_correctness e.
    apply tflatten_nil_nnrc_arrow.
  Qed.

  Definition tflatten_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/nil" (* name *)
         "Simplify flatten of an empty bag" (* description *)
         "tflatten_nil_fun" (* lemma name *)
         tflatten_nil_fun (* lemma *).

  Definition tflatten_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_nil_step tflatten_nil_fun_correctness.

  Definition tsigma_to_if_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
      | (NNRCUnop OpFlatten
                 (NNRCFor v1 (NNRCUnop OpBag e2)
                         (NNRCIf e1
                                (NNRCUnop OpBag (NNRCVar v2))
                                (NNRCConst (dcoll nil))))) =>
        if (v1 == v2)
        then (NNRCLet v1 e2 (NNRCIf e1 (NNRCUnop OpBag (NNRCVar v1)) (NNRCConst (dcoll nil))))
        else e
      | _ => e
    end.

  (* ♯flatten({ e1 ? { $t1 } : {} | $t1 ∈ { e2 } }) ≡ LET $t1 := e2 IN e1 ? { $t1 } : {} *)

  Lemma tsigma_to_if_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tsigma_to_if_fun e).
  Proof.
    tprove_correctness e.
    apply tsigma_to_if_arrow.
  Qed.

  Definition tsigma_to_if_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "sigma/if" (* name *)
         "???" (* description *)
         "tsigma_to_if_fun" (* lemma name *)
         tsigma_to_if_fun (* lemma *).

  Definition tsigma_to_if_step_correct {model:basic_model}
    := mkOptimizerStepModel tsigma_to_if_step tsigma_to_if_fun_correctness.

  (* {| e3 | $t2 ∈ ♯flatten({| e2 ? ‵{|$t1|} : ‵{||} | $t1 ∈ e1 |}) |}
       ⇒ ♯flatten({| e2 ? ‵{| LET $t2 := $t1 IN e3 ]|} : ‵{||} | $t1 ∈ e1 |}) *)

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tmap_sigma_fusion_samevar_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
      | (NNRCFor v2
                (NNRCUnop OpFlatten
                         (NNRCFor v1 e1
                                 (NNRCIf e2 (NNRCUnop OpBag ee) (NNRCConst (dcoll nil)))))
                e3) =>
          if (v1 == v2)
          then
            (NNRCUnop OpFlatten
                     (NNRCFor v1 e1
                             (NNRCIf e2
                                    (NNRCUnop OpBag (NNRCLet v1 ee e3))
                                    (NNRCConst (dcoll nil)))))
        else e
      | _ => e
    end.

  Lemma tmap_sigma_fusion_samevar_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tmap_sigma_fusion_samevar_fun e).
  Proof.
    tprove_correctness e.
    apply tmap_sigma_fusion_samevar_arrow.
  Qed.

    Definition tmap_sigma_fusion_samevar_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "sigma/same var fusion" (* name *)
         "???" (* description *)
         "tmap_sigma_fusion_samevar_fun" (* lemma name *)
         tmap_sigma_fusion_samevar_fun (* lemma *).

  Definition tmap_sigma_fusion_samevar_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_sigma_fusion_samevar_step tmap_sigma_fusion_samevar_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tdot_of_rec_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
      | (NNRCUnop (OpDot s1)
                (NNRCUnop (OpRec s2) e1)) =>
        if (s1 == s2)
        then e1
        else e
      | _ => e
    end.

  Lemma tdot_of_rec_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tdot_of_rec_fun e).
  Proof.
    tprove_correctness e.
    apply tdot_of_rec.
  Qed.

    Definition tdot_of_rec_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "dot/rec" (* name *)
         "Simplify lookup of a new record constructor" (* description *)
         "tdot_of_rec_fun" (* lemma name *)
         tdot_of_rec_fun (* lemma *).

  Definition tdot_of_rec_step_correct {model:basic_model}
    := mkOptimizerStepModel tdot_of_rec_step tdot_of_rec_fun_correctness.

  (* Java equivalent: NOT IMPLEMENTED *)
  Definition tnth0_bag_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
      | (NNRCBinop OpBagNth (NNRCUnop OpBag e) (NNRCConst (dnat 0))) =>
        NNRCUnop OpLeft e
      | _ => e
    end.

  Lemma tnth0_bag_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tnth0_bag_fun e).
  Proof.
    tprove_correctness e.
    apply tnth0_bag.
  Qed.

  Definition tnth0_bag_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "nth0/bag" (* name *)
         "Simplify first element of a collection with one element" (* description *)
         "tnth0_bag_fun" (* lemma name *)
         tnth0_bag_fun (* lemma *).

  Definition tnth0_bag_step_correct {model:basic_model}
    := mkOptimizerStepModel tnth0_bag_step tnth0_bag_fun_correctness.

  (* Java equivalent: NOT IMPLEMENTED *)
  Definition tnth0_nil_fun  {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
      | NNRCBinop OpBagNth (NNRCConst (dcoll nil)) (NNRCConst (dnat 0)) =>
        NNRCConst dnone
      | _ => e
    end.

  Lemma tnth0_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tnth0_nil_fun e).
  Proof.
    tprove_correctness e.
    apply tnth0_nil.
  Qed.

  Definition tnth0_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "nth0/nil" (* name *)
         "Simplify first element of an empty collection" (* description *)
         "tnth0_nil_fun" (* lemma name *)
         tnth0_nil_fun (* lemma *).

  Definition tnth0_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tnth0_nil_step tnth0_nil_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tmerge_concat_to_concat_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | (‵[| (s1, p1)|] ⊗ ‵[| (s2, p2)|])
         => if (equiv_decb s1 s2)
            then e
            else (‵{|‵[| (s1, p1)|] ⊕ ‵[| (s2, p2)|]|})
       | _ => e
       end.

  Lemma tmerge_concat_to_concat_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tmerge_concat_to_concat_fun e).
  Proof.
    destruct e; simpl; try reflexivity.
    destruct b; simpl; try reflexivity.
    destruct e1; simpl; try reflexivity.
    destruct u; simpl; try reflexivity.
    destruct e2; simpl; try reflexivity.
    destruct u; simpl; try reflexivity.
    unfold equiv_decb.
    destruct (equiv_dec s s0); try reflexivity.
    apply tnnrc_merge_concat_to_concat_arrow; trivial.
  Qed.

    Definition tmerge_concat_to_concat_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "merge-concat->merge" (* name *)
         "Simplify a merge-concat of two singleton records with different fields using concat" (* description *)
         "tmerge_concat_to_concat_fun" (* lemma name *)
         tmerge_concat_to_concat_fun (* lemma *).

  Definition tmerge_concat_to_concat_step_correct {model:basic_model}
    := mkOptimizerStepModel tmerge_concat_to_concat_step tmerge_concat_to_concat_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tdot_of_concat_rec_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | (NNRCUnop (OpDot s) (NNRCBinop OpRecConcat e1 (NNRCUnop (OpRec s2) e2)))
         => if equiv_decb s s2
            then e2
            else (NNRCUnop (OpDot s) e1)
       | _ => e
       end.

  Lemma tdot_of_concat_rec_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tdot_of_concat_rec_fun e).
  Proof.
    destruct e; simpl; try reflexivity.
    destruct u; simpl; try reflexivity.
    destruct e; simpl; try reflexivity.
    destruct b; simpl; try reflexivity.
    destruct e2; simpl; try reflexivity.
    destruct u; simpl; try reflexivity.
    unfold equiv_decb.
    destruct (equiv_dec s s0); try reflexivity.
    - red in e; subst.
      apply tnnrc_dot_of_concat_rec_eq_arrow.
    - apply tnnrc_dot_of_concat_rec_neq_arrow.
      trivial.
  Qed.

    Definition tdot_of_concat_rec_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "dot/concat/rec 2" (* name *)
         "Simplifies lookup of a concatenation with a record constructor" (* description *)
         "tdot_of_concat_rec_fun" (* lemma name *)
         tdot_of_concat_rec_fun (* lemma *).

  Definition tdot_of_concat_rec_step_correct {model:basic_model}
    := mkOptimizerStepModel tdot_of_concat_rec_step tdot_of_concat_rec_fun_correctness.

  (** Inlining *)

  (* TODO: A better/less hacky cost function.  This will probably need many more real
     examples to tune with, as it will always contain some black-magic. *)
  (* Java equivalent: NnrcOptimizer.is_small_unop *)
  Definition is_small_unop {fruntime:foreign_runtime} (u:unary_op) :=
    match u with
    | OpIdentity
    | OpNeg
    | OpBag
    | OpLeft
    | OpRight
    | OpBrand _
    | OpRec _
      => true
    | _ => false
    end.

  (* Java equivalent: NnrcOptimizer.should_inline_small *)
  Fixpoint should_inline_small {fruntime:foreign_runtime} (from:nnrc)
    := match from with
       | NNRCVar _
       | NNRCConst _ => true
       | NNRCUnop u e => is_small_unop u && should_inline_small e
       | NNRCBinop OpRecConcat (NNRCUnop (OpRec _) e1) (NNRCUnop (OpRec _) e2) => true
       | _ => false
       end.

  (* Java equivalent: NnrcOptimizer.should_inline_few_occurances *)
  Definition should_inline_few_occurences {fruntime:foreign_runtime} (x:var) (to:nnrc)
    := match use_count x to with
       | NotUsed
       | UsedOnce => true
       | _ => false
       end.

  (* Java equivalent: NnrcOptimizer.should_inline *)
  Definition should_inline {fruntime:foreign_runtime} (x:var) (from to:nnrc)
    := should_inline_small from
       || should_inline_few_occurences x to.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tinline_let_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | NNRCLet x e1 e2 =>
         if should_inline x e1 e2
         then nnrc_subst (unshadow_simpl (nnrc_free_vars e1) e2) x e1
         else e
       | _ => e
       end.

  Lemma tinline_let_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tinline_let_fun e).
  Proof.
    tprove_correctness e.
    apply tlet_inline_arrow.
  Qed.

    Definition tinline_let_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "let inline" (* name *)
         "Inline let statements heuristically deemed suitable for inlining" (* description *)
         "tinline_let_fun" (* lemma name *)
         tinline_let_fun (* lemma *).

  Definition tinline_let_step_correct {model:basic_model}
    := mkOptimizerStepModel tinline_let_step tinline_let_fun_correctness.

  (* push map through either and if *)
  (* Java equivalent: NnrcOptimizer.[same] *)
    Definition tfor_over_if_nil_fun  {fruntime:foreign_runtime}(e:nnrc)
      := match e with
         | NNRCFor x (NNRCIf e1 e2 ‵{||}) ebody =>
                     (NNRCIf e1 (NNRCFor x e2 ebody) ‵{||})
       | _ => e
       end.

  Lemma tfor_over_if_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tfor_over_if_nil_fun e).
  Proof.
    tprove_correctness e.
    rewrite tfor_over_if_arrow; simpl.
    rewrite tfor_nil_arrow.
    reflexivity.
  Qed.

    Definition tfor_over_if_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "for/if/else nil" (* name *)
         "Push loop comprehension over an if statement through the if statement when the else clause just constructs an empty bag" (* description *)
         "tfor_over_if_nil_fun" (* lemma name *)
         tfor_over_if_nil_fun (* lemma *).

  Definition tfor_over_if_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tfor_over_if_nil_step tfor_over_if_nil_fun_correctness.

  (* for (map) fusion *)
    Definition tfor_over_for_fun  {fruntime:foreign_runtime}(e:nnrc)
      := match e with
         | NNRCFor x (NNRCFor y source body1) body2 =>
           if (in_dec string_dec y (nnrc_free_vars body2))
           then let fr := really_fresh_in
                     nnrc_unshadow_sep y (nnrc_free_vars body1 ++ nnrc_bound_vars body1) body2
                in NNRCFor fr source
                     (NNRCLet x (nnrc_subst body1 y (NNRCVar fr)) body2)
           else NNRCFor y source
                        (NNRCLet x body1 body2)
       | _ => e
       end.

  Lemma tfor_over_for_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tfor_over_for_fun e).
  Proof.
    tprove_correctness e.
    - rewrite <- tfor_over_for_arrow; simpl; trivial.
      + apply tproper_NNRCFor; try reflexivity.
        generalize (really_fresh_from_avoid nnrc_unshadow_sep v0 (nnrc_free_vars e1_2 ++ nnrc_bound_vars e1_2) e2)
        ; rewrite in_app_iff; intros inn.
         apply tnnrcfor_rename_arrow; tauto.
      + apply really_fresh_from_free.
    - apply tfor_over_for_arrow; simpl; trivial.
  Qed.

    Definition tfor_over_for_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "for/for" (* name *)
         "Fuse nested loop comprehensions" (* description *)
         "tfor_over_for_fun" (* lemma name *)
         tfor_over_for_fun (* lemma *).

  Definition tfor_over_for_step_correct {model:basic_model}
    := mkOptimizerStepModel tfor_over_for_step tfor_over_for_fun_correctness.

(* END *)
  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tfor_over_either_nil_fun  {fruntime:foreign_runtime} (e:nnrc)
    := match e with
       |  (NNRCFor x (NNRCEither e1 xl el xr ‵{||}) ebody)
          =>
            (    let xl' := really_fresh_in nnrc_unshadow_sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody in
              (NNRCEither e1
                       xl' (NNRCFor x (nnrc_subst el xl (NNRCVar xl')) ebody)
                       xr ‵{||}))
       | _ => e
       end.

  Lemma tfor_over_either_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tfor_over_either_nil_fun e).
  Proof.
    tprove_correctness e.
    rewrite tfor_over_either_arrow; simpl.
    rewrite tfor_nil_arrow.
    rewrite tnnrceither_rename_r_arrow by intuition; simpl.
    reflexivity.
  Qed.

    Definition tfor_over_either_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "for/either/right nil" (* name *)
         "Push loop comprehension over an either statement through the either statement when the right clause just constructs an empty bag" (* description *)
         "tfor_over_either_nil_fun" (* lemma name *)
         tfor_over_either_nil_fun (* lemma *).

  Definition tfor_over_either_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tfor_over_either_nil_step tfor_over_either_nil_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tunop_over_either_const_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | NNRCUnop op (NNRCEither e1 xl el xr (NNRCConst d)) =>
         NNRCEither e1 xl (NNRCUnop op el) xr (NNRCUnop op (NNRCConst d))
       | _ => e
       end.

  Lemma tunop_over_either_const_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tunop_over_either_const_fun e).
  Proof.
    tprove_correctness e.
    apply tnnrcunop_over_either_arrow.
  Qed.

    Definition tunop_over_either_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "unary/either/right const" (* name *)
         "Push unary operators through either when the right branch is a constant" (* description *)
         "tunop_over_either_const_fun" (* lemma name *)
         tunop_over_either_const_fun (* lemma *).

  Definition tunop_over_either_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tunop_over_either_const_step tunop_over_either_const_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tunop_over_if_const_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | NNRCUnop op (NNRCIf e1 e2 (NNRCConst d)) =>
         NNRCIf e1 (NNRCUnop op e2) (NNRCUnop op (NNRCConst d))
       | _ => e
       end.

  Lemma tunop_over_if_const_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tunop_over_if_const_fun e).
  Proof.
    tprove_correctness e.
    apply tnnrcunop_over_if_arrow.
  Qed.

  Definition tunop_over_if_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "unary/if/else const" (* name *)
         "Push unary operators through if when the else branch is a constant" (* description *)
         "tunop_over_if_const_fun" (* lemma name *)
         tunop_over_if_const_fun (* lemma *).

  Definition tunop_over_if_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tunop_over_if_const_step tunop_over_if_const_fun_correctness.

  (* Java equivalent: NOT IMPLEMENTED *)
  Definition tbinop_over_if_left_const_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | NNRCBinop op (NNRCIf e1 e2 (NNRCConst d)) e =>
         NNRCIf e1 (NNRCBinop op e2 e) (NNRCBinop op (NNRCConst d) e)
       | _ => e
       end.

  Lemma tbinop_over_if_left_const_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tbinop_over_if_left_const_fun e).
  Proof.
    tprove_correctness e.
    apply tnnrcbinop_over_if_left_arrow.
  Qed.

  Definition tbinop_over_if_left_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "binary/if/else const" (* name *)
         "Push binary operators through if when the else branch is a constant" (* description *)
         "tbinop_over_if_left_const_fun" (* lemma name *)
         tbinop_over_if_left_const_fun (* lemma *).

  Definition tbinop_over_if_left_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tbinop_over_if_left_const_step tbinop_over_if_left_const_fun_correctness.

  (* Java equivalent: NOT IMPLEMENTED *)
  Definition tbinop_over_let_left_const_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | NNRCBinop op (NNRCLet x e1 e2) (NNRCConst d) =>
         NNRCLet x e1 (NNRCBinop op e2 (NNRCConst d))
       | _ => e
       end.

  Lemma tbinop_over_let_left_const_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tbinop_over_let_left_const_fun e).
  Proof.
    tprove_correctness e.
    apply tnnrcbinop_over_let_left_arrow.
    unfold nnrc_free_vars.
    simpl.
    congruence.
  Qed.

  Definition tbinop_over_let_left_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "binary/let/const" (* name *)
         "Push binary operators through let when the right expression is a constant" (* description *)
         "tbinop_over_let_left_const_fun" (* lemma name *)
         tbinop_over_let_left_const_fun (* lemma *).

  Definition tbinop_over_let_left_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tbinop_over_let_left_const_step tbinop_over_let_left_const_fun_correctness.

    (* optimizations for rproject *)

  (* Java equivalent: NnrcOptimizer.[same] *)
   Definition tproject_nil_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject nil) e₁
        => NNRCConst (drec nil)
      | _ => e
    end.

  Definition tproject_nil_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_nil_fun p.
  Proof.
    tprove_correctness p.
    apply tnnrcproject_nil.
  Qed.

  Hint Rewrite @tproject_nil_fun_correctness : toptim_correct.

    Definition tproject_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "project/nil" (* name *)
         "Simplify record projection over empty bags" (* description *)
         "tproject_nil_fun" (* lemma name *)
         tproject_nil_fun (* lemma *).

  Definition tproject_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tproject_nil_step tproject_nil_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tproject_over_const_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject sl)
          (NNRCConst (drec l))
        => NNRCConst (drec (rproject l sl))
      | _ => e
    end.

  Definition tproject_over_const_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_const_fun p.
  Proof.
    tprove_correctness p.
    apply tnnrcproject_over_const.
  Qed.

  Hint Rewrite @tproject_over_const_fun_correctness : toptim_correct.

  Definition tproject_over_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "project/const rec" (* name *)
         "Simplify record projection over constant records" (* description *)
         "tproject_over_const_fun" (* lemma name *)
         tproject_over_const_fun (* lemma *).

  Definition tproject_over_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tproject_over_const_step tproject_over_const_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tproject_over_rec_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject sl)
          (NNRCUnop (OpRec s) p₁)
        => if in_dec string_dec s sl
           then NNRCUnop (OpRec s) p₁
           else ‵[||]
      | _ => e
    end.

  Definition tproject_over_rec_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_rec_fun p.
  Proof.
    tprove_correctness p.
    - apply tnnrcproject_over_rec_in; trivial.
    - apply tnnrcproject_over_rec_nin; trivial.
  Qed.

  Hint Rewrite @tproject_over_rec_fun_correctness : toptim_correct.

  Definition tproject_over_rec_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "project/rec" (* name *)
         "Simplify record projection over a record constructor" (* description *)
         "tproject_over_rec_fun" (* lemma name *)
         tproject_over_rec_fun (* lemma *).

  Definition tproject_over_rec_step_correct {model:basic_model}
    := mkOptimizerStepModel tproject_over_rec_step tproject_over_rec_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
   Definition tproject_over_concat_r_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject sl)
               (NNRCBinop OpRecConcat
                        p₁ (NNRCUnop (OpRec s) p₂))
        => if in_dec string_dec s sl
           then NNRCBinop OpRecConcat
                         (NNRCUnop (OpRecProject (remove string_dec s sl)) p₁)
                        (NNRCUnop (OpRec s) p₂)
           else (NNRCUnop (OpRecProject sl) p₁)
      | _ => e
    end.

  Definition tproject_over_concat_r_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_concat_r_fun p.
  Proof.
    tprove_correctness p.
    - apply tnnrcproject_over_concat_rec_r_in; trivial.
    - apply tnnrcproject_over_concat_rec_r_nin; trivial.
  Qed.

  Hint Rewrite @tproject_over_concat_r_fun_correctness : toptim_correct.

  Definition tproject_over_concat_r_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "project/concat/right rec" (* name *)
         "Simplify record projection over concatenation with a record constructor" (* description *)
         "tproject_over_concat_r_fun" (* lemma name *)
         tproject_over_concat_r_fun (* lemma *).

  Definition tproject_over_concat_r_step_correct {model:basic_model}
    := mkOptimizerStepModel tproject_over_concat_r_step tproject_over_concat_r_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
     Definition tproject_over_concat_l_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject sl)
               (NNRCBinop OpRecConcat
                        (NNRCUnop (OpRec s) p₁) p₂)
        => if in_dec string_dec s sl
                     (* this case would need shape/type inference to handle, since we don't know if s is in p₂ *)

           then e
           else (NNRCUnop (OpRecProject sl) p₂)
      | _ => e
    end.

  Definition tproject_over_concat_l_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_concat_l_fun p.
  Proof.
    tprove_correctness p.
    apply tnnrcproject_over_concat_rec_l_nin; trivial.
  Qed.

  Hint Rewrite @tproject_over_concat_l_fun_correctness : toptim_correct.

  Definition tproject_over_concat_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "project/concat/left rec" (* name *)
         "Simplify record projection over concatenation with a record constructor" (* description *)
         "tproject_over_concat_l_fun" (* lemma name *)
         tproject_over_concat_l_fun (* lemma *).

  Definition tproject_over_concat_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tproject_over_concat_l_step tproject_over_concat_l_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tproject_over_project_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject sl1)
          (NNRCUnop (OpRecProject sl2) p1)
        => NNRCUnop (OpRecProject (set_inter string_dec sl2 sl1)) p1
      | _ => e
    end.

  Definition tproject_over_project_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_project_fun p.
  Proof.
    tprove_correctness p.
    apply tnnrcproject_over_nnrcproject.
  Qed.

  Hint Rewrite @tproject_over_project_fun_correctness : toptim_correct.

  Definition tproject_over_project_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "project/project" (* name *)
         "Fuse nested record projections" (* description *)
         "tproject_over_project_fun" (* lemma name *)
         tproject_over_project_fun (* lemma *).

  Definition tproject_over_project_step_correct {model:basic_model}
    := mkOptimizerStepModel tproject_over_project_step tproject_over_project_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
   Definition tproject_over_either_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject sl)
          (NNRCEither p xl p₁ xr p₂)
        => NNRCEither p xl (NNRCUnop (OpRecProject sl) p₁) xr (NNRCUnop (OpRecProject sl) p₂)
      | _ => e
    end.

  Definition tproject_over_either_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_either_fun p.
  Proof.
    tprove_correctness p.
    apply tnnrcproject_over_either.
  Qed.

  Hint Rewrite @tproject_over_either_fun_correctness : toptim_correct.

  Definition tproject_over_either_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "project/either/" (* name *)
         "Push record projection through either" (* description *)
         "tproject_over_either_fun" (* lemma name *)
         tproject_over_either_fun (* lemma *).

  Definition tproject_over_either_step_correct {model:basic_model}
    := mkOptimizerStepModel tproject_over_either_step tproject_over_either_fun_correctness.

  (* count optimizations *)
  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tcount_over_flat_for_either_if_nil_fun  {fruntime:foreign_runtime} (e:nnrc)
    := match e with
       | (♯count(♯flatten(NNRCFor v
                              ehead (NNRCEither e1 xl
                                               (NNRCIf e11(‵{| e12|}) ‵{||}) xr ‵{||}))))
         => (♯count(♯flatten(NNRCFor v
                              ehead (NNRCEither e1 xl
                                               (NNRCIf e11(‵{| ‵(dunit) |}) ‵{||}) xr ‵{||}))))
       | _ => e
       end.

  Lemma tcount_over_flat_for_either_if_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tcount_over_flat_for_either_if_nil_fun e).
  Proof.
    destruct e; simpl; try reflexivity.
    repeat (match_destr; try reflexivity).
    apply tcount_over_flat_for_either_if_nil_arrow.
  Qed.

  Definition tcount_over_flat_for_either_if_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "count/flatten/for/either/right if/else nil" (* name *)
         "Remove work that is not needed when only the bag count is needed" (* description *)
         "tcount_over_flat_for_either_if_nil_fun" (* lemma name *)
         tcount_over_flat_for_either_if_nil_fun (* lemma *).

  Definition tcount_over_flat_for_either_if_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tcount_over_flat_for_either_if_nil_step tcount_over_flat_for_either_if_nil_fun_correctness.

  (* Java equivalent: NnrcOptimizer.[same] *)
  Definition tcount_over_flat_for_either_either_nil_fun  {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | (♯count(♯flatten(NNRCFor v
                                 ehead (NNRCEither e1 xl
                                                  (NNRCEither e11 xll (‵{| e12|}) xrr ‵{||}) xr ‵{||}))))
         => (♯count(♯flatten(NNRCFor v
                                    ehead (NNRCEither e1 xl
                                                     (NNRCEither e11 xll (‵{| ‵(dunit) |}) xrr ‵{||}) xr ‵{||}))))

     | _ => e
       end.

  Lemma tcount_over_flat_for_either_either_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tcount_over_flat_for_either_either_nil_fun e).
  Proof.
    destruct e; simpl; try reflexivity.
    repeat (match_destr; try reflexivity).
    apply tcount_over_flat_for_either_either_nil_arrow.
  Qed.

    Definition tcount_over_flat_for_either_either_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "count/flatten/for/either/right either/right nil" (* name *)
         "Remove work that is not needed when only the bag count is needed" (* description *)
         "tcount_over_flat_for_either_either_nil_fun" (* lemma name *)
         tcount_over_flat_for_either_either_nil_fun (* lemma *).

  Definition tcount_over_flat_for_either_either_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tcount_over_flat_for_either_either_nil_step tcount_over_flat_for_either_either_nil_fun_correctness.

  (* list of all optimizations *)
    Definition tnnrc_optim_list {fruntime:foreign_runtime} : list (@OptimizerStep nnrc)
      := [
          tconcat_nil_step
          ; tmerge_nil_step
          ; tfor_nil_step
          ; tfor_singleton_to_let_step
          ; tflatten_singleton_step
          ; tflatten_nil_step
          ; tsigma_to_if_step
          ; tmap_sigma_fusion_samevar_step
          ; tdot_of_rec_step
          ; tnth0_bag_step
          ; tnth0_nil_step
          ; tmerge_concat_to_concat_step
          ; tdot_of_concat_rec_step
          ; tinline_let_step
          ; tfor_over_if_nil_step
          ; tfor_over_for_step
          ; tfor_over_either_nil_step
          ; tunop_over_either_const_step
          ; tunop_over_if_const_step
          ; tbinop_over_if_left_const_step
          ; tbinop_over_let_left_const_step
          ; tproject_nil_step
          ; tproject_over_const_step
          ; tproject_over_rec_step
          ; tproject_over_concat_r_step
          ; tproject_over_concat_l_step
          ; tproject_over_project_step
          ; tproject_over_either_step
          ; tcount_over_flat_for_either_if_nil_step
          ; tcount_over_flat_for_either_either_nil_step
        ].

    Definition tnnrc_optim_model_list {model:basic_model} : list (OptimizerStepModel tnnrc_rewrites_to)
      := [
          tconcat_nil_step_correct
          ; tmerge_nil_step_correct
          ; tfor_nil_step_correct
          ; tfor_singleton_to_let_step_correct
          ; tflatten_singleton_step_correct
          ; tflatten_nil_step_correct
          ; tsigma_to_if_step_correct
          ; tmap_sigma_fusion_samevar_step_correct
          ; tdot_of_rec_step_correct
          ; tnth0_bag_step_correct
          ; tnth0_nil_step_correct
          ; tmerge_concat_to_concat_step_correct
          ; tdot_of_concat_rec_step_correct
          ; tinline_let_step_correct
          ; tfor_over_if_nil_step_correct
          ; tfor_over_for_step_correct
          ; tfor_over_either_nil_step_correct
          ; tunop_over_either_const_step_correct
          ; tunop_over_if_const_step_correct
          ; tbinop_over_if_left_const_step_correct
          ; tbinop_over_let_left_const_step_correct
          ; tproject_nil_step_correct
          ; tproject_over_const_step_correct
          ; tproject_over_rec_step_correct
          ; tproject_over_concat_r_step_correct
          ; tproject_over_concat_l_step_correct
          ; tproject_over_project_step_correct
          ; tproject_over_either_step_correct
          ; tcount_over_flat_for_either_if_nil_step_correct
          ; tcount_over_flat_for_either_either_nil_step_correct
        ].

  Lemma tnnrc_optim_model_list_complete {model:basic_model}
    : optim_model_list_complete tnnrc_optim_list tnnrc_optim_model_list.
  Proof.
    optim_correct_list_complete_prover.
  Qed.

  Definition tnnrc_optim_list_correct {model:basic_model}
    : optim_list_correct tnnrc_rewrites_to tnnrc_optim_list
    := optim_list_correct_from_model tnnrc_optim_model_list_complete.

  Lemma tnnrc_optim_list_distinct {fruntime:foreign_runtime}:
    optim_list_distinct tnnrc_optim_list.
  Proof.
    apply optim_list_distinct_prover.
    vm_compute.
    apply eq_refl.
  Qed.

  (* *************************** *)
  Definition nnrc_optim_top
             {fruntime:foreign_runtime}
             {logger:optimizer_logger string nnrc}
             (opc:optim_phases_config)
    : nnrc -> nnrc :=
    run_phases tnnrc_map_deep NNRCSize.nnrc_size tnnrc_optim_list opc.

  Lemma nnrc_optim_top_correctness
        {model:basic_model} {logger:optimizer_logger string nnrc}
        (opc:optim_phases_config)
        (p:nnrc) :
    tnnrc_rewrites_to p (nnrc_optim_top opc p).
  Proof.
    unfold nnrc_optim_top.
    apply run_phases_correctness.
    - intros. apply tnnrc_map_deep_correctness; auto.
    - apply tnnrc_optim_list_correct.
  Qed.

  Section default.

    (* Java equivalent: NnrcOptimizer.head_rew_list *)
    Definition nnrc_default_optim_list {fruntime:foreign_runtime} : list string
    := [
        optim_step_name tinline_let_step
        ; optim_step_name tcount_over_flat_for_either_either_nil_step
        ; optim_step_name tcount_over_flat_for_either_if_nil_step
        ; optim_step_name tmerge_concat_to_concat_step
        ; optim_step_name tdot_of_concat_rec_step
        ; optim_step_name tdot_of_rec_step
        ; optim_step_name tnth0_bag_step
        ; optim_step_name tnth0_nil_step
        ; optim_step_name tflatten_singleton_step
        ; optim_step_name tflatten_nil_step
        ; optim_step_name tfor_singleton_to_let_step
        ; optim_step_name tunop_over_either_const_step
        ; optim_step_name tunop_over_if_const_step
        ; optim_step_name tbinop_over_if_left_const_step
        ; optim_step_name tbinop_over_let_left_const_step
        ; optim_step_name tfor_over_either_nil_step
        ; optim_step_name tfor_over_for_step
        ; optim_step_name tfor_over_if_nil_step
        ; optim_step_name tfor_nil_step
        ; optim_step_name tmerge_nil_step
        ; optim_step_name tconcat_nil_step
        ; optim_step_name tmap_sigma_fusion_samevar_step
        ; optim_step_name tproject_nil_step
        ; optim_step_name tproject_over_const_step
        ; optim_step_name tproject_over_rec_step
        ; optim_step_name tproject_over_concat_r_step
        ; optim_step_name tproject_over_concat_l_step
        ; optim_step_name tproject_over_project_step
        ; optim_step_name tproject_over_either_step
      ].

    Remark nnrc_default_optim_list_all_valid {fruntime:foreign_runtime}
      : valid_optims tnnrc_optim_list nnrc_default_optim_list = (nnrc_default_optim_list,nil).
    Proof.
      vm_compute; trivial.
    Qed.

    Definition default_nnrc_optim_phases {fruntime:foreign_runtime} :=
      ("[nnrc] default"%string,nnrc_default_optim_list,10)::nil.

  End default.

  (* Java equivalent: NnrcOptimizer.trew *)
  Definition nnrc_optim_top_default
             {fruntime:foreign_runtime} {logger:optimizer_logger string nnrc}
    := nnrc_optim_top default_nnrc_optim_phases.

  Lemma nnrc_optim_top_default_correct
        {model:basic_model} {logger:optimizer_logger string nnrc} p:
    tnnrc_rewrites_to p (nnrc_optim_top_default p).
  Proof.
    unfold nnrc_optim_top_default.
    apply nnrc_optim_top_correctness.
  Qed.

End NNRCOptimizer.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert


text:
Require Import Algebra.Semigroup.
Require Import Algebra.Group.
Require Import Algebra.AbelianGroup.

Section RingTheory.
Context {R: Set}(plus: R -> R -> R)(zero: R)(minus: R -> R)(mult: R -> R -> R).

Class Ring := {
  ring_plus_assoc: forall (a b c: R), plus (plus a b) c = plus a (plus b c);
  ring_plus_comm: forall (a b: R), plus a b = plus b a;
  ring_plus_ident: forall (a: R), plus a zero = a;
  ring_plus_inv: forall (a: R), plus a (minus a) = zero;
  ring_mult_assoc: forall (a b c: R), mult (mult a b) c = mult a (mult b c);
  ring_distrib_left: forall (a b c: R), mult a (plus b c) = plus (mult a b) (mult a c);
  ring_distrib_right: forall (a b c: R), mult (plus b c) a = plus (mult b a) (mult c a);
}.

Lemma ring_agroup_plus:
  Ring -> AbelianGroup plus zero minus.
Proof.
  intros Rring.
  constructor.
  { apply ring_plus_assoc. }
  { apply ring_plus_comm. }
  { apply ring_plus_ident. }
  { apply ring_plus_inv. }
Qed.

Lemma ring_semigroup_mult:
  Ring -> Semigroup mult.
Proof.
  intros Rring.
  constructor.
  apply ring_mult_assoc.
Qed.

Lemma agroup_plus_semigroup_mult_distrib_ring:
  AbelianGroup plus zero minus ->
  Semigroup mult ->
  (forall (a b c: R), mult a (plus b c) = plus (mult a b) (mult a c)) ->
  (forall (a b c: R), mult (plus b c) a = plus (mult b a) (mult c a)) ->
  Ring.
Proof.
  intros Ragroup_plus Rsemigrp_mult Hld Hrd.
  constructor;
    try assumption.
  { apply semigroup_assoc.
    apply (agroup_semigroup plus zero minus).
    assumption. }
  { apply (agroup_comm plus zero minus). }
  { apply (agroup_ident plus zero minus). }
  { apply (agroup_inv plus zero minus). }
  { apply semigroup_assoc.
    assumption. }
Qed.

Context `{Rring: Ring}.

Theorem ring_left_mult_zero (a: R):
  mult zero a = zero.
Proof.
  cut (AbelianGroup plus zero minus).
  { intros Ragroup_plus.
    cut (mult (plus zero zero) a = mult zero a).
    { intros H.
      rewrite ring_distrib_right in H.
      apply (agroup_idemp_zero plus zero minus) in H.
      assumption. }
    { rewrite ring_plus_ident.
      reflexivity. } }
  { apply ring_agroup_plus.
    assumption. }
Qed.

Theorem ring_right_mult_zero (a: R):
  mult a zero = zero.
Proof.
  cut (AbelianGroup plus zero minus).
  { intros Ragroup_plus.
    cut (mult a (plus zero zero) = mult a zero).
    { intros H.
      rewrite ring_distrib_left in H.
      apply (agroup_idemp_zero plus zero minus) in H.
      assumption. }
    { rewrite (agroup_ident plus zero minus zero).
      reflexivity. } }
  { apply ring_agroup_plus.
    assumption. }
Qed.

Theorem ring_mult_minus_left (a b: R):
  mult (minus a) b = minus (mult a b).
Proof.
  cut (AbelianGroup plus zero minus).
  { intros Ragroup_plus.
    apply (agroup_minus_unique plus zero minus);
    rewrite <- ring_distrib_right.
    rewrite (agroup_inv plus zero minus).
    apply ring_left_mult_zero. }
  { apply ring_agroup_plus.
    assumption. }
Qed.

Theorem ring_mult_minus_right (a b: R):
  mult a (minus b) = minus (mult a b).
Proof.
  cut (AbelianGroup plus zero minus).
  { intros Ragroup_plus.
    apply (agroup_minus_unique plus zero minus);
      rewrite <- ring_distrib_left.
    rewrite (agroup_inv plus zero minus).
    apply ring_right_mult_zero. }
  { apply ring_agroup_plus.
    assumption. }
Qed.

Theorem ring_mult_minus_minus (a b: R):
  mult (minus a) (minus b) = mult a b.
Proof.
  cut (AbelianGroup plus zero minus).
  { intros Ragroup_plus.
    rewrite ring_mult_minus_left.
    rewrite ring_mult_minus_right.
    apply (agroup_minus_involute plus zero minus). }
  { apply ring_agroup_plus.
    assumption. }
Qed.
End RingTheory.

author: ku-sldg

repo: algebra

save_path: github-repos/coq/ku-sldg-algebra


text:
Set Implicit Arguments.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Lists.ListSet.
Require Import Coq.Bool.Bool.
Require Import EqNat.
Require Import Coq.Init.Logic.
Require Import Coq.Program.Equality.
Require Import MyBase.
Require Import lang.
Require Import hoas.
Require Import static_semantics.
Require Import dynamic_semantics.

Inductive SubContext : ℾ -> ℾ -> Prop :=
| SubIntro {Γ1 Γ2} : (forall {s τ}, s ∷ τ ∈ Γ1 -> s ∷ τ ∈ Γ2) -> SubContext Γ1 Γ2
| SubCons s τ {Γ1 Γ2} : SubContext Γ1 Γ2 -> SubContext (ConsEnv s τ Γ1) (ConsEnv s τ Γ2)
| SubShadow {Γ1 Γ2} Γ' : SubContext Γ1 Γ2 -> SubContext (ShadowEnv Γ1 Γ') (ShadowEnv Γ2 Γ').

Lemma InterpretSubContext {Γ1 Γ2} : SubContext Γ1 Γ2 -> forall {s τ}, s ∷ τ ∈ Γ1 -> s ∷ τ ∈ Γ2.
  intros H s τ H0.
  induction H.
  - apply (H s τ).
    assumption.
  - destruct (string_dec s s0) as [-> | neq].
    + rewrite (InContextUnique H0 (InConsEnv)).
      constructor.
    + inversion H0.
      * congruence.
      * specialize (IHSubContext inSub).
        done.
  - inversion H0.
    + done.
    + specialize (IHSubContext inLeft).
      done.
Qed.

Lemma SubContextRefl Γ : SubContext Γ Γ.
  enough (forall s τ, s ∷ τ ∈ Γ -> s ∷ τ ∈ Γ).
  done.
  trivial.
Qed.

Lemma SubContextTrans {Γ1 Γ2 Γ3} : SubContext Γ1 Γ2 -> SubContext Γ2 Γ3 -> SubContext Γ1 Γ3.
  intros H H0.
  constructor.
  intros s τ H1.
  apply (InterpretSubContext H0).
  apply (InterpretSubContext H).
  assumption.
Qed.

Lemma SubEquiv {Γ1 Γ2} : EquivContext Γ1 Γ2 <-> (SubContext Γ1 Γ2 /\ SubContext Γ2 Γ1).
  split.
  - intros H.
    split.
    + apply SubIntro.
      intros s τ H0.
      rewrite <- (InterpretEquivContext H).
      assumption.
    + apply SubIntro.
      intros s τ H0.
      rewrite (InterpretEquivContext H).
      assumption.
  - intros (ab, ba).
    apply EquivIntro.
    intros s τ.
    split.
    + exact (InterpretSubContext ab).
    + exact (InterpretSubContext ba).
Qed.

Notation "a ⊆ b" := (SubContext a b) (at level 1, b at next level).

Lemma SubContextConsRight {Γ1 Γ2} : Γ1 ⊆ Γ2 -> forall x τ, x ∉ Γ1 -> Γ1 ⊆ (ConsEnv x τ Γ2).
  intros H x τ H0.
  apply SubIntro.
  intros s τ0 H1.
  destruct (string_dec s x) as [-> | neq].
  - destruct (InContextInverse H1 H0).
  - pose (InterpretSubContext H H1).
    done.
Qed.

Lemma Strengthening {s e} (notInFV : s ∉f e) : forall {Γ τ' τ} (typechecks1 : (ConsEnv s τ' Γ) ⊢ e ∷ τ), Γ ⊢ e ∷ τ.
  induction notInFV; intros Γ τ' τ'' typechecks1.
  - inversion typechecks1.
    subst.
    constructor.
    refine (InSubConsEnvInversion _ H1).
    congruence.
  - inversion typechecks1.
    subst.
    constructor.
  - inversion typechecks1.
    subst.
    constructor.
    + eapply IHnotInFV1; done.
    + eapply IHnotInFV2; done.
  - inversion typechecks1.
    subst.
    econstructor.
    + eapply IHnotInFV1; done.
    + eapply IHnotInFV2; done.
  - inversion typechecks1.
    subst.
    constructor.
    assumption.
    eapply IHnotInFV.
    enough (EquivContext (ConsEnv x τ (ConsEnv f (τ → τ'0) (ConsEnv s τ' Γ)))
                         (ConsEnv s τ' (ConsEnv x τ (ConsEnv f (τ → τ'0) Γ)))).
    exact (EquivContextAlsoTypechecks type1 H).
    pose (EquivContextReorder (EquivContextRefl (ConsEnv f (τ → τ'0) Γ)) notX τ τ').
    pose (EquivCons x τ (EquivContextReorder (EquivContextRefl Γ) notF (AbsType τ τ'0) τ')).
    exact (EquivContextTrans e0 e).
  - inversion typechecks1.
    subst.
    constructor.
    assumption.
    enough (EquivContext (ConsEnv x τ (ConsEnv f (τ → τ'0) (ConsEnv x τ' Γ))) (ConsEnv x τ (ConsEnv f (τ → τ'0) Γ))).
    exact (EquivContextAlsoTypechecks type1 H).
    pose (EquivCons x τ (EquivContextReorder (EquivContextRefl Γ) nefx (AbsType τ τ'0) τ')).
    pose (EquivContextDoubleElim (ConsEnv f (τ → τ'0) Γ) x τ τ').
    exact (EquivContextTrans e e0).
  - inversion typechecks1.
    subst.
    constructor.
    assumption.
    enough (EquivContext (ConsEnv x τ (ConsEnv f (τ → τ'0) (ConsEnv f τ' Γ))) (ConsEnv x τ (ConsEnv f (τ → τ'0) Γ))).
    exact (EquivContextAlsoTypechecks type1 H).
    exact (EquivCons x τ (EquivContextDoubleElim Γ f (AbsType τ τ'0) τ')).
Qed.

Lemma Weakening {Γ e τ} (typchecks1 : Γ ⊢ e ∷ τ) :
  forall {Γ'}, Γ ⊆ Γ' -> Γ' ⊢ e ∷ τ.
Proof with done.
  induction typchecks1; intros Γ'' Γ''sub.
  - done.
  - refine (VSE (InterpretSubContext Γ''sub _))...
  - refine (ASE (IHtypchecks1_1 _ _)
                (IHtypchecks1_2 _ _))...
  - refine (PSE (IHtypchecks1_1 _ _)
                (IHtypchecks1_2 _ _))...
  - specialize (IHtypchecks1 (ConsEnv x τ (ConsEnv f (τ → τ') Γ''))
                             (SubCons x τ (SubCons f (τ → τ') Γ''sub)))...
Qed.

Lemma OtherWeakening {s e} (sNotIn : s ∉f e) : forall {Γ τ} (typechecks1 : Γ ⊢ e ∷ τ) {τ'}, (ConsEnv s τ' Γ) ⊢ e ∷ τ.
Proof with done.
  induction sNotIn; intros Γ τ'' typechecks1 τ'; inv typechecks1; econstructor; subst.
  - refine (InSubConsEnv _ _)...
  - eapply IHsNotIn1...
  - eapply IHsNotIn2...
  - eapply IHsNotIn1...
  - eapply IHsNotIn2...
  - assumption.
  - specialize (IHsNotIn (ConsEnv x τ (ConsEnv f (τ → τ'0) Γ)) τ'0 type1 τ').
    apply (EquivContextAlsoTypechecks IHsNotIn).
    pose (EquivContextReorder (EquivContextRefl (ConsEnv f (τ → τ'0) Γ)) notX τ τ').
    pose (EquivCons x τ (EquivContextReorder (EquivContextRefl Γ) notF (AbsType τ τ'0) τ')).
    exact (EquivContextSymm (EquivContextTrans e0 e)).
  - assumption.
  - refine (EquivContextAlsoTypechecks type1 _).
    pose (EquivCons x τ (EquivContextReorder (EquivContextRefl Γ) nefx (AbsType τ τ'0) τ')).
    pose (EquivContextDoubleElim (ConsEnv f (τ → τ'0) Γ) x τ τ').
    exact (EquivContextSymm (EquivContextTrans e e0)).
  - assumption.
  - refine (EquivContextAlsoTypechecks type1 _).
    exact (EquivContextSymm (EquivCons x τ (EquivContextDoubleElim Γ f (AbsType τ τ'0) τ'))).
Qed.

Reserved Notation "a ≡ b % c" (at level 1, b at next level).

Inductive ContextCongruenceModuloS : ℾ -> ℾ -> string -> Prop :=
| CongModIntro Γ1 Γ2 s :
    (forall s' τ, (s=s') \/ (s' ∷ τ ∈ Γ1 <-> s' ∷ τ ∈ Γ2)) ->
    (Γ1 ≡ Γ2 % s)
| CongModCons {Γ1 Γ2 s s' τ} : Γ1 ≡ Γ2 % s -> (ConsEnv s' τ Γ1) ≡ (ConsEnv s' τ Γ2) % s
| CongModShad {Γ1 Γ2 Γ' s} : Γ1 ≡ Γ2 % s -> (ShadowEnv Γ1 Γ') ≡ (ShadowEnv Γ2 Γ') % s
where "a ≡ b % c" := (ContextCongruenceModuloS a b c).

Lemma CongModRefl Γ s : Γ ≡ Γ % s.
  apply CongModIntro.
  intros s' τ.
  right.
  reflexivity.
Qed.

Lemma InterpretCongMod' {Γ1 Γ2 s}
  : Γ1 ≡ Γ2 % s -> forall s' τ, (s=s') \/ (s' ∷ τ ∈ Γ1 <-> s' ∷ τ ∈ Γ2).
  intros H s' τ.
  induction H.
  - exact (H s' τ).
  - decompose [or] IHContextCongruenceModuloS.
    + done.
    + right.
      destruct H0.
      split; inversion 1; done.
  - decompose [or] IHContextCongruenceModuloS.
    + done.
    + right.
      destruct H0.
      split; inversion 1; done.
Qed.

Lemma InterpretCongMod {Γ1 Γ2 s}
  : Γ1 ≡ Γ2 % s -> forall {s' τ}, s<>s' -> (s' ∷ τ ∈ Γ1 <-> s' ∷ τ ∈ Γ2).
  intros H s' τ H0.
  destruct (InterpretCongMod' H s' τ); done.
Qed.

Lemma CongModSymm {Γ1 Γ2 s} : Γ1 ≡ Γ2 % s -> Γ2 ≡ Γ1 % s.
  intros H.
  eapply CongModIntro.
  intros s' τ.
  destruct (string_dec s s') as [-> | neq].
  - done.
  - right.
    symmetry.
    apply (InterpretCongMod H neq).
Qed.

Lemma CongModToEquiv {Γ1 Γ2 s} : Γ1 ≡ Γ2 % s -> forall τ, (EquivContext (ConsEnv s τ Γ1) (ConsEnv s τ Γ2)).
  intros H τ.
  eapply EquivIntro.
  intros s0 τ0.
  epose (InterpretCongMod' H).
  - destruct (string_dec s s0) as [-> | neq].
    + split; intros H'; inversion H'; done.
    + destruct (o s0 τ0) as [-> | equiv].
      contradiction.
      split; intros H'; inversion H'; done.
Qed.

Lemma CongModConsLeft {x τ Γ1 Γ2} : Γ1 ≡ Γ2 % x -> (ConsEnv x τ Γ1) ≡ Γ2 % x.
  intros H.
  eapply CongModIntro.
  intros s' τ0.
  destruct (string_dec s' x) as [-> | neq].
  - done.
  - right.
    split.
    + intros H0.
      pose (InSubConsEnvInversion neq H0).
      eapply InterpretCongMod.
      eapply CongModSymm.
      exact H.
      congruence.
      eapply InSubConsEnvInversion.
      exact neq.
      exact H0.
    + intros H0.
      eapply InSubConsEnv.
      done.
      enough (x <> s').
      rewrite (InterpretCongMod H H1).
      done.
      congruence.
Qed.

Lemma Substitution {e1 Γ1 τ1} (typechks1 : Γ1 ⊢ e1 ∷ τ1) : forall e2 e3 Γ2 τ2 s,
  (s ∷ τ2 ∈ Γ1) ->
  Γ2 ⊢ e2 ∷ τ2 ->
  Γ1 ≡ Γ2 % s ->
  [e2 / s] e1 = e3 ->
  Γ2 ⊢ e3 ∷ τ1.
Proof with done.
  intros e2 e3 Γ2 τ2 s H H0 H1 H2.
  dependent induction typechks1.
  - inversion H2...
  - inversion H3.
    subst.
    rewrite (InContextUnique H H0)...
    rewrite (InterpretCongMod H2 neq) in H...
  - inversion H2.
    subst.
    constructor.
    + eapply IHtypechks1_1.
      exact H.
      exact H0.
      exact H1.
      exact LeftAddCAS.
    + eapply IHtypechks1_2.
      exact H.
      exact H0.
      exact H1.
      exact RightAddCAS.
  - inversion H2.
    subst.
    eapply PSE.
    + eapply IHtypechks1_1.
      exact H.
      exact H0.
      exact H1.
      exact LeftAppCAS.
    + eapply IHtypechks1_2.
      exact H.
      exact H0.
      exact H1.
      exact RightAppCAS.
  - inversion H2.
    subst.
    + eapply BSE.
      assumption.
      eapply IHtypechks1.
      * exact (InSubConsEnv notX (InSubConsEnv notF H)).
      * eapply (OtherWeakening _).
        eapply (OtherWeakening _).
        eassumption.
      * exact (CongModCons (CongModCons H1)).
      * assumption.
    + subst.
      eapply BSE.
      assumption.
      pose (EquivCons x τ (CongModToEquiv H1 (τ → τ'))).
      refine (EquivContextAlsoTypechecks _ _).
      exact typechks1.
      exact e.
    + subst.
      eapply BSE.
      assumption.
      pose (@CongModCons _ _ _ f (τ → τ') H1).
      pose (CongModToEquiv c τ).
      refine (EquivContextAlsoTypechecks _ _).
      exact typechks1.
      exact e.
      Unshelve.
      assumption.
      assumption.
Qed.

Lemma CannonicalForms {e τ} :
  NullEnv ⊢ e ∷ τ -> (𝕍 e) ->
  match τ with
  | NatType => exists n, e = (NatExpr n)
  | (AbsType τ1 τ2) => exists f x body, f<>x /\ (e = (AbsExpr f x τ1 body))
  end.
  intros H H0.
  destruct H.
  - exists n; done.
  - inversion H0.
  - inversion H0.
  - inversion H0.
  - exists f.
    exists x.
    exists body.
    done.
Qed.

Lemma TypedEvalContextInversion {Γ E τ0 τ} (Etype : Γ ⊢ E [τ0] ∷ τ)
  : exists x e, x ∉ Γ /\ EvaluationContextFillsTo E x e /\ (ConsEnv x τ0 Γ) ⊢ e ∷ τ.
  destruct Etype.
  - destruct (ContextFinite Γ).
    exists x.
    exists x.
    done.
  - exists x.
    exists (AddExpr e1 e2).
    epose (Weakening H (SubContextConsRight (SubContextRefl Γ) τ H0)).
    done.
  - exists x.
    exists (AddExpr n e).
    done.
  - exists x.
    exists (AppExpr e1 e2).
    epose (Weakening H (SubContextConsRight (SubContextRefl Γ) τ H0)).
    done.
  - exists x.
    exists (AppExpr (AbsExpr fn arg τarg body) e).
    epose (Weakening H (SubContextConsRight (SubContextRefl Γ) τ H0)).
    done.
Qed.

Lemma DecompositionOfTypes {E} : forall {e0 e1 Γ τ},
    EvaluationContextFillsTo E e0 e1 -> Γ ⊢ e1 ∷ τ -> exists τ1, Γ ⊢ e0 ∷ τ1 /\ Γ ⊢ E [τ1] ∷ τ.
  induction E; intros e0 e1 Γ τ' H H0.
  all:inversion H; subst.
  exists τ'; done.
  all:inversion H0; subst.
  - destruct (IHE e0 e1' Γ NatType subFills type1) as (τ1, (typ1, typ2)).
    exists τ1.
    destruct (TypedEvalContextInversion typ2) as (x, (e2, (notIn, (fills, typ3)))).
    done.
  - destruct (IHE e0 e2' Γ NatType subFills type2) as (τ1, (typ1, typ2)).
    exists τ1.
    destruct (TypedEvalContextInversion typ2) as (x, (e2, (notIn, (fills, typ3)))).
    done.
  - destruct (IHE e0 e1' Γ (AbsType τ1 τ') subFills type1) as (τ2, (typ1, typ2)).
    exists τ2.
    destruct (TypedEvalContextInversion typ2) as (x, (e2, (notIn, (fills, typ3)))).
    done.
  - inversion type1.
    destruct (IHE e0 e2' Γ τ1 subFills type2) as (τ2, (typ1, typ2)).
    exists τ2.
    destruct (TypedEvalContextInversion typ2) as (s, (e2, (notIn, (fills, typ3)))).
    done.
Qed.

Definition CanStep e := exists e', e ⥛ e'.
Definition NotStuck e := 𝕍 e \/ (CanStep e).

Lemma Progress {e} : forall {τ} (etyp: NullEnv ⊢ e ∷ τ), (NotStuck e).
  induction e.
  - intros; subst.
    inversion etyp.
    inversion H1.
  - left; now constructor.
  - intros τ etyp.
    inversion etyp.
    right.
    subst.
    specialize (IHe1 _ type1).
    specialize (IHe2 _ type2).
    destruct IHe1 as [ ve1 | se1 ].
    + destruct (CannonicalForms type1 ve1).
      subst.
      destruct IHe2 as [ ve2 | se2 ].
      * destruct (CannonicalForms type2 ve2).
        exists (NatExpr (x + x0)).
        done.
      * inversion se2.
        inversion H.
        done.
    + inversion se1.
      inversion H.
      exists (AddExpr x e2).
      done.
  - done.
  - intros τ etyp.
    inversion etyp.
    subst.
    specialize (IHe1 _ type1).
    specialize (IHe2 _ type2).
    right.
    destruct IHe1 as [ ve1 | se1 ].
    + destruct (CannonicalForms type1 ve1) as (f1, (x1, (body1, (ne1, eq1)))).
      subst.
      * inversion type1.
        subst.
        destruct IHe2 as [ ve2 | se2 ].
        -- destruct (@CASAlways e2 x1 body1) as (body2, cas1).
           apply AlwaysSafeToSubInto.
           destruct (@CASAlways (AbsExpr f1 x1 τ1 body1) f1 body2) as (body3, cas2).
           apply AlwaysSafeToSubInto.
           exists body3.
           done.
        -- inversion se2.
           inversion H.
           subst.
           exists (AppExpr (AbsExpr f1 x1 τ1 body1) x).
           done.
    + inversion se1.
      inversion H.
      exists (AppExpr x e2).
      done.
Qed.

Lemma βPreservation {e e'} (estep : e ⥛β e') : forall τ (etyp : NullEnv ⊢ e ∷ τ),  NullEnv ⊢ e' ∷ τ.
  induction estep; intros τ0 etyp; inversion etyp.
  - done.
  - subst.
    inversion type1.
    subst.
    eapply Substitution.
    + eapply Substitution.
      * exact type0.
      * apply InConsEnv.
      * eapply Weakening.
        exact type2.
        eapply SubContextConsRight.
        apply SubContextRefl.
        apply (@NotInNullEnv f).
      * eapply CongModConsLeft.
        apply CongModRefl.
      * exact CASx.
    + apply InConsEnv.
    + exact type1.
    + eapply CongModConsLeft.
      apply CongModRefl.
    + exact CASf.
Qed.

Lemma Preservation {e e'} (estep : e ⥛ e') : forall τ (etyp : NullEnv ⊢ e ∷ τ),  NullEnv ⊢ e' ∷ τ.
  intros τ etyp.
  inversion estep.
  subst.
  destruct (DecompositionOfTypes fillse1 etyp) as (τn, (typee1, ?)).
  pose (typee2 := βPreservation betaStep typee1).
  eapply InterpretTypedEvalContext.
  exact H.
  exact typee2.
  exact fillse2.
Qed.

Lemma Safety {e τ} (etyp : NullEnv ⊢ e ∷ τ) {e'} (estep : e ⥛* e') : (NotStuck e').
  induction estep.
  - now apply (Progress etyp).
  - apply (IHestep (Preservation ess etyp)).
Qed.

repo: STLC-coq


text:
Require Import Coq.Program.Basics.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Combinators.
Require Import Setoid.

Require Import Lists.List.
Import ListNotations.

Require Import FinProof.Common.
Require Import FinProof.CommonInstances.
Require Import FinProof.CommonProofs.
Require Import ZArith.
Require Import Psatz.

Require Import depoolContract.SolidityNotations.
Require Import depoolContract.ProofEnvironment.
Require Import depoolContract.Lib.Tactics.
Require Import depoolContract.Lib.CommonCommon.

(* Module SolidityNotations := SolidityNotations XTypesSig StateMonadSig. *)
Import SolidityNotations.
Import List.

Local Open Scope solidity_scope.
Local Open Scope list_scope.
Local Open Scope Z_scope.

Set Typeclasses Iterative Deepening.

Set Typeclasses Depth 100.

Fixpoint toUniqueArray {X} (eqX: X -> X -> bool) (l: list X) (m: listPair Z X) : listPair Z X :=
match l with
| nil => m
| x::xs => if (bIn eqX x (xHMapElems m)) then (toUniqueArray eqX xs m) else
                                              (toUniqueArray eqX xs (hmapPush x m))
end.

Lemma toUniqueArrayFalse_helper1: forall X (H: XBoolEquable bool X)  (x0: listPair Z X) a,
boolEquivalence eqb ->
hmapFindWithDefault false (@eqb bool X H) a
       (List.map (fun p : Z * X => (snd p, true)) x0) = false ->
bIn eqb a (List.map snd x0) = false.
Proof.
 intros. induction x0.
 simpl. auto.
 simpl. simpl in H1.
 unfold hmapFindWithDefault in H1.
 unfold hmapLookup in H1. simpl in H1.
 remember (eqb (snd a0) a).
 replace (eqb a (snd a0)) with y in H1.
 destruct y. simpl in H0. inversion H1.
 replace (bIn eqb a (List.map snd x0)) with false.
 auto. symmetry. apply IHx0.
 apply H1. rewrite Heqy. apply boolEqSym. auto.
Qed.

Lemma toUniqueArrayTrue_helper1: forall X (H: XBoolEquable bool X)  (x0: listPair Z X) a,
boolEquivalence eqb ->
hmapFindWithDefault false (@eqb bool X H) a
       (List.map (fun p : Z * X => (snd p, true)) x0) = true ->
bIn eqb a (List.map snd x0) = true.
Proof.
 intros. induction x0.
 simpl in H1. inversion H1.
 simpl. simpl in H1.
 unfold hmapFindWithDefault in H1.
 unfold hmapLookup in H1. simpl in H1.
 remember (eqb (snd a0) a).
 replace (eqb a (snd a0)) with y in H1.
 destruct y. simpl in H1. auto.
 rewrite IHx0. auto. auto. rewrite Heqy.
 apply boolEqSym. auto.
Qed.

Lemma toUniqueArrayFalse_helper2: forall X (H:XBoolEquable bool X)  x0 a,
bIn eqb a (List.map snd x0) = false ->
hmapIsMember Z.eqb (Z.of_nat (Datatypes.length x0)) x0 = false ->
(List.map (fun p : Z * X => (snd p, true)) x0) [a]← true =
List.map (fun p : Z * X => (snd p, true)) (hmapInsert Z.eqb (xHMapSize x0) a x0).
Proof.
 intros. unfold hmapInsert.
 simpl.
 replace (bIn eqb a (map fst (map (fun p : Z * X => (snd p, true)) x0))) with false.
 replace (bIn Z.eqb (Z.of_nat (Datatypes.length x0)) (map fst x0)) with false.
 unfold Datatypes.id. simpl. auto.
 symmetry.
 replace (List.map fst (List.map (fun p : Z * X => (snd p, true)) x0)) with (List.map snd x0).
 auto.
 generalize x0. intros. induction x1.
 simpl. auto.
 simpl. rewrite IHx1. auto.
Qed.

Lemma toUniqueArrayFalse_helper3: forall X (x0: listPair Z X) a0,
(forall z, z >= (Z.of_nat (Datatypes.length x0)) ->
                        hmapIsMember Z.eqb z x0 = false) ->
hmapIsMember Z.eqb (Z.of_nat (Datatypes.length (hmapPush a0 x0))) (hmapPush a0 x0) = false.
Proof.
 intros. unfold hmapIsMember.
 unfold hmapIsMember in H.
 remember (Z.of_nat (Datatypes.length x0)).
 remember (Z.of_nat (Datatypes.length (hmapPush a0 x0))).
 assert (z0 >= z).
 rewrite Heqz. rewrite Heqz0. apply hmapSizePush.
 apply H in H0.
 unfold hmapPush. unfold hmapInsert.
 replace (hmapIsMember xIntEqb (xHMapSize x0) x0) with false.
 simpl. rewrite <- Heqz.
 unfold  Datatypes.id.
 replace (z =? z0) with false.
 replace (bIn Z.eqb z0 (List.map fst x0)) with false.
 auto. symmetry. rewrite Heqz.
 rewrite Heqz0.
 unfold hmapPush. unfold hmapInsert.
 replace (hmapIsMember xIntEqb (xHMapSize x0) x0) with false.
 simpl.  unfold Datatypes.id.
 remember (Datatypes.length x0).
 apply Z.eqb_neq. rewrite Zpos_P_of_succ_nat. lia.
 symmetry. unfold hmapIsMember. apply H.
 rewrite Heqz. simpl. lia. symmetry. unfold hmapIsMember. apply H.
 rewrite Heqz. simpl. lia.
Qed.

Lemma toUniqueArrayFalse_helper3': forall X (x0: listPair Z X) a0 z,
(forall z, z >= (Z.of_nat (Datatypes.length x0)) ->
                        hmapIsMember Z.eqb z x0 = false) ->
z >= Z.of_nat (Datatypes.length (hmapPush a0 x0)) ->
hmapIsMember Z.eqb z (hmapPush a0 x0) = false.
Proof.
 intros. unfold hmapIsMember.
 unfold hmapIsMember in H.
 remember (Z.of_nat (Datatypes.length x0)).
 remember (Z.of_nat (Datatypes.length (hmapPush a0 x0))).
 assert (z1 >= z0).
 rewrite Heqz1. rewrite Heqz0. apply hmapSizePush.
 apply H in H1.
 unfold hmapPush. unfold hmapInsert.
 replace (hmapIsMember xIntEqb (xHMapSize x0) x0) with false.
 simpl. rewrite <- Heqz0.
 unfold  Datatypes.id.
 replace (z0 =? z) with false.
 replace (bIn Z.eqb z (List.map fst x0)) with false.
 auto. symmetry. apply H.
 rewrite Heqz0. apply Zge_trans with (m:=z1). auto.
 rewrite Heqz1.
 unfold hmapPush. unfold hmapInsert.
 replace (hmapIsMember xIntEqb (xHMapSize x0) x0) with false.
 simpl.  unfold Datatypes.id.
 remember (Datatypes.length x0).
 rewrite Zpos_P_of_succ_nat. lia.
 symmetry. unfold hmapIsMember. apply H.
 rewrite Heqz0. simpl. lia.
 symmetry.  apply Z.eqb_neq.
 assert (z1 = z0 + 1).
 rewrite Heqz1. rewrite Heqz0.
 unfold hmapPush.
 unfold hmapInsert. replace (hmapIsMember xIntEqb (xHMapSize x0) x0) with false.
 simpl. simpl. unfold Datatypes.id. remember (Datatypes.length x0).
 rewrite Zpos_P_of_succ_nat. lia.
 symmetry. unfold hmapIsMember. apply H.
 rewrite Heqz0. simpl. lia.
 lia. symmetry. unfold hmapIsMember. apply H.
 rewrite Heqz0. simpl. lia.
Qed.

Lemma toUniqueArrayFalse: forall {X}`{XBoolEquable bool X}
(l: list X) x0 (a: X),
boolEquivalence eqb ->
(forall z, z >= (Z.of_nat (Datatypes.length x0)) ->
                        hmapIsMember Z.eqb z x0 = false) ->
(List.map (fun p => (snd p, true))
        (toUniqueArray eqb l x0)) [a] = false ->
hmapInsert eqb a true
  (List.map (fun p => (snd p, true)) (toUniqueArray eqb l x0)) =
List.map (fun p => (snd p, true))
  (toUniqueArray eqb (l ++ [a]) x0).
Proof.
 intros. generalize dependent x0. induction l; intros.
 simpl. simpl in H2.
 remember (bIn eqb a (List.map snd x0)).
 destruct b. apply toUniqueArrayFalse_helper1 in H2.
 congruence. auto.
 apply toUniqueArrayFalse_helper1 in H2.
 unfold hmapPush.
 setoid_rewrite toUniqueArrayFalse_helper2. auto. auto.
 apply H1. lia. auto.
 simpl.
 remember (bIn eqb a0 (List.map snd x0)).
 destruct b. apply IHl. auto.
 simpl in H2. rewrite <- Heqb in H2. auto.
 apply IHl. intros. apply toUniqueArrayFalse_helper3'.
 intros. apply H1. auto. auto.
 simpl in H2. rewrite <- Heqb in H2.
 apply H2.
Qed.

Lemma toUniqueArrayTrue: forall {X}`{XBoolEquable bool X}
(l: list X) x0 (a: X),
boolEquivalence eqb ->
(forall z, z >= (Z.of_nat (Datatypes.length x0)) ->
                        hmapIsMember Z.eqb z x0 = false) ->
(List.map (fun p => (snd p, true))
        (toUniqueArray eqb l x0)) [a] = true ->
List.map (fun p => (snd p, true))
  (toUniqueArray eqb l x0) =
List.map (fun p => (snd p, true))
  (toUniqueArray eqb (l ++ [a]) x0).
Proof.
 intros. generalize dependent x0. induction l; intros.
 simpl. simpl in H2.
 remember (bIn eqb a (List.map snd x0)).
 destruct b. auto. apply toUniqueArrayTrue_helper1 in H2.
 congruence. auto.
 simpl in H2. simpl. remember (bIn eqb a0 (List.map snd x0)).
 destruct b. apply IHl. auto.
 auto. apply IHl.
 intros. unfold hmapPush.
 apply toUniqueArrayFalse_helper3'. intros.
 apply H1. auto. auto. auto.
Qed.

Lemma toUniqueArrayFalse2: forall {X}`{XBoolEquable bool X}
(l: list X) x0 (a: X),
boolEquivalence eqb ->
(List.map (fun p => (snd p, true))
        (toUniqueArray eqb l x0)) [a] = false ->
hmapInsert Z.eqb
  (Z.of_nat (Datatypes.length (toUniqueArray eqb l x0))) a
  (toUniqueArray eqb l x0) =
toUniqueArray eqb (l ++ [a]) x0.
Proof.
 intros. generalize dependent x0. induction l; intros.
 simpl in H1. simpl. remember (bIn eqb a (List.map snd x0)).
 destruct b. apply toUniqueArrayFalse_helper1 in H1.
 congruence. auto.
 apply toUniqueArrayFalse_helper1 in H1.
 unfold hmapPush. auto. auto.
 simpl. simpl in H1.
 remember (bIn eqb a0 (List.map snd x0)).
 destruct b. apply IHl.  auto.
 apply IHl. auto.
Qed.

Lemma toUniqueArrayTrue2: forall {X}`{XBoolEquable bool X}
(l: list X) x0 (a: X),
boolEquivalence eqb ->
(List.map (fun p => (snd p, true))
          (toUniqueArray eqb l x0)) [a] = true ->
toUniqueArray eqb l x0 =
toUniqueArray eqb (l ++ [a]) x0.
Proof.
 intros. generalize dependent x0. induction l; intros.
 simpl. simpl in H1. apply toUniqueArrayTrue_helper1 in H1.
 rewrite H1. auto. auto.
 simpl. simpl in H1. remember (bIn eqb a0 (List.map snd x0)).
 destruct b. apply IHl. auto.
 apply IHl. auto.
Qed.

Lemma toUniqueArrayFalse3: forall {X}`{XBoolEquable bool X}
(l: list X) x0 (a: X),
boolEquivalence eqb ->
(forall z, z >= (Z.of_nat (Datatypes.length x0)) ->
                        hmapIsMember Z.eqb z x0 = false) ->
(List.map (fun p => (snd p, true))
        (toUniqueArray eqb l x0)) [a] = false ->
Z.of_nat (Datatypes.length (toUniqueArray eqb l x0)) + 1 =
Z.of_nat (Datatypes.length (toUniqueArray eqb (l ++ [a]) x0)).
Proof.
 intros. generalize dependent x0. induction l; intros.
 simpl in H1. simpl. remember (bIn eqb a (List.map snd x0)).
 destruct b. apply toUniqueArrayFalse_helper1 in H2. simpl in H2.
 congruence. auto.
 apply toUniqueArrayFalse_helper1 in H2. simpl in H2.
 unfold hmapPush. unfold hmapInsert.
 replace (bIn Z.eqb (Z.of_nat (Datatypes.length x0)) (map fst x0)) with false.
 simpl. unfold Datatypes.id. remember (Datatypes.length x0).
 rewrite Zpos_P_of_succ_nat. lia.
 symmetry. apply H1. lia. auto.

 simpl. remember (bIn eqb a0 (List.map snd x0)).
 destruct b. apply IHl.  auto. simpl in H2.
 rewrite <- Heqb in H2. auto.
 apply IHl. intros.
 apply toUniqueArrayFalse_helper3'. intros.
 apply H1. auto. auto.
 simpl in H2. rewrite <- Heqb in H2.
 auto.
Qed.

Lemma toUniqueArrayTrue3: forall {X}`{XBoolEquable bool X}
(l: list X) x0 (a: X),
boolEquivalence eqb ->
(List.map (fun p => (snd p, true))
          (toUniqueArray eqb l x0)) [a] = true ->
Z.of_nat
  (Datatypes.length (toUniqueArray eqb l x0)) =
Z.of_nat
  (Datatypes.length
     (toUniqueArray eqb (l ++ [a]) x0)).
Proof.
 intros. generalize dependent x0. induction l; intros.
 simpl. simpl in H1. apply toUniqueArrayTrue_helper1 in H1.
 rewrite H1. auto. auto.
 simpl. simpl in H1.
 remember (bIn eqb a0 (List.map snd x0)).
 destruct b. apply IHl. auto. apply IHl.
 auto.
Qed.

author: Pruvendo


text:
From solutions Require Export language.

(** * Polymorphic, existential and recursive types in HeapLang *)
(** In order to define a type system for HeapLang (in the file [typed.v]), we
need to extend HeapLang with constructs for polymorphic functions (i.e.,
type-level lambdas and application), existential types (i.e., pack and
unpack), and iso-recursive types (i.e., fold and unfold). Since HeapLang is an
untyped language, it does natively have these constructs. *)

(** We retrofit type-level lambdas and application on HeapLang by defining them
as mere thunks, and ordinary application, respectively. This ensures that
polymorphic programs satisfy a **value restriction**, which is needed to obtain
type safety in the presence of mutable state. *)
Notation "Λ: e" := (λ: <>, e)%E (at level 200, only parsing) : expr_scope.
Notation "Λ: e" := (λ: <>, e)%V (at level 200, only parsing) : val_scope.
Notation "e '<_>'" := (App e%E #()) (at level 10, only parsing) : expr_scope.

(** We also use ordinary lambdas and application to retrofit [pack] and
[unpack] on HeapLang. This time we first define some helper functions so that
we can have a nice notation for these constructs. *)
Definition exist_pack : val := λ: "x", "x".
Definition exist_unpack : val := λ: "x" "y", "x" "y".

Notation "'pack:' e" := (exist_pack e%E)
  (at level 200, e at level 200,
   format "'[' 'pack:'  e ']'") : expr_scope.

Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (Lam x%binder e2%E) e1%E)
  (at level 200, x at level 1, e1, e2 at level 200,
   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (LamV x%binder e2%E) e1%E)
  (at level 200, x at level 1, e1, e2 at level 200,
   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : val_scope.

(** And we apply the trick one more to retrofit [fold] and [unfold] on
HeapLang. *)
Definition rec_fold : val := λ: "x", "x".
Definition rec_unfold : val := λ: "x", "x".

Notation "'fold:' e" := (rec_fold e%E)
  (at level 200, e at level 200,
   format "'[' 'fold:'  e ']'") : expr_scope.

Notation "'unfold:' e" := (rec_unfold e%E)
  (at level 200, e at level 200,
   format "'[' 'unfold:'  e ']'") : expr_scope.

(** ** Exercise (swap_poly, easy) *)
(** Below we define a polymorphic version of the [swap] function. *)
Definition swap_poly : val := Λ: λ: "l1" "l2",
  let: "x" := !"l1" in
  "l1" <- !"l2";;
  "l2" <- "x".

(** Prove the following specification. *)
Lemma wp_swap_poly `{!heapG Σ} l1 l2 v1 v2 :
  l1 ↦ v1 -∗
  l2 ↦ v2 -∗
  WP swap_poly <_> #l1 #l2 {{ v, ⌜ v = #() ⌝ ∗ l1 ↦ v2 ∗ l2 ↦ v1 }}.
(* SOLUTION *) Proof.
  iIntros "Hl1 Hl2".
  rewrite /swap_poly.
  do 2 wp_load.
  do 2 wp_store.
  by iFrame.
Qed.

author: DKXXXL