Library zoo_std.int

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.int__code.
Require Import zoo_std.int__types.
Require Import zoo.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 Type 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 Type 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.

Require zoo_std.int__opaque.