Skip to content

Commit aaa37c6

Browse files
committed
Prove mrec_loop2
1 parent cf1443c commit aaa37c6

File tree

1 file changed

+94
-0
lines changed

1 file changed

+94
-0
lines changed

theories/Interp/RecursionFacts.v

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -254,3 +254,97 @@ Instance euttge_interp_mrec' {E D R} (ctx : D ~> itree (D +' E)) :
254254
Proof.
255255
do 4 red. eapply euttge_interp_mrec. reflexivity.
256256
Qed.
257+
258+
Module Interp_mrec_loop2.
259+
260+
Inductive invariant {D E} (ctx : D ~> itree (D +' E)) {R}
261+
: itree (D +' E) R -> itree (D +' E) R -> Prop :=
262+
| Equal {t} : invariant ctx t t
263+
| Interp {A} {t : itree (D +' E) A} {k k' : A -> _} : (forall a, invariant ctx (k a) (k' a)) -> invariant ctx (t >>= k) (interp (Handler.case_ ctx Handler.inr_) t >>= k')
264+
| Bind {A} {t : itree (D +' E) A} {k k' : A -> _}
265+
: (forall (a : A), invariant ctx (k a) (k' a)) ->
266+
invariant ctx (t >>= k) (t >>= fun x => k' x)
267+
.
268+
Hint Constructors invariant : core.
269+
270+
Inductive itree_case {E R} (t : itree E R) : Prop :=
271+
| CaseRet r : Ret r ≅ t -> itree_case t
272+
| CaseTau u : Tau u ≅ t -> itree_case t
273+
| CaseVis A (e : E A) k : Vis e k ≅ t -> itree_case t.
274+
275+
Lemma case_itree {E R} (t : itree E R) : itree_case t.
276+
Proof.
277+
destruct (observe t) eqn:Eq.
278+
- econstructor 1. rewrite <- Eq, <- itree_eta; reflexivity.
279+
- econstructor 2. rewrite <- Eq, <- itree_eta; reflexivity.
280+
- econstructor 3. rewrite <- Eq, <- itree_eta; reflexivity.
281+
Qed.
282+
283+
Lemma interp_mrec_loop2_ {D E} (ctx : D ~> itree (D +' E)) {R}
284+
: forall {t : itree (D +' E) R} {u : itree (D +' E) R},
285+
invariant ctx t u -> interp_mrec ctx t ≈ interp_mrec (Handler.cat ctx (Handler.case_ ctx Handler.inr_)) u.
286+
Proof with auto.
287+
einit.
288+
ecofix SELF. induction 1 as [t | A t k | A t k k'].
289+
- destruct (case_itree t) as [ ? H | u H | A [d|e] k H ]; rewrite <- H; rewrite 2 unfold_interp_mrec; simpl.
290+
+ eret.
291+
+ etau.
292+
+ etau.
293+
+ evis.
294+
- destruct (case_itree t) as [ ? W | u W | ? [d|e] h W ]; rewrite <- W.
295+
+ rewrite interp_ret. rewrite 2 bind_ret_l.
296+
apply H0.
297+
+ rewrite interp_tau, 2 bind_tau, 2 unfold_interp_mrec. simpl.
298+
etau.
299+
+ rewrite interp_vis. simpl. rewrite bind_bind.
300+
rewrite unfold_interp_mrec; simpl.
301+
destruct (case_itree (ctx _ d)) as [ ? H1 | ? H1 | ? [d'|e] ? H1 ]; rewrite <- H1.
302+
* rewrite 2 bind_ret_l.
303+
rewrite bind_tau.
304+
rewrite unfold_interp_mrec with (t := Tau _); simpl.
305+
etau.
306+
* rewrite 2 bind_tau.
307+
rewrite 2 unfold_interp_mrec; simpl.
308+
rewrite tau_euttge.
309+
setoid_rewrite tau_euttge at 3.
310+
etau. ebase.
311+
* rewrite 2 bind_vis, 2 unfold_interp_mrec. simpl.
312+
rewrite tau_euttge.
313+
unfold Handler.cat at 2.
314+
setoid_rewrite tau_euttge at 3.
315+
etau. ebase. right. apply SELFL. eauto.
316+
* rewrite 2 bind_vis, 2 unfold_interp_mrec; simpl.
317+
rewrite tau_euttge.
318+
setoid_rewrite tau_euttge at 3.
319+
evis. etau. ebase.
320+
+ rewrite interp_vis; simpl. unfold Handler.inr_ at 2, Handler.htrigger.
321+
rewrite bind_trigger. rewrite 2 bind_vis.
322+
rewrite 2 unfold_interp_mrec; simpl.
323+
setoid_rewrite unfold_interp_mrec at 2; simpl.
324+
setoid_rewrite tau_euttge at 3.
325+
evis. etau.
326+
- destruct (case_itree t) as [ ? W | ? W | ? [d|e] h W]; rewrite <- W.
327+
+ rewrite 2 bind_ret_l. apply H0.
328+
+ rewrite 2 bind_tau, 2 unfold_interp_mrec; simpl. etau.
329+
+ rewrite 2 bind_vis, 2 unfold_interp_mrec; simpl.
330+
unfold Handler.cat at 2. etau. ebase.
331+
+ rewrite 2 bind_vis, 2 unfold_interp_mrec; simpl. evis. etau.
332+
Qed.
333+
334+
End Interp_mrec_loop2.
335+
336+
Lemma interp_mrec_loop2 {D E} (ctx : D ~> itree (D +' E)) {R} {t : itree (D +' E) R}
337+
: interp_mrec ctx t ≈ interp_mrec (Handler.cat ctx (Handler.case_ ctx inr_)) t.
338+
Proof.
339+
apply Interp_mrec_loop2.interp_mrec_loop2_.
340+
constructor.
341+
Qed.
342+
343+
Theorem mrec_loop2 {D E} (ctx : D ~> itree (D +' E)) {R} {d : D R}
344+
: mrec ctx d ≈ mrec (Handler.cat ctx (Handler.case_ ctx inr_)) d.
345+
Proof.
346+
unfold mrec.
347+
unfold Handler.cat at 2.
348+
rewrite <- unfold_interp_mrec_h.
349+
apply interp_mrec_loop2.
350+
Qed.

0 commit comments

Comments
 (0)