1 files changed, 27 insertions, 29 deletions
diff --git a/sound.v b/sound.v
index 761d7ad..2ae5001 100644
--- a/sound.v
+++ b/sound.v
@@ -13,9 +13,8 @@ Lemma strong_value_stuck_rtc sv e:
  expr_from_strong_value sv -->* e →
  e = expr_from_strong_value sv.
 Proof.
-  intros. inv H.
+  intros. inv H; [done|].
-  - reflexivity.
+  exfalso. apply strong_value_stuck with (sv := sv). by exists y.
-  - exfalso. apply strong_value_stuck with (sv := sv). by exists y.
 Qed.
 Lemma force__strong_value (e : expr) (v : value) :
@@ -68,33 +67,32 @@ Lemma force_map_fmap_union_insert (sws : gmap string strong_value) es k e sv :
 Proof.
  intros [n Hsteps] % rtc_nsteps.
  revert sws es k e Hsteps.
-  induction n; intros sws es k e Hsteps.
+  induction n; intros sws es k e Hsteps; [inv Hsteps|].
-  - inv Hsteps.
+  inv Hsteps.
-  - inv Hsteps.
+  inv H0.
-    inv H0.
+  inv H2.
-    inv H2.
+  - inv H3. inv H1.
-    + inv H3. inv H1.
+    + simplify_option_eq. unfold expr_from_strong_value, compose.
-      * simplify_option_eq. unfold expr_from_strong_value, compose.
+      by rewrite H4.
-        by rewrite H4.
+    + edestruct strong_value_stuck. exists y. done.
-      * edestruct strong_value_stuck. exists y. done.
+  - inv H0. simplify_option_eq.
-    + inv H0. simplify_option_eq.
+    apply rtc_transitive
-      apply rtc_transitive
+    with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪
-      with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪
+      (expr_from_strong_value <$> sws))))).
-        (expr_from_strong_value <$> sws))))).
+    + do 2 rewrite <-insert_union_l.
-      * do 2 rewrite <-insert_union_l.
+      apply rtc_once.
-        apply rtc_once.
+      eapply E_Ctx
-        eapply E_Ctx
+      with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪
-        with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪
+        (expr_from_strong_value <$> sws)))))).
-          (expr_from_strong_value <$> sws)))))).
+      * eapply IsCtx_Compose.
-        -- eapply IsCtx_Compose.
+        -- constructor.
+        -- eapply IsCtx_Compose
+           with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪
+             (expr_from_strong_value <$> sws)))))).
           ++ constructor.
-           ++ eapply IsCtx_Compose
+           ++ done.
-              with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪
+      * done.
-                (expr_from_strong_value <$> sws)))))).
+    + by apply IHn.
-              ** constructor.
-              ** done.
-        -- done.
-      * by apply IHn.
 Qed.
 Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x

diff --git a/sound.v b/sound.v index 761d7ad..2ae5001 100644 --- a/sound.v +++ b/sound.v
@@ -13,9 +13,8 @@ Lemma strong_value_stuck_rtc sv e:
13	expr_from_strong_value sv -->* e →	13	expr_from_strong_value sv -->* e →
14	e = expr_from_strong_value sv.	14	e = expr_from_strong_value sv.
15	Proof.	15	Proof.
16	intros. inv H.	16	intros. inv H; [done\|].
17	- reflexivity.	17	exfalso. apply strong_value_stuck with (sv := sv). by exists y.
18	- exfalso. apply strong_value_stuck with (sv := sv). by exists y.
19	Qed.	18	Qed.
20		19
21	Lemma force__strong_value (e : expr) (v : value) :	20	Lemma force__strong_value (e : expr) (v : value) :
@@ -68,33 +67,32 @@ Lemma force_map_fmap_union_insert (sws : gmap string strong_value) es k e sv :
68	Proof.	67	Proof.
69	intros [n Hsteps] % rtc_nsteps.	68	intros [n Hsteps] % rtc_nsteps.
70	revert sws es k e Hsteps.	69	revert sws es k e Hsteps.
71	induction n; intros sws es k e Hsteps.	70	induction n; intros sws es k e Hsteps; [inv Hsteps\|].
72	- inv Hsteps.	71	inv Hsteps.
73	- inv Hsteps.	72	inv H0.
74	inv H0.	73	inv H2.
75	inv H2.	74	- inv H3. inv H1.
76	+ inv H3. inv H1.	75	+ simplify_option_eq. unfold expr_from_strong_value, compose.
77	* simplify_option_eq. unfold expr_from_strong_value, compose.	76	by rewrite H4.
78	by rewrite H4.	77	+ edestruct strong_value_stuck. exists y. done.
79	* edestruct strong_value_stuck. exists y. done.	78	- inv H0. simplify_option_eq.
80	+ inv H0. simplify_option_eq.	79	apply rtc_transitive
81	apply rtc_transitive	80	with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪
82	with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪	81	(expr_from_strong_value <$> sws))))).
83	(expr_from_strong_value <$> sws))))).	82	+ do 2 rewrite <-insert_union_l.
84	* do 2 rewrite <-insert_union_l.	83	apply rtc_once.
85	apply rtc_once.	84	eapply E_Ctx
86	eapply E_Ctx	85	with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪
87	with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪	86	(expr_from_strong_value <$> sws)))))).
88	(expr_from_strong_value <$> sws)))))).	87	* eapply IsCtx_Compose.
89	-- eapply IsCtx_Compose.	88	-- constructor.
		89	-- eapply IsCtx_Compose
		90	with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪
		91	(expr_from_strong_value <$> sws)))))).
90	++ constructor.	92	++ constructor.
91	++ eapply IsCtx_Compose	93	++ done.
92	with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪	94	* done.
93	(expr_from_strong_value <$> sws)))))).	95	+ by apply IHn.
94	** constructor.
95	** done.
96	-- done.
97	* by apply IHn.
98	Qed.	96	Qed.
99		97
100	Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x	98	Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x