From 80f307850d74f1fbb8b5df2f9e7ecde8e13642ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Mar 2019 22:27:44 -0500 Subject: Add UnderLets.list_rect_arrow_interp_related --- src/UnderLetsProofs.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 41bf801d2..77030b646 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -518,6 +518,36 @@ Module Compilers. ls'). Proof using Type. induction Hls; cbn [list_rect] in *; auto. Qed. + Lemma list_rect_arrow_interp_related {A B C Pnil Pcons ls x B' C' Pnil' Pcons' ls' x' R} + {R' : B -> B' -> Prop} + (Hnil : forall x x', interp_related R (Pnil x) (Pnil' x')) + (Hcons : forall x x', + expr.interp_related ident_interp x x' + -> forall l l', + List.Forall2 (expr.interp_related ident_interp) l l' + -> forall rec rec', + (forall v v', R' v v' -> interp_related R (rec v) (rec' v')) + -> forall v v', + R' v v' + -> interp_related R (Pcons x l rec v) (Pcons' x' l' rec' v')) + (Hls : List.Forall2 (expr.interp_related ident_interp (t:=A)) ls ls') + (Hx : R' x x') + : interp_related + R + (list_rect + (fun _ : list _ => B -> UnderLets C) + Pnil + Pcons + ls + x) + (list_rect + (fun _ : list _ => B' -> C') + Pnil' + Pcons' + ls' + x'). + Proof using Type. revert x x' Hx; induction Hls; cbn [list_rect] in *; auto. Qed. + Lemma nat_rect_interp_related {A PO PS n A' PO' PS' n' R} (Hnil : interp_related R PO PO') (Hcons : forall n rec rec', -- cgit v1.2.3