NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library frag_list_max3

Require Import Max Omega List ZArith EqNat.
Require Import seplog.
Require Import expr_b_dp.
Require Import frag_list_triple.
Require Import frag_list_entail.

Import seplog_Z_m.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.assert_m.

Local Open Scope heap_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope frag_list_scope.

Local Close Scope Z_scope.

with bigtoe

Lemma max3_verif :
  {{{ (true_b, frag_list_entail.emp) }}}
  ifte (var_e 1 >>= var_e 2) thendo
    ifte (var_e 1 >>= var_e 3) thendo
      (0 <- var_e 1)
    elsedo
      (0 <- var_e 3)
  elsedo
    ifte (var_e 2 >>= var_e 3) thendo
      (0 <- var_e 2)
    elsedo
      (0 <- var_e 3)
  {{{ ((var_e 0 =e var_e 1) |e (var_e 0 =e var_e 2) |e (var_e 0 =e var_e 3), frag_list_entail.emp) }}}.
Proof.
eapply tritra_use.
simpl.
eapply refl_equal.
Tritra.
Qed.