Library zoo_std.int

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base.
From zoo_std Require Export
  base
  int__code.
From zoo Require Import
  options.

Notation "e1 `min` e2" := (
  (Val int٠min) e1%E e2%E
)(at level 35
) : expr_scope.
Notation "e1 `max` e2" := (
  (Val int٠max) e1%E e2%E
)(at level 35
) : expr_scope.

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Section Z.
    Implicit Types n : Z.

    Lemma int٠min𑁒spec n1 n2 E Φ :
      ▷ Φ #(n1 `min` n2) -∗
      WP #n1 `min` #n2 @ E {{ Φ }}.
    #[global] Instance int٠min𑁒diaspec n1 n2 E :
      DIASPEC
      {{
        True
      }}
        #n1 `min` #n2 @ E
      {{
        RET #(n1 `min` n2);
        True
      }}
    | 30.

    Lemma int٠max𑁒spec n1 n2 E Φ :
      ▷ Φ #(n1 `max` n2) -∗
      WP #n1 `max` #n2 @ E {{ Φ }}.
    #[global] Instance int٠max𑁒diaspec n1 n2 E :
      DIASPEC
      {{
        True
      }}
        #n1 `max` #n2 @ E
      {{
        RET #(n1 `max` n2);
        True
      }}
    | 30.

    Lemma int٠positive_part𑁒spec n E Φ :
      ▷ Φ #₊n -∗
      WP int٠positive_part #n @ E {{ Φ }}.
    #[global] Instance int٠positive_part𑁒diaspec n E :
      DIASPEC
      {{
        True
      }}
        int٠positive_part #n @ E
      {{
        RET #₊n;
        True
      }}
    | 30.
  End Z.

  Section nat.
    Implicit Types n : nat.

    Lemma int٠min𑁒spec_nat n1 n2 E Φ :
      ▷ Φ #(n1 `min` n2)%nat -∗
      WP #n1 `min` #n2 @ E {{ Φ }}.
    #[global] Instance int٠min𑁒diaspec_nat n1 n2 E :
      DIASPEC
      {{
        True
      }}
        #n1 `min` #n2 @ E
      {{
        RET #(n1 `min` n2)%nat;
        True
      }}
    | 20.

    Lemma int٠max𑁒spec_nat n1 n2 E Φ :
      ▷ Φ #(n1 `max` n2)%nat -∗
      WP #n1 `max` #n2 @ E {{ Φ }}.
    #[global] Instance int٠max𑁒diaspec_nat n1 n2 E :
      DIASPEC
      {{
        True
      }}
        #n1 `max` #n2 @ E
      {{
        RET #(n1 `max` n2)%nat;
        True
      }}
    | 20.

    Lemma int٠positive_part𑁒spec_nat n E Φ :
      ▷ Φ #n -∗
      WP int٠positive_part #n @ E {{ Φ }}.
    #[global] Instance int٠positive_part𑁒diaspec_nat n E :
      DIASPEC
      {{
        True
      }}
        int٠positive_part #n @ E
      {{
        RET #n;
        True
      }}
    | 20.
  End nat.
End zoo_G.

From zoo_std Require
  int__opaque.