Library init_spec
the tactic 'init_spec' is used to initialize the specifications
(pre-condition, post-condition, etc..) and the target code into a hoare triple.
Require Import include.
Require Import memory.
Require Import memdata.
Require Import assertion.
Require Import absop.
Require Import simulation.
Require Import language.
Require Import opsem.
Require Import os_program.
Require Import os_spec.
Require Import inferules.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import baseTac.
Require Import auxdef.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import derivedrules.
Require Import hoare_conseq.
Require Import symbolic_execution.
Require Import hoare_assign.
Require Import hoare_lemmas.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Require Import type_val_match.
Open Scope code_scope.
Fixpoint decllen (lst :decllist): nat :=
match lst with
| dnil => O
| dcons _ _ lst´ => S (decllen lst´)
end.
Lemma dl_vl_match_dv_same_length :
forall (dl:decllist) (vl: list val),
dl_vl_match dl vl = true -> decllen dl = length vl.
Lemma len_exist_0 :
forall (vl: list val),
length (rev vl) = 0%nat -> vl = nil.
Lemma len_exist_1 :
forall (vl: list val),
length (rev vl) = 1%nat ->
exists v1 , vl = v1 :: nil.
Lemma len_exist_2 :
forall (vl: list val),
length (rev vl) = 2%nat ->
exists v1 v2, vl = v1 :: v2 :: nil.
Lemma len_exist_3 :
forall (vl: list val),
length (rev vl) = 3%nat ->
exists v1 v2 v3, vl = v1 :: v2 :: v3 :: nil.
Lemma len_exist_4 :
forall (vl: list val),
length (rev vl) = 4%nat ->
exists v1 v2 v3 v4, vl = v1 :: v2 :: v3 :: v4 :: nil.
Lemma len_exist_5 :
forall (vl: list val),
length (rev vl) = 5%nat ->
exists v1 v2 v3 v4 v5, vl = v1 :: v2 :: v3 :: v4 :: v5 :: nil.
Lemma len_exist_6 :
forall (vl: list val),
length (rev vl) = 6%nat ->
exists v1 v2 v3 v4 v5 v6,
vl = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: nil.
Lemma dl_vl_match_0:
forall vl ,
dl_vl_match dnil (rev vl) = true -> vl = nil .
Lemma dl_vl_match_1:
forall vl x t ,
dl_vl_match (dcons x t dnil) (rev vl) = true ->
exists v, vl = v :: nil /\ type_val_match t v = true.
Lemma dl_vl_match_2:
forall vl x1 t1 x2 t2 ,
dl_vl_match ⌞x1 @ t1 ; x2 @ t2⌟ (rev vl) = true ->
exists v1 v2, vl = v1 :: v2 :: nil /\
type_val_match t2 v1 = true /\
type_val_match t1 v2 = true.
Lemma dl_vl_match_3: forall vl x1 t1 x2 t2 x3 t3 ,
dl_vl_match ⌞x1 @ t1 ; x2 @ t2 ; x3 @ t3⌟ (rev vl) = true ->
exists v1 v2 v3, vl = v1 :: v2 :: v3 :: nil /\
type_val_match t3 v1 = true /\
type_val_match t2 v2 = true /\
type_val_match t1 v3 = true.
Lemma dl_vl_match_4: forall vl x1 t1 x2 t2 x3 t3 x4 t4 ,
dl_vl_match ⌞x1 @ t1 ; x2 @ t2 ; x3 @ t3 ; x4 @ t4⌟ (rev vl) = true ->
exists v1 v2 v3 v4, vl = v1 :: v2 :: v3 :: v4 :: nil /\
type_val_match t4 v1 = true /\
type_val_match t3 v2 = true /\
type_val_match t2 v3 = true /\
type_val_match t1 v4 = true.
Lemma dl_vl_match_5: forall vl x1 t1 x2 t2 x3 t3 x4 t4 x5 t5 ,
dl_vl_match ⌞x1 @ t1 ; x2 @ t2 ; x3 @ t3 ; x4 @ t4 ; x5 @ t5⌟ (rev vl) = true ->
exists v1 v2 v3 v4 v5,
vl = v1 :: v2 :: v3 :: v4 :: v5 :: nil /\
type_val_match t5 v1 = true /\
type_val_match t4 v2 = true /\
type_val_match t3 v3 = true /\
type_val_match t2 v4 = true /\
type_val_match t1 v5 = true.
Lemma dl_vl_match_6 :
forall vl x1 t1 x2 t2 x3 t3 x4 t4 x5 t5 x6 t6 ,
dl_vl_match ⌞x1 @ t1 ; x2 @ t2 ; x3 @ t3 ; x4 @ t4 ; x5 @ t5 ; x6 @ t6⌟ (rev vl) = true ->
exists v1 v2 v3 v4 v5 v6,
vl = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: nil /\
type_val_match t6 v1 = true /\
type_val_match t5 v2 = true /\
type_val_match t4 v3 = true /\
type_val_match t3 v4 = true /\
type_val_match t2 v5 = true /\
type_val_match t1 v6 = true.
Ltac unfold_internal_pre_post :=
match goal with
| H:_
|- {|_ , _, _, ?r, _|}|- {{?p}}_ {{_}} =>
match p with
| (?p ** ?t _ _) ** A_dom_lenv ?b =>
try unfold t
end;
match r with
| context [(_ ** ?t _ _ _) ** A_dom_lenv ?b] =>
try unfold t
end
| _ => idtac
end.
Ltac init_retspec :=
match goal with
| H : Some _ = BuildRetI _ _ _ _ _ |- _ =>
unfold BuildRetI in H; simpl in H; inverts H
| H : Some _ = BuildRetA´ _ _ _ _ |- _ =>
unfold BuildRetA´ in H; simpl in H; inverts H
end.
Ltac init_prespec :=
match goal with
| H : Some _ = BuildPreI ?x ?y ?z _ _ |- _ =>
unfold BuildPreI in H;
let xy:= fresh in
remember (x y) as xy;
destruct xy as [ xy | ]; tryfalse;
let a := fresh in
destruct xy as [ [ [ ? a ] ] ];
let b := fresh in
remember (dl_vl_match a (rev z)) as b;
destruct b; tryfalse
| H: Some _ = BuildPreA´ ?x ?y _ ?z |- _ =>
unfold BuildPreA´ in H;
let xy := fresh in
remember (x y) as xy;
destruct xy as [ xy | ]; tryfalse;
let a := fresh in
destruct xy as [ [ [ ? a ] ] ];
let b := fresh in
remember (dl_vl_match a (rev z)) as b;
destruct b; tryfalse
end;
match goal with
| H : Some _ = _ _ |- _ => inverts H
end;
match goal with
| H : true = _ ?l _ |- _ => apply sym_eq in H;
match listlen l with
| 0%nat => apply dl_vl_match_0 in H; mytac
| 1%nat => apply dl_vl_match_1 in H; mytac
| 2%nat => apply dl_vl_match_2 in H; mytac
| 3%nat => apply dl_vl_match_3 in H; mytac
| 4%nat => apply dl_vl_match_4 in H; mytac
| 5%nat => apply dl_vl_match_5 in H; mytac
| 6%nat => apply dl_vl_match_6 in H; mytac
| _ => fail
end
end;
match goal with
| H : Some _ = _ |- _ =>
simpl in H; inverts H
end;
do 4 eexists; split; auto.
Ltac init_spec_api :=
intros; init_retspec; init_prespec;
eapply backward_rule1;
[ apply Aop_Aop´_eq´
| idtac ];
let H := fresh in
eapply r_conseq_rule;
[ intros ? ? H; apply Aop_Aop´_eq; exact H
| intros ? H; exact H
| idtac ];
type_val_match_elim.
Ltac init_spec_internal := intros; init_retspec; init_prespec;
type_val_match_elim; unfold_internal_pre_post.
Ltac init_spec := first [init_spec_api | init_spec_internal ].
Tactic Notation "init" "spec" :=
init_spec.
Close Scope code_scope.