Module Qcert.NNRC.Lang.NNRCSize

Require Import String.
Require Import Lia.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import DataRuntime.
Require Import cNNRC.
Require Import cNNRCShadow.

Section NNRCSize.
  Context {fruntime:foreign_runtime}.

  Fixpoint nnrc_size (n:nnrc) : nat
    := match n with
       | NNRCGetConstant v => 1
       | 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; lia.
Qed.

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.