Module NNRCSize

Section NNRCSize.
  Require Import Omega.
  Require Import BasicRuntime cNNRC.

  Context {fruntime:foreign_runtime}.

  Fixpoint nnrc_size (n:nnrc) : nat
    := match n with
         | NNRCVar v => 1
         | NNRCConst d => 1
         | NNRCBinop op n₁ n₂ => S (nnrc_size n₁ + nnrc_size n₂)
         | NNRCUnop op n₁ => S (nnrc_size n₁)
         | NNRCLet v n₁ n₂ => S (nnrc_size n₁ + nnrc_size n₂)
         | NNRCFor v n₁ n₂ => S (nnrc_size n₁ + nnrc_size n₂)
         | NNRCIf n₁ n₂ n₃ => S (nnrc_size n₁ + nnrc_size n₂ + nnrc_size n₃)
         | NNRCEither nd vl nl vr nr => S (nnrc_size nd + nnrc_size nl + nnrc_size nr)
         | NNRCGroupBy g sl n => S (nnrc_size n)
       end.

  Lemma nnrc_size_nzero (n:nnrc) : nnrc_size n <> 0.

Proof.

induction n; simpl; omega.
Qed.

  Require Import cNNRCShadow.
  Require Import EquivDec Decidable.
  Require Import String.

  Lemma nnrc_rename_lazy_size n x1 x2:
    nnrc_size (nnrc_rename_lazy n x1 x2) = nnrc_size n.

Proof.

    nnrc_cases (induction n) Case;
    unfold nnrc_rename_lazy in *;
    simpl;
    destruct (equiv_dec x1 x2);
    simpl;
    try reflexivity;
    try solve [ rewrite IHn1;
                rewrite IHn2;
                rewrite IHn3;
                reflexivity ];
    try solve [ rewrite IHn1;
                rewrite IHn2;
                reflexivity ];
    try solve [ rewrite IHn;
                reflexivity ];
    try solve [ rewrite IHn1;
                destruct (equiv_dec v x1);
                simpl; try reflexivity;
                rewrite IHn2;
                reflexivity ].
    - Case "NNRCVar"%string.
      destruct (equiv_dec v x1);
        simpl; reflexivity.
    - Case "NNRCEither"%string.
      rewrite IHn1.
      destruct (equiv_dec v x1);
        destruct (equiv_dec v0 x1);
        simpl; try reflexivity.
      + rewrite IHn3.
        reflexivity.
      + rewrite IHn2.
        reflexivity.
      + rewrite IHn2.
        rewrite IHn3.
        reflexivity.
  Qed.

End NNRCSize.