Commit 97bdda19 authored by Ike Mulder's avatar Ike Mulder
Browse files

Added extra reloc reasoning principle, added more mutual recursive function...

Added extra reloc reasoning principle, added more mutual recursive function tests, simplified AsFunOfOnly with pattern Ltac.
parent d2866f65
Pipeline #67148 failed with stage
in 11 minutes and 37 seconds
......@@ -137,4 +137,5 @@ Proof.
eapply (refines_sound Σ).
iIntros (? Δ).
iApply fg_cg_incrementer_refinement.
Qed.
\ No newline at end of file
Qed.
......@@ -86,6 +86,12 @@ Section main.
HINT1 empty_hyp_first [tpwp_def j e E1 E2 Φ] [id]; tpwp j e E1 E2 Φ.
Proof. move => <-. iStepS. rewrite tpwp_eq. iStepS. by iApply "H1". Qed.
Global Instance restore_if_right_val e1 e2 v A E :
TCIf (TCEq E ) False TCTrue
IntoVal e2 v
HINT1 empty_hyp_last [|={E,}=> REL e1 << v : A] [id]; REL e1 << (inl e2) @ E : A.
Proof. move => _ <-. iStepS. by iApply restore_mask. Qed.
Global Instance tpwp_abduct_K_val j e E1 E2 Φ v K:
IntoVal e v
HINT1 empty_hyp_first [tpwp_def j (fill K e) E1 E2 Φ] [id]; tpwp j (fill K e) E1 E2 Φ.
......
......@@ -155,10 +155,8 @@ Section proof.
iStepsS. iLöb as "IH". rel_rec_l.
iStepsS.
destruct x4 as [|h1 ls1]; iReIntro "H7".
- iStepR; iStepsS. iRestore.
iStepsS.
- iRestore.
iStepsS.
- iStepR; iStepsS.
- iRestore; iStepsS.
Qed.
Definition stackInt A : lrel Σ := LRel (λ v1 v2,
......
......@@ -36,8 +36,7 @@ Section symbol_refinement.
repeat (iApply refines_pair).
- iStepsS.
- iStepsS. (* after store: run store on RHS. *) do 44 iStepR. iRestore.
iStepsS. (* after store CONS: run all on RHS *) repeat iStepR. iRestore.
iStepsS.
iStepsS. (* after store CONS: run all on RHS *) repeat iStepR.
- iStepsS. (* after load, do load on RHS. *) repeat iStepR. rewrite bool_decide_true; last lia.
do 8 iStepR. iRestore.
iStepsS. (* after 2nd load, do 2nd load on RHS. *) repeat iStepR. iRestore.
......@@ -57,8 +56,7 @@ Section symbol_refinement.
repeat (iApply refines_pair).
- iStepsS.
- iStepsS. (* after store: run store on RHS. *) do 44 iStepR. iRestore.
iStepsS. (* after store CONS: run all on RHS *) repeat iStepR. iRestore.
iStepsS.
iStepsS. (* after store CONS: run all on RHS *) repeat iStepR.
- iStepsS. rewrite bool_decide_true; last lia.
iStepsS. (* first op: do nothing on RHS. *) iRestore.
iStepsS. (* this load: do load on RHS. *) do 8 iStepR. iRestore.
......
......@@ -158,7 +158,6 @@ Section list_functions.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS. iStepDebug. solveStep with "H1". iSolveTC. simpl.
Qed.
......
......@@ -69,6 +69,9 @@ Section list_functions.
Definition is_literal_list (l : val) (vs : list val) :=
is_list l (map (λ vl vr, vl = vr%I) vs).
Definition is_Z_list (l : val) (zs : list Z) :=
is_literal_list l (map (LitV LitInt) zs).
Inductive tree (A : Type) :=
leaf : A tree A
| node : list (tree A) tree A.
......@@ -82,9 +85,9 @@ Section list_functions.
list_sum (map (tree_size) ts)
end.
Fixpoint is_tree (l : val) (t : tree val) : iProp Σ :=
Fixpoint is_tree (l : val) (t : tree Z) : iProp Σ :=
match t with
| leaf a => l = InjLV a
| leaf a => l = InjLV $ #a
| node ts => (l' : val), l = InjRV l'
is_list l' (map (λ t v, is_tree v t) ts)
end.
......@@ -139,15 +142,15 @@ Section list_functions.
{{ True }}
Case l e1 e2
{{ [^0] RET Case l e1 e2;
(( (a : val), t = leaf a) ( (ts : list $ tree val), t = node ts)) is_tree l t }} | 50.
(( (a : Z), t = leaf a) ( (ts : list $ tree Z), t = node ts)) is_tree l t }} | 50.
Proof.
iStepsS. destruct t as [a|ts]; eauto.
Qed.
Global Instance flatten_tree_help_spec (lt lvs : val) (t : tree val) (vs : list val) :
SPEC {{ is_tree lt t is_literal_list lvs vs }}
Global Instance flatten_tree_help_spec (lt lvs : val) (t : tree Z) (zs : list Z) :
SPEC {{ is_tree lt t is_Z_list lvs zs }}
flatten_tree_help lt lvs
{{ (v : val), RET v; is_literal_list v (flatten_tree t ++ vs) }}.
{{ (v : val), RET v; is_Z_list v (flatten_tree t ++ zs) }}.
Proof.
do 31 iStepS; [iStepsS | ].
iStepDebug. solveStep with empty_hyp_last; [iSolveTC | simpl].
......@@ -191,24 +194,24 @@ Section list_functions.
iStepDebug.
solveStep with "H2";[iSolveTC | simpl].
iStepsS.
rewrite /is_literal_list.
rewrite /is_Z_list /is_literal_list.
rewrite app_assoc.
iStepsS.
Qed.
Hint Extern 4 (@map ?A _ ?f ?l = []) =>
unify l (@nil A); reflexivity : solve_pure_eq_add.
cut (l = []); [ move => -> // | pure_solver.trySolvePure] : solve_pure_eq_add.
Lemma flatten_tree_spec (lt : val) (t : tree val) :
Lemma flatten_tree_spec (lt : val) (t : tree Z) :
SPEC {{ is_tree lt t }}
hl_flatten_tree lt
{{ (v : val), RET v; is_literal_list v (flatten_tree t) }}.
{{ (v : val), RET v; is_Z_list v (flatten_tree t) }}.
Proof.
iStepsS. rewrite right_id.
iStepsS.
Qed.
Lemma tree_size_spec (l : val) (t : tree val) :
Lemma tree_size_spec (l : val) (t : tree Z) :
SPEC {{ is_tree l t }} hl_tree_size l {{ RET #(tree_size t); is_tree l t }}.
Proof.
do 25 iStepS; [iStepsS| ].
......@@ -248,6 +251,222 @@ Section list_functions.
iStepsS.
Qed.
Fixpoint in_tree_b `{EqDecision A} (a : A) (t : tree A) : bool :=
match t with
| leaf a' => if decide (a' = a) then true else false
| node ts =>
foldr orb false $ map (in_tree_b a) ts
end.
Fixpoint in_tree {A : Type} (a : A) (t : tree A) : Prop :=
match t with
| leaf a' => a' = a
| node ts =>
foldr or False $ map (in_tree a) ts
end.
Fixpoint tree_depth {A : Type} (t : tree A) : nat :=
match t with
| leaf _ => 0
| node ts =>
S (foldr max 0 $ map tree_depth ts)
end.
Lemma tree_depth_ind {A : Type} (P : tree A Prop) :
( (n : nat) (t : tree A), tree_depth t n P t)
( t : tree A, P t).
Proof.
intros. elim: t.
- intros. apply (H O). simpl. lia.
- intros.
apply (H (tree_depth $ node l)). done.
Qed.
Lemma tree_strong_ind {A : Type} (P : tree A Prop) :
( a : A, P (leaf a))
( l : list (tree A), ( t : tree A, t l P t) P (node l))
( t : tree A, P t).
Proof.
move => Hleaf Hnode.
apply tree_depth_ind. elim.
- elim; first (intros; apply Hleaf).
move => l /= Hl. lia.
- move => n Hn.
elim; first (intros; apply Hleaf).
elim.
* intros. apply Hnode. intros. inversion H0.
* intros. apply Hnode. intros.
apply Hn.
apply le_S_n. etrans; last apply H0.
revert H1. generalize (a :: l).
elim; first (move => H3; inversion H3).
intros. inversion_clear H2.
+ simpl. apply le_n_S. apply Max.le_max_l.
+ simpl. etrans; last first.
apply le_n_S. apply Max.le_max_r. by apply H1.
Qed.
Lemma in_tree_in_tree_b_iff `{EqDecision A} (a : A) (t : tree A) :
in_tree_b a t in_tree a t.
Proof.
induction t as [a'|ts IH] using tree_strong_ind.
- simpl. destruct (decide (a' = a)) as [->|Hneq]; split; eauto. case.
- revert IH. elim: ts; first done.
intros. simpl.
rewrite orb_True. rewrite IH; last left.
change (foldr orb false (map (in_tree_b a) l)) with (in_tree_b a (node l)).
rewrite H //. intros. apply IH. by right.
Qed.
Global Instance in_tree_dec `{EqDecision A} (a : A) (t : tree A) : Decision (in_tree a t).
Proof.
rewrite /Decision.
destruct (in_tree_b a t) eqn:Heq; [left|right];
rewrite -in_tree_in_tree_b_iff Heq //. exact id.
Defined.
Definition hl_in_tree : val :=
rec: "in_tree" "v" "t" :=
let: "in_ltreef" :=
rec: "in_ltree" "ts" :=
match: "ts" with
NONE => #false
| SOME "lh" =>
let: "lv" := ! "lh" in
"in_tree" "v" (Fst "lv") || "in_ltree" (Snd "lv")
end
in
match: "t" with
InjL "a" => "a" = "v"
| InjR "ts" =>
"in_ltreef" "ts"
end.
Global Instance or_complement (P Q : Prop) : Decision (P Q) Decision P Decision (¬P Q).
Proof.
intros. case: H.
- case: H0.
* intros. right. move => [HP HQ]. by apply HP.
* intros. left. split => //. case: a => //.
- move => /Decidable.not_or [HP HQ]. right. move => [HP' HQ']. by apply HQ.
Qed.
Lemma or_assume_left_not (P Q : Prop) : Decision P P Q P (¬P Q).
Proof.
intros.
destruct H; split; case; eauto.
case => _ HQ. by right.
Qed.
Lemma decision_iff (P Q : Prop) : Decision P P Q Decision Q.
Proof.
case => HP HPQ.
- left. by apply HPQ.
- right. rewrite -HPQ //.
Qed.
Lemma bool_decide_eq `{!Decision P, !Decision Q} : (bool_decide P = bool_decide Q) (P Q).
Proof.
split.
- case: Decision0 => HP.
* rewrite bool_decide_true //.
move => HQ. apply eq_sym, bool_decide_eq_true in HQ. split =>//.
* rewrite bool_decide_false //.
move => HQ. apply eq_sym, bool_decide_eq_false in HQ. split =>//.
- move => HPQ.
case: Decision0 => HP.
* rewrite bool_decide_true //.
apply eq_sym, bool_decide_eq_true, HPQ, HP.
* rewrite bool_decide_false //.
apply eq_sym, bool_decide_eq_false.
rewrite -HPQ //.
Qed.
Lemma bool_decide_or_2 (P Q : Prop) (HPQ : Decision (P Q)) (HP : Decision P) (HQ : Decision Q) :
@bool_decide (P Q) HPQ = bool_decide P || bool_decide Q.
Proof.
destruct (bool_decide _) eqn:HPQt; last first.
{ apply bool_decide_eq_false_1, Decidable.not_or in HPQt as [HnP HnQ].
rewrite !bool_decide_false //. }
apply bool_decide_eq_true_1 in HPQt. destruct HPQt as [HPt|HQt].
- rewrite bool_decide_true //.
- generalize (bool_decide P) => b. rewrite bool_decide_true //. by destruct b.
Qed.
Lemma bool_decide_or_3 (P Q : Prop) (HPQ : Decision (P Q)) (HP : Decision P) :
@bool_decide (P Q) HPQ = bool_decide P || bool_decide (¬ P Q).
Proof.
etrans; last first. rewrite -bool_decide_or_2 //.
apply bool_decide_eq, or_assume_left_not, HP.
Qed.
Lemma hl_in_tree_spec (t : tree Z) (tv : val) (a : Z) :
SPEC {{ is_tree tv t }} hl_in_tree #a tv {{ RET #(bool_decide (in_tree a t)); is_tree tv t }}.
Proof.
do 31 iStepS; [iStepsS; shelve | ].
iStepDebug. solveStep with empty_hyp_last. iSolveTC. simpl.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
{ apply map_eq_nil in H1. subst.
iReIntro "H3".
iStepsS. }
apply map_eq_cons in H1 as [vs [vss' [-> [Hvs Hvss']]]]. subst.
iReIntro "H3".
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepDebug.
solveStep with "H2". iSolveTC. simpl.
iStepsS. erewrite bool_decide_or_2. rewrite (bool_decide_false (in_tree _ _)) //.
Unshelve.
- destruct (decide (x0 = x1)) as [->|Hneq].
* rewrite !bool_decide_true //.
* rewrite !bool_decide_false //. contradict Hneq. simplify_eq => //.
- erewrite bool_decide_or_3. rewrite bool_decide_true //.
Qed.
Definition flatten : val :=
rec: "flatten" "l" :=
let: "auxfun" := rec: "aux" "vs" "rem" :=
......
......@@ -192,21 +192,10 @@ Global Hint Extern 4 (TCIfEq _ _ _) =>
Ltac get_as_fun_of_raw term arg := (* does not check that arg is a variable *)
lazymatch term with
| context pat [arg] =>
let x := fresh "x" in
let result := constr:((
fun x => ltac:(
let term' := context pat[x] in
let result' := get_as_fun_of_raw term' arg in
let result_nrm := eval cbn in (result' x) in
exact (result_nrm)
)
)) in
result
| _ =>
let atype := type of arg in
constr:((λ _ : atype, term))
let pat := eval pattern arg in term in
lazymatch pat with
| ?the_fun arg =>
constr:(the_fun)
end.
Ltac get_as_fun_of term arg := (* shortcircuits to trivial function if arg is not a variable *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment