simplify proofs for cyclic lists (#126)

affeldt-aist · Oct 31, 2023 · 68841f8 · 68841f8
1 parent 1679e81
commit 68841f8
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 13 deletions.
diff --git a/example_typed_store.v b/example_typed_store.v
@@ -117,14 +117,11 @@ rewrite bindA.
 under eq_bind => tl.
   rewrite !bindA.
   under eq_bind do rewrite !bindA bindretf !bindA bindretf /=.
-  rewrite -bindA.
   over.
-rewrite -bindA crunret // -bindA_uncurry /= crungetput // bindA.
-under eq_bind => tl.
-  rewrite !bindA.
-  under eq_bind do rewrite bindretf /=.
-  over.
-by rewrite crungetnew // -(bindskipf (_ >>= _)) crunnewget // crunskip.
+rewrite -bindA_uncurry -bindA crunret // crungetput // bindA.
+under eq_bind do rewrite !bindA.
+under eq_bind do under eq_bind do rewrite bindretf /=.
+by rewrite crungetnew // crunnewget0.
 Qed.
 
 Definition tl (T : ml_type) (param : coq_type (ml_rlist T))
@@ -141,16 +138,14 @@ Proof.
 rewrite bindA -cnewchk.
 under eq_bind => r1.
   under eq_bind do rewrite !bindA.
-  under eq_bind do under eq_bind do rewrite !(bindA,bindretf) /=.
-  under cchknewE do rewrite -bindA cputgetC //.
+  under cchknewE do rewrite !(bindA,bindretf) -bindA cputgetC //.
   rewrite cnewget /=.
-  under eq_bind do under eq_bind do rewrite cputget /=.
-  rewrite -bindA.
+  under cchknewE do rewrite cputget /=.
   over.
-rewrite cnewchk -bindA crunret // -bindA_uncurry /= crungetput // bindA.
+rewrite cnewchk -bindA_uncurry -bindA crunret // crungetput // bindA.
 under eq_bind do rewrite !bindA.
 under eq_bind do under eq_bind do rewrite bindretf /=.
-by rewrite crungetnew // -(bindskipf (_ >>= _)) crunnewget // crunskip.
+by rewrite crungetnew // crunnewget0.
 Qed.
 
 End cyclic.

diff --git a/typed_store_lib.v b/typed_store_lib.v
@@ -97,6 +97,9 @@ Proof. by rewrite bindA bindskipf cgetget. Qed.
 Lemma cgetret T (r : loc T) : cget r >>= Ret = cget r :> M _.
 Proof. by rewrite bindmret. Qed.
 
+Lemma crunnewget0 T s : crun (cnew T s >>= fun r => cget r : M _).
+Proof. by rewrite -(bindskipf (_ >>= _)) crunnewget // crunskip. Qed.
+
 Lemma crunnew0 T s : crun (cnew T s : M _).
 Proof. by rewrite -(bindskipf (cnew T s)) crunnew // crunskip. Qed.