aboutsummaryrefslogtreecommitdiffstats
path: root/complete.v
diff options
context:
space:
mode:
Diffstat (limited to 'complete.v')
-rw-r--r--complete.v58
1 files changed, 28 insertions, 30 deletions
diff --git a/complete.v b/complete.v
index 9939b50..5a2ccdc 100644
--- a/complete.v
+++ b/complete.v
@@ -34,36 +34,34 @@ Proof.
34 induction v using strong_value_ind'; try by exists 2. 34 induction v using strong_value_ind'; try by exists 2.
35 unfold expr_from_strong_value. simpl. 35 unfold expr_from_strong_value. simpl.
36 fold expr_from_strong_value. 36 fold expr_from_strong_value.
37 induction bs using map_ind. 37 induction bs using map_ind; [by exists 2|].
38 + by exists 2. 38 apply map_Forall_insert in H as [[n Hn] H2]; try done.
39 + apply map_Forall_insert in H as [[n Hn] H2]; try done. 39 apply IHbs in H2 as [o Ho]. clear IHbs.
40 apply IHbs in H2 as [o Ho]. clear IHbs. 40 exists (S (n `max` o)).
41 exists (S (n `max` o)). 41 rewrite eval_S. csimpl.
42 rewrite eval_S. csimpl. 42 setoid_rewrite map_mapM_Some_2_L
43 setoid_rewrite map_mapM_Some_2_L 43 with (m2 := value_from_strong_value <$> <[i := x]>m);
44 with (m2 := value_from_strong_value <$> <[i := x]>m); csimpl. 44 csimpl; [by rewrite <-map_fmap_compose|].
45 * by rewrite <-map_fmap_compose. 45 destruct o as [|o]; csimpl in *; try discriminate.
46 * destruct o as [|o]; csimpl in *; try discriminate. 46 apply map_Forall2_alt_L.
47 apply map_Forall2_alt_L. 47 split; [set_solver|].
48 split. 48 intros j u v ??. rewrite eval_S in Ho.
49 -- set_solver. 49 apply bind_Some in Ho as [vs [Ho1 Ho2]].
50 -- intros j u v ??. rewrite eval_S in Ho. 50 setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq.
51 apply bind_Some in Ho as [vs [Ho1 Ho2]]. 51 unfold expr_from_strong_value in Ho2.
52 setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq. 52 rewrite map_fmap_compose in Ho2.
53 unfold expr_from_strong_value in Ho2. 53 simplify_eq.
54 rewrite map_fmap_compose in Ho2. 54 destruct (decide (i = j)).
55 simplify_eq. 55 - simplify_eq.
56 destruct (decide (i = j)). 56 repeat rewrite lookup_fmap, lookup_insert in *.
57 ++ simplify_eq. 57 simplify_eq/=.
58 repeat rewrite lookup_fmap, lookup_insert in *. 58 apply eval_le with (n := n); lia || done.
59 simplify_eq/=. 59 - repeat rewrite lookup_fmap, lookup_insert_ne in * by done.
60 apply eval_le with (n := n); lia || done. 60 repeat rewrite <-lookup_fmap in *.
61 ++ repeat rewrite lookup_fmap, lookup_insert_ne in * by done. 61 apply map_Forall2_alt_L in Ho1.
62 repeat rewrite <-lookup_fmap in *. 62 destruct Ho1 as [Ho1 Ho2].
63 apply map_Forall2_alt_L in Ho1. 63 apply eval_le with (n := o); try lia.
64 destruct Ho1 as [Ho1 Ho2]. 64 by apply Ho2 with (i := j).
65 apply eval_le with (n := o); try lia.
66 by apply Ho2 with (i := j).
67Qed. 65Qed.
68 66
69Lemma eval_force_strong_value' v : 67Lemma eval_force_strong_value' v :