generated_proof_compare_int.v 1020 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
From refinedc.typing Require Import typing.
From refinedc.examples.binary_search Require Import generated_code.
From refinedc.examples.binary_search Require Import generated_spec.
From refinedc.examples.binary_search Require Import binary_search_extra.
Set Default Proof Using "Type".

(* Generated from [examples/binary_search.c]. *)
Section proof_compare_int.
  Context `{!typeG Σ} `{!globalG Σ}.

  (* Typing proof for [compare_int]. *)
  Lemma type_compare_int :
     typed_function impl_compare_int type_of_compare_int.
  Proof.
    start_function "compare_int" ([[[x y] px] py]) => arg_x arg_y local_xi local_yi.
    split_blocks ((
      
    )%I : gmap label (iProp Σ)) ((
      
    )%I : gmap label (iProp Σ)).
    - repeat liRStep; liShow.
      all: print_typesystem_goal "compare_int" "#0".
    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
    all: print_sidecondition_goal "compare_int".
  Qed.
End proof_compare_int.