generated_proof_append.v 1000 Bytes
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
4
5
6
7
8
9
10
From refinedc.typing Require Import typing.
From refinedc.examples.talk_demo3 Require Import generated_code.
From refinedc.examples.talk_demo3 Require Import generated_spec.
Set Default Proof Using "Type".

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

  (* Typing proof for [append]. *)
11
12
13
  Lemma type_append (global_append : loc) :
    global_append ◁ᵥ global_append @ function_ptr type_of_append -
    typed_function (impl_append global_append) type_of_append.
Michael Sammler's avatar
Michael Sammler committed
14
  Proof.
15
    Open Scope printing_sugar.
Michael Sammler's avatar
Michael Sammler committed
16
    start_function "append" (p) => arg_l arg_k.
Michael Sammler's avatar
Michael Sammler committed
17
18
19
20
21
22
23
24
25
26
27
    split_blocks ((
      
    )%I : gmap label (iProp Σ)) ((
      
    )%I : gmap label (iProp Σ)).
    - repeat liRStep; liShow.
      all: print_typesystem_goal "append" "#0".
    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
    all: print_sidecondition_goal "append".
  Qed.
End proof_append.